[VerifToSMT] Only update registers on clock posedge (#7878)

llvm · Nov 25, 2024 · c690c9d · c690c9d
1 parent 87d10b7
commit c690c9d
Show file tree

Hide file tree

Showing 3 changed files with 73 additions and 5 deletions.
diff --git a/lib/Conversion/VerifToSMT/VerifToSMT.cpp b/lib/Conversion/VerifToSMT/VerifToSMT.cpp
@@ -342,8 +342,35 @@ 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);
+          }
 
           // Add the rest of the loop state args
           for (; loopIndex < loopVals.size(); ++loopIndex)
@@ -398,8 +425,20 @@ void ConvertVerifToSMTPass::runOnOperation() {
   // issues with whether assertions are/aren't lowered yet)
   SymbolTable symbolTable(getOperation());
   WalkResult assertionCheck = getOperation().walk(
-      [&](Operation *op) { // Check there is exactly one assertion
-        if (isa<verif::BoundedModelCheckingOp>(op)) {
+      [&](Operation *op) { // Check there is exactly one assertion and clock
+        if (auto bmcOp = dyn_cast<verif::BoundedModelCheckingOp>(op)) {
+          // Check only one clock is present in the circuit inputs
+          auto numClockArgs = 0;
+          for (auto argType : bmcOp.getCircuit().getArgumentTypes())
+            if (isa<seq::ClockType>(argType))
+              numClockArgs++;
+          // TODO: this can be removed once we have a way to associate reg
+          // ins/outs with clocks
+          if (numClockArgs > 1) {
+            op->emitError(
+                "only modules with one or zero clocks are currently supported");
+            signalPassFailure();
+          }
           SmallVector<mlir::Operation *> worklist;
           int numAssertions = 0;
           op->walk([&](Operation *curOp) {

diff --git a/test/Conversion/VerifToSMT/verif-to-smt-errors.mlir b/test/Conversion/VerifToSMT/verif-to-smt-errors.mlir
@@ -98,3 +98,27 @@ 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 or zero clocks are currently supported}}
+  %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
+}
diff --git a/test/Conversion/VerifToSMT/verif-to-smt.mlir b/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]]