From c690c9dcf2b095d8d99e9dad0474a814e229c2e2 Mon Sep 17 00:00:00 2001 From: Bea Healy <57840981+TaoBi22@users.noreply.github.com> Date: Mon, 25 Nov 2024 15:14:27 +0000 Subject: [PATCH] [VerifToSMT] Only update registers on clock posedge (#7878) --- lib/Conversion/VerifToSMT/VerifToSMT.cpp | 47 +++++++++++++++++-- .../VerifToSMT/verif-to-smt-errors.mlir | 24 ++++++++++ test/Conversion/VerifToSMT/verif-to-smt.mlir | 7 ++- 3 files changed, 73 insertions(+), 5 deletions(-) diff --git a/lib/Conversion/VerifToSMT/VerifToSMT.cpp b/lib/Conversion/VerifToSMT/VerifToSMT.cpp index 57ef512d1f2d..4384ea2d46f2 100644 --- a/lib/Conversion/VerifToSMT/VerifToSMT.cpp +++ b/lib/Conversion/VerifToSMT/VerifToSMT.cpp @@ -342,8 +342,35 @@ struct VerifBoundedModelCheckingOpConversion else newDecls.push_back(builder.create(loc, newTy)); } - newDecls.append( - SmallVector(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(loc, oldClock); + auto isPosedgeBV = + builder.create(loc, oldClockLow, newClock); + // Convert posedge bv<1> to bool + auto trueBV = builder.create(loc, 1, 1); + auto isPosedge = + builder.create(loc, isPosedgeBV, trueBV); + auto regStates = + iterArgs.take_front(circuitFuncOp.getNumArguments()) + .take_back(numRegs); + auto regInputs = circuitCallOuts.take_back(numRegs); + SmallVector 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( + 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(op)) { + [&](Operation *op) { // Check there is exactly one assertion and clock + if (auto bmcOp = dyn_cast(op)) { + // Check only one clock is present in the circuit inputs + auto numClockArgs = 0; + for (auto argType : bmcOp.getCircuit().getArgumentTypes()) + if (isa(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 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 index fed757844412..c64baea5a427 100644 --- 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 index 7d11138a4202..bd7260f0f941 100644 --- 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]]