[Verif] fix : Verif Clock I1 to !seq.clock

include/circt/Dialect/Verif/VerifOps.td

@@ -71,10 +71,8 @@ def ClockEdgeAttr : I32EnumAttr<"ClockEdge", "clock edge",
 
 class ClockedAssertLikeOp<string mnemonic, list<Trait> traits = []> :
   VerifOp<mnemonic, traits> {
-  let arguments = (ins LTLAnyPropertyType:$property,
-                      ClockEdgeAttr:$edge, I1:$clock,
-                      Optional<I1>:$enable,
-                      OptionalAttr<StrAttr>:$label);
+  let arguments = (ins LTLAnyPropertyType:$property, ClockEdgeAttr:$edge,
+      ClockType:$clock, Optional<I1>:$enable, OptionalAttr<StrAttr>:$label);
   let assemblyFormat = [{
     $property (`if` $enable^)? `,` $edge $clock 
     (`label` $label^)? attr-dict `:` type($property)
@@ -162,7 +160,7 @@ def HasBeenResetOp : VerifOp<"has_been_reset", [Pure]> {
     startup or power-cycling and the start of reset. `verif.has_been_reset` is
     guaranteed to produce a 0 value in that period, as well as during the reset.
   }];
-  let arguments = (ins I1:$clock, I1:$reset, BoolAttr:$async);
+  let arguments = (ins ClockType:$clock, I1:$reset, BoolAttr:$async);
   let results = (outs I1:$result);
   let assemblyFormat = [{
     $clock `,` custom<KeywordBool>($async, "\"async\"", "\"sync\"")

test/Dialect/Verif/basic.mlir

@@ -133,7 +133,7 @@ hw.module @foo() {
 }
 
 // CHECK-LABEL: hw.module @HasBeenReset
-hw.module @HasBeenReset(in %clock: i1, in %reset: i1) {
+hw.module @HasBeenReset(in %clock: !seq.clock, in %reset: i1) {
   // CHECK-NEXT: verif.has_been_reset %clock, async %reset
   // CHECK-NEXT: verif.has_been_reset %clock, sync %reset
   %hbr0 = verif.has_been_reset %clock, async %reset

test/Dialect/Verif/canonicalization.mlir

@@ -1,7 +1,7 @@
 // RUN: circt-opt --canonicalize %s | FileCheck %s
 
 // CHECK-LABEL: @HasBeenReset
-hw.module @HasBeenReset(in %clock: i1, in %reset: i1) {
+hw.module @HasBeenReset(in %clock: !seq.clock, in %reset: i1) {
   // CHECK-NEXT: %false = hw.constant false
   // CHECK-NEXT: %true = hw.constant true
   %false = hw.constant false
@@ -37,21 +37,21 @@ hw.module @HasBeenReset(in %clock: i1, in %reset: i1) {
 }
 
 // CHECK-LABEL: @clockedAssert
-hw.module @clockedAssert(in %clock : i1, in %a : i1, in %en : i1) {
+hw.module @clockedAssert(in %clock : !seq.clock, in %a : i1, in %en : i1) {
   // CHECK: verif.clocked_assert %a if %en, posedge %clock : i1
   %clk = ltl.clock %a, posedge %clock : i1
   verif.assert %clk if %en : !ltl.sequence
 }
 
 // CHECK-LABEL: @clockedAssume
-hw.module @clockedAssume(in %clock : i1, in %a : i1, in %en : i1) {
+hw.module @clockedAssume(in %clock : !seq.clock, in %a : i1, in %en : i1) {
   // CHECK: verif.clocked_assume %a if %en, posedge %clock : i1
   %clk = ltl.clock %a, posedge %clock : i1
   verif.assume %clk if %en : !ltl.sequence
 }
 
 // CHECK-LABEL: @clockedCover
-hw.module @clockedCover(in %clock : i1, in %a : i1, in %en : i1) {
+hw.module @clockedCover(in %clock : !seq.clock, in %a : i1, in %en : i1) {
   // CHECK: verif.clocked_cover %a if %en,  posedge %clock : i1
   %clk = ltl.clock %a, posedge %clock : i1
   verif.cover %clk if %en : !ltl.sequence

test/Dialect/Verif/verify.mlir

@@ -2,7 +2,7 @@
 
 // -----
 
-hw.module @verifyClocks(in %clk: i1, in %a: i1, in %b: i1) {
+hw.module @verifyClocks(in %clk: !seq.clock, in %a: i1, in %b: i1) {
   %n0 = ltl.not %a : i1
 
   // expected-error @below {{Nested clock or disable operations are not allowed for clock_assertlike operations.}}
@@ -12,7 +12,7 @@ hw.module @verifyClocks(in %clk: i1, in %a: i1, in %b: i1) {
 
 // -----
 
-hw.module @verifyClocks1(in %clk: i1, in %a: i1, in %b: i1) {
+hw.module @verifyClocks1(in %clk: !seq.clock, in %a: i1, in %b: i1) {
   %n0 = ltl.not %a : i1
 
   // expected-error @below {{Nested clock or disable operations are not allowed for clock_assertlike operations.}}
@@ -22,7 +22,7 @@ hw.module @verifyClocks1(in %clk: i1, in %a: i1, in %b: i1) {
 
 // -----
 
-hw.module @verifyClocks2(in %clk: i1, in %a: i1, in %b: i1) {
+hw.module @verifyClocks2(in %clk: !seq.clock, in %a: i1, in %b: i1) {
   %n0 = ltl.not %a : i1
 
   // expected-error @below {{Nested clock or disable operations are not allowed for clock_assertlike operations.}}
@@ -32,7 +32,7 @@ hw.module @verifyClocks2(in %clk: i1, in %a: i1, in %b: i1) {
 
 // -----
 
-hw.module @deeplynested(in %clk: i1, in %a: i1, in %b: i1) {
+hw.module @deeplynested(in %clk: !seq.clock, in %a: i1, in %b: i1) {
   %n0 = ltl.not %a : i1
   // expected-error @below {{Nested clock or disable operations are not allowed for clock_assertlike operations.}}
   %clocked = ltl.clock %n0, posedge %clk : !ltl.property
@@ -47,6 +47,6 @@ hw.module @deeplynested(in %clk: i1, in %a: i1, in %b: i1) {
 
 // -----
 
-hw.module @clockedarg(in %clocked: !ltl.property, in %a: i1, in %clk: i1) {
+hw.module @clockedarg(in %clocked: !ltl.property, in %a: i1, in %clk: !seq.clock) {
   verif.clocked_assert %clocked if %a, posedge %clk : !ltl.property
 }