[Verif] Use Seq ClockType for clocked asserts

[fabianschuiki]

The Verif dialect uses i1 operands as clocks: https://github.com/llvm/circt/blob/main/include/circt/Dialect/Verif/VerifOps.td#L72-L82. This should probably be a !seq.clock to align better with other clock uses in the core dialect.

[markram1729]

Hi @fabianschuiki , can i work on this ?

[fabianschuiki]

Absolutely, thanks! 👍

[markram1729]

Hi @fabianschuiki ,
I have one observation
at Verif ClockassertLikeOp, it has ltl.property , structurised same as clockop defined at ltl.clock

if i change this operation , i think i should omit ltl.property

at VerifOps.cpp AssertlikeOp canonicalise assumes ltl::clockop

i need your suggestion here , clockassertlikeop expects ltl property and $clock from ltl.clock
wouldn't it be good if we dont change to !seq.clock

If I need to implement !seq.clock I will change $edge $clock to only $clock

                      ClockEdgeAttr:$edge, I1:$clock,
                      Optional<I1>:$enable,
                      OptionalAttr<StrAttr>:$label);
let assemblyFormat = [{
    $property (`if` $enable^)? `,` $edge $clock 
    (`label` $label^)? attr-dict `:` type($property)
  }]; 

will be changed to

let arguments = (ins LTLAnyPropertyType:$property,
                       ClockType:$clock,
                      Optional<I1>:$enable,
                      OptionalAttr<StrAttr>:$label);
let assemblyFormat = [{
    $property (`if` $enable^)? `,`  $clock 
    (`label` $label^)? attr-dict `:` type($property)
  }]; 

I change the Verifyops.cpp accordingly

testing files as well

[fabianschuiki]

Hey @markram1729, thanks for pushing on this! Why do you have to drop the $edge operand? It would be great if ltl.clock could also have a !seq.clock operand instead of an i1 🙂.