From ee46579ee8c45ba0d0f4003f4f930c397ce04c34 Mon Sep 17 00:00:00 2001 From: markram1729 Date: Sat, 30 Aug 2025 10:46:03 +0530 Subject: [PATCH] fix : Verif CLock I1 to !seq.clock --- include/circt/Dialect/Verif/VerifOps.td | 8 +++----- test/Dialect/Verif/basic.mlir | 2 +- test/Dialect/Verif/canonicalization.mlir | 8 ++++---- test/Dialect/Verif/verify.mlir | 10 +++++----- 4 files changed, 13 insertions(+), 15 deletions(-) diff --git a/include/circt/Dialect/Verif/VerifOps.td b/include/circt/Dialect/Verif/VerifOps.td index 3cfbe7a37764..8d779159a57d 100644 --- a/include/circt/Dialect/Verif/VerifOps.td +++ b/include/circt/Dialect/Verif/VerifOps.td @@ -71,10 +71,8 @@ def ClockEdgeAttr : I32EnumAttr<"ClockEdge", "clock edge", class ClockedAssertLikeOp traits = []> : VerifOp { - let arguments = (ins LTLAnyPropertyType:$property, - ClockEdgeAttr:$edge, I1:$clock, - Optional:$enable, - OptionalAttr:$label); + let arguments = (ins LTLAnyPropertyType:$property, ClockEdgeAttr:$edge, + ClockType:$clock, Optional:$enable, OptionalAttr:$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($async, "\"async\"", "\"sync\"") diff --git a/test/Dialect/Verif/basic.mlir b/test/Dialect/Verif/basic.mlir index 26a4c2f4afa5..45cb631888ea 100644 --- a/test/Dialect/Verif/basic.mlir +++ b/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 diff --git a/test/Dialect/Verif/canonicalization.mlir b/test/Dialect/Verif/canonicalization.mlir index a69a47e879b5..b3e51f72bb59 100644 --- a/test/Dialect/Verif/canonicalization.mlir +++ b/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 diff --git a/test/Dialect/Verif/verify.mlir b/test/Dialect/Verif/verify.mlir index 3ae83b09d5fa..d8d58cec8574 100644 --- a/test/Dialect/Verif/verify.mlir +++ b/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 }