[LTL] Add clocked and disabled property types

[dobios]

#7022 highlighted a difficulty in reasoning about certain characteristics of ltl properties, e.g. finding out how many clocks or disables are associated to a given property without resorting to a use-def analysis.
This PR attempts to solve that by encoded those concepts directly in ltl's type-system.

Let me know what you think!

[uenoku]

FYI you can pass multiple classes to isa<>, e.g:

Suggested change

	return isa<ClockedPropertyType>(type) || isa<ClockedSequenceType>(type) ||
	isa<ClockedDisabledPropertyType>(type);
	return isa<ClockedPropertyType, ClockedSequenceType, ClockedDisabledPropertyType>(type);

[fabianschuiki]

From an implementation point of view this looks great!

I'm wondering if it's worth the complication given what #7022 originally tried to achieve. If I recall correctly, we basically want a clocked_assert op that provides a single unique clock and disable and checks a property/sequence that itself does not have any clock or disable specified. That unclockedness/undisabledness of the operand we'd like to enforce in the clocked_assert op. And the objection to doing so in the verifier was that it would need to traverse the use-def chain, which is considered poor verifier design in MLIR. #7022 identified three options I think:

1. Traverse use-def chain in the verifier. (Thrown out because of potential performance implications.)
2. Encode the clockedness/disabledness in the LTL type system (this PR).
3. Put unclockedness/undisabledness verification into a dedicated pass that runs infrequently.

The one thing that strikes me as odd about the encoding in the type system is that it feels like it's answering a question that isn't useful outside of clocked_assert verification. If I understand correctly, the typing rules for ops is roughly:

• unclocked + unclocked = unclocked property/sequence
• clocked + unclocked = clocked
• clocked + clocked = clocked
• same for disable

So if any operand is a clocked property, the result is also a clocked property. This makes the type answer the question of whether there is any nested property/sequence that is clocked. This feels somewhat unintuitive, since the ltl.clock op specifies a clock for all the nested ops, so it's more about turning a "needs clock" property into a property that has its clock fully specified. This sounds like asking the question whether all nested propertys/sequences are clocked or not. As a concrete example:

%0 = ltl.delay %a : sequence
%1 = ltl.clock %0 : clocked_sequence
%2 = ltl.delay %b : sequence
%3 = ltl.and %1, %2 : clocked_sequence

The fact that %3 reads as a clocked even though it contains a subsequence that still needs a clock to be specified feels unintuitive. So in a sense, encoding the thing that the clocked_assert verifier is interested in in the type system seems to not be really reusable information. But I also get that this is the only way to do it if we want to use the type system for this 😬

What are your thoughts on doing the verification in a dedicated pass? That sounds like it might be simpler than extending the LTL type system.

[ekiwi]

There is a 4th way of fixing this issue: Remove the ltl.clock operation and make Chisel instead emit clocked assert, assume and cover statements. This way you do not have to change the type system, make a checker or even a translation pass. Everything would already by in its most useful form when it comes from Chisel. Are there any downsides to removing ltl.clock?

[dobios]

There is a 4th way of fixing this issue: Remove the ltl.clock operation and make Chisel instead emit clocked assert, assume and cover statements. This way you do not have to change the type system, make a checker or even a translation pass. Everything would already by in its most useful form when it comes from Chisel. Are there any downsides to removing ltl.clock?

Hey @ekiwi! Thanks for the comment! The one reason we would want to keep ltl.clock is to be able to express properties with multiple clocks, i.e. (from my limited knowledge of SV) in SV you can write something like

assert property (@(posedge clk) disable iff (cond) (a |-> (@(posedge fclk) b ##1 c)))

and we would not be able to express that without having ltl.clock or some other way to associate a clock to an arbitrary subproperty without having it be part of the assertion,

That being said, AFAIK we can't actually express that in Chisel (correct me if I'm wrong) but so far the only way I was able to find to connect a clock to a property was via AssertProperty which itself only accepts one clock input. So for the Chisel case, we can probably offload this to the front-end entirely and have it only emit clocked_assert like operations. I'll look into this a bit more and see if this might be an issue for any other front-end (other than SV which isn't really supported yet).

[ekiwi]

Hey @ekiwi! Thanks for the comment! The one reason we would want to keep ltl.clock is to be able to express properties with multiple clocks, i.e. (from my limited knowledge of SV) in SV you can write something like

I never considered this case before, thanks for pointing it out. Do you know what the semantics of this are? Is the property essentially active on either clock edge and then certain automaton transitions are only available depending on which event triggered it?

Anyways, I do feel like once you are in a position where this feature is required, you might be able to come up with a better solution than the very generic ltl.clock operation.

[dobios]

Hey @ekiwi! Thanks for the comment! The one reason we would want to keep ltl.clock is to be able to express properties with multiple clocks, i.e. (from my limited knowledge of SV) in SV you can write something like

I never considered this case before, thanks for pointing it out. Do you know what the semantics of this are? Is the property essentially active on either clock edge and then certain automaton transitions are only available depending on which event triggered it?

Anyways, I do feel like once you are in a position where this feature is required, you might be able to come up with a better solution than the very generic ltl.clock operation.

SV basically has a clock resolution process, where it will check the sequence using the closest parenting clock. So in the case of the example I showed, the consequent sequence in the overlapping implication is describing fclk clock ticks with ##1 rather than clk clock ticks. I think this process is described in IEEE 1800 16.16, and there are some examples of multiple clocks being used later on.

[dobios]

After further reasoning, I don't think that this is a good approach, so I'm closing the PR.