[Verif] Require a clock when num_regs is non-zero on a BMC op (#7891)

llvm · Nov 25, 2024 · 83b5ff3 · 83b5ff3
1 parent c690c9d
commit 83b5ff3
Show file tree

Hide file tree

Showing 3 changed files with 31 additions and 6 deletions.
diff --git a/lib/Dialect/Verif/VerifOps.cpp b/lib/Dialect/Verif/VerifOps.cpp
@@ -143,6 +143,9 @@ LogicalResult BoundedModelCheckingOp::verifyRegions() {
                 "there are clock arguments in the circuit region "
                 "before any other values";
   }
+  if (getNumRegs() > 0 && totalClocks == 0)
+    return emitOpError("num_regs is non-zero, but the circuit region has no "
+                       "clock inputs to clock the registers");
   auto initialValues = getInitialValues();
   if (initialValues.size() != getNumRegs()) {
     return emitOpError()

diff --git a/test/Conversion/VerifToSMT/verif-to-smt-errors.mlir b/test/Conversion/VerifToSMT/verif-to-smt-errors.mlir
@@ -20,7 +20,7 @@ func.func @assert_with_unsupported_property_type(%arg0: !smt.bv<1>) {
 
 func.func @multiple_assertions_bmc() -> (i1) {
   // expected-error @below {{bounded model checking problems with multiple assertions are not yet correctly handled - instead, you can assert the conjunction of your assertions}}
-  %bmc = verif.bmc bound 10 num_regs 1 initial_values [unit]
+  %bmc = verif.bmc bound 10 num_regs 0 initial_values []
   init {}
   loop {}
   circuit {
@@ -40,7 +40,7 @@ func.func @multiple_assertions_bmc() -> (i1) {
 
 func.func @multiple_asserting_modules_bmc() -> (i1) {
   // expected-error @below {{bounded model checking problems with multiple assertions are not yet correctly handled - instead, you can assert the conjunction of your assertions}}
-  %bmc = verif.bmc bound 10 num_regs 1 initial_values [unit]
+  %bmc = verif.bmc bound 10 num_regs 0 initial_values []
   init {}
   loop {}
   circuit {
@@ -61,7 +61,7 @@ hw.module @OneAssertion(in %x: i1) {
 
 func.func @two_separated_assertions() -> (i1) {
   // expected-error @below {{bounded model checking problems with multiple assertions are not yet correctly handled - instead, you can assert the conjunction of your assertions}}
-  %bmc = verif.bmc bound 10 num_regs 1 initial_values [unit]
+  %bmc = verif.bmc bound 10 num_regs 0 initial_values []
   init {}
   loop {}
   circuit {
@@ -82,7 +82,7 @@ hw.module @OneAssertion(in %x: i1) {
 
 func.func @multiple_nested_assertions() -> (i1) {
   // expected-error @below {{bounded model checking problems with multiple assertions are not yet correctly handled - instead, you can assert the conjunction of your assertions}}
-  %bmc = verif.bmc bound 10 num_regs 1 initial_values [unit]
+  %bmc = verif.bmc bound 10 num_regs 0 initial_values []
   init {}
   loop {}
   circuit {

diff --git a/test/Dialect/Verif/errors.mlir b/test/Dialect/Verif/errors.mlir
@@ -138,9 +138,14 @@ verif.bmc bound 10 num_regs 0 initial_values [unit] attributes {verif.some_attr}
 
 // expected-error @below {{number of initial values must match the number of registers}}
 verif.bmc bound 10 num_regs 1 initial_values [] attributes {verif.some_attr} init {
+  %clkInit = hw.constant false
+  %toClk = seq.to_clock %clkInit
+  verif.yield %toClk : !seq.clock
 } loop {
+^bb0(%clk1: !seq.clock):
+  verif.yield %clk1 : !seq.clock
 } circuit {
-^bb0(%arg0: i32):
+^bb0(%clk: !seq.clock, %arg0: i32):
   %false = hw.constant false
   // Arbitrary assertion so op verifies
   verif.assert %false : i1
@@ -151,11 +156,28 @@ verif.bmc bound 10 num_regs 1 initial_values [] attributes {verif.some_attr} ini
 
 // expected-error @below {{initial values must be integer or unit attributes}}
 verif.bmc bound 10 num_regs 1 initial_values ["foo"] attributes {verif.some_attr} init {
+  %clkInit = hw.constant false
+  %toClk = seq.to_clock %clkInit
+  verif.yield %toClk : !seq.clock
 } loop {
+^bb0(%clk1: !seq.clock):
+  verif.yield %clk1 : !seq.clock
 } circuit {
-^bb0(%arg0: i32):
+^bb0(%clk: !seq.clock, %arg0: i32):
   %false = hw.constant false
   // Arbitrary assertion so op verifies
   verif.assert %false : i1
   verif.yield %arg0 : i32
 }
+
+// -----
+
+// expected-error @below {{num_regs is non-zero, but the circuit region has no clock inputs to clock the registers}}
+verif.bmc bound 10 num_regs 1 initial_values [unit] attributes {verif.some_attr} init {
+} loop {
+} circuit {
+^bb0(%arg0: i32):
+  %true = hw.constant true
+  verif.assert %true : i1
+  verif.yield %arg0 : i32
+}