[VerifToSMT] Only update registers on clock posedge

lib/Conversion/VerifToSMT/VerifToSMT.cpp

@@ -274,6 +274,16 @@ struct VerifBoundedModelCheckingOpConversion
       }
     }
 
+    // TODO: this can be removed once we have a way to associate reg ins/outs
+    // with clocks
+    if (clockIndexes.size() > 1)
+      return op->emitError(
+          "only modules with one clock are currently supported");
+
+    // If we have no clocks then num_regs has to be 0
+    if (clockIndexes.size() == 0 && numRegs != 0)
+      return op->emitError("num_regs is non-zero but found no clock");
+
     auto numStateArgs = initVals.size() - initIndex;
     // Add the rest of the init vals (state args)
     for (; initIndex < initVals.size(); ++initIndex)
@@ -342,8 +352,37 @@ struct VerifBoundedModelCheckingOpConversion
             else
               newDecls.push_back(builder.create<smt::DeclareFunOp>(loc, newTy));
           }
-          newDecls.append(
-              SmallVector<Value>(circuitCallOuts.take_back(numRegs)));
+
+          // Only update the registers on a clock posedge
+          // TODO: this will also need changing with multiple clocks - currently
+          // it only accounts for the one clock case.
+          if (clockIndexes.size() == 1) {
+            auto clockIndex = clockIndexes[0];
+            auto oldClock = iterArgs[clockIndex];
+            auto newClock = loopVals[clockIndex];
+            auto oldClockLow = builder.create<smt::BVNotOp>(loc, oldClock);
+            auto isPosedgeBV =
+                builder.create<smt::BVAndOp>(loc, oldClockLow, newClock);
+            // Convert posedge bv<1> to bool
+            auto trueBV = builder.create<smt::BVConstantOp>(loc, 1, 1);
+            auto isPosedge =
+                builder.create<smt::EqOp>(loc, isPosedgeBV, trueBV);
+            auto regStates =
+                iterArgs.take_front(circuitFuncOp.getNumArguments())
+                    .take_back(numRegs);
+            auto regInputs = circuitCallOuts.take_back(numRegs);
+            SmallVector<Value> nextRegStates;
+            for (auto [regState, regInput] : llvm::zip(regStates, regInputs)) {
+              // Create an ITE to calculate the next reg state
+              // TODO: we create a lot of ITEs here that will slow things down -
+              // these could be avoided by making init/loop regions concrete
+              nextRegStates.push_back(builder.create<smt::IteOp>(
+                  loc, isPosedge, regInput, regState));
+            }
+            newDecls.append(nextRegStates);
+          }
+          // We don't need to worry about the else case as we asserted above
+          // that it means num_regs is 0
 
           // Add the rest of the loop state args
           for (; loopIndex < loopVals.size(); ++loopIndex)

test/Conversion/VerifToSMT/verif-to-smt-errors.mlir

@@ -98,3 +98,46 @@ hw.module @TwoAssertions(in %x: i1, in %y: i1) {
   verif.assert %x : i1
   verif.assert %y : i1
 }
+
+// -----
+
+func.func @multiple_clocks() -> (i1) {
+  // expected-error @below {{only modules with one clock are currently supported}}
+  // expected-error @below {{failed to legalize operation 'verif.bmc' that was explicitly marked illegal}}
+  %bmc = verif.bmc bound 10 num_regs 1 initial_values [unit]
+  init {
+    %c0_i1 = hw.constant 0 : i1
+    %clk = seq.to_clock %c0_i1
+    verif.yield %clk, %clk : !seq.clock, !seq.clock
+  }
+  loop {
+    ^bb0(%clock0: !seq.clock, %clock1: !seq.clock):
+    verif.yield %clock0, %clock1 : !seq.clock, !seq.clock
+  }
+  circuit {
+  ^bb0(%clock0: !seq.clock, %clock1: !seq.clock, %arg0: i32):
+    %c1_i32 = hw.constant 1 : i32
+    %cond1 = comb.icmp ugt %arg0, %c1_i32 : i32
+    verif.assert %cond1 : i1
+    verif.yield %arg0 : i32
+  }
+  func.return %bmc : i1
+}
+
+// -----
+
+func.func @regs_but_no_blocks() -> (i1) {
+  // expected-error @below {{num_regs is non-zero but found no clock}}
+  // expected-error @below {{failed to legalize operation 'verif.bmc' that was explicitly marked illegal}}
+  %bmc = verif.bmc bound 10 num_regs 1 initial_values [unit]
+  init {}
+  loop {}
+  circuit {
+  ^bb0(%arg0: i32):
+    %c1_i32 = hw.constant 1 : i32
+    %cond1 = comb.icmp ugt %arg0, %c1_i32 : i32
+    verif.assert %cond1 : i1
+    verif.yield %arg0 : i32
+  }
+  func.return %bmc : i1
+}

test/Conversion/VerifToSMT/verif-to-smt.mlir

@@ -109,7 +109,12 @@ func.func @test_lec(%arg0: !smt.bv<1>) -> (i1, i1, i1) {
 // CHECK:        [[ORI:%.+]] = arith.ori [[SMTCHECK]], [[ARG5]]
 // CHECK:        [[LOOP:%.+]]:2 = func.call @bmc_loop([[ARG1]], [[ARG4]])
 // CHECK:        [[F2:%.+]] = smt.declare_fun : !smt.bv<32>
-// CHECK:        scf.yield [[LOOP]]#0, [[F2]], [[CIRCUIT]]#1, [[LOOP]]#1, [[ORI]]
+// CHECK:        [[OLDCLOCKLOW:%.+]] = smt.bv.not %arg1
+// CHECK:        [[BVPOSEDGE:%.+]] = smt.bv.and [[OLDCLOCKLOW]], [[LOOP]]#0
+// CHECK:        [[BVTRUE:%.+]] = smt.bv.constant #smt.bv<-1> : !smt.bv<1>
+// CHECK:        [[BOOLPOSEDGE:%.+]] = smt.eq [[BVPOSEDGE]], [[BVTRUE]]
+// CHECK:        [[NEWREG:%.+]] = smt.ite [[BOOLPOSEDGE]], [[CIRCUIT]]#1, [[ARG3]]
+// CHECK:        scf.yield [[LOOP]]#0, [[F2]], [[NEWREG]], [[LOOP]]#1, [[ORI]]
 // CHECK:      }
 // CHECK:      [[XORI:%.+]] = arith.xori [[FOR]]#4, [[TRUE]]
 // CHECK:      smt.yield [[XORI]]