[circt-bmc] Add circt-bmc tool (#7621)

Co-authored-by: Martin Erhart <[email protected]>

integration_test/CMakeLists.txt

@@ -9,6 +9,7 @@ set(CIRCT_INTEGRATION_TEST_DEPENDS
   circt-translate
   circt-rtl-sim
   circt-lec
+  circt-bmc
   firtool
   hlstool
   ibistool

integration_test/circt-bmc/comb-errors.mlir

@@ -0,0 +1,15 @@
+// REQUIRES: libz3
+// REQUIRES: circt-bmc-jit
+
+//  RUN: circt-bmc %s -b 10 --module OrEqAnd --shared-libs=%libz3 | FileCheck %s --check-prefix=OREQAND
+//  OREQAND: Assertion can be violated!
+
+module {
+  hw.module @OrEqAnd(in %i0: i1, in %i1: i1) {
+    %or = comb.or bin %i0, %i1 : i1
+    %and = comb.and bin %i0, %i1 : i1
+    // Condition
+    %cond = comb.icmp bin eq %or, %and : i1
+    verif.assert %cond : i1
+  }
+}

integration_test/circt-bmc/comb.mlir

@@ -0,0 +1,28 @@
+// REQUIRES: libz3
+// REQUIRES: circt-bmc-jit
+
+//  RUN: circt-bmc %s -b 10 --module OrCommutes --shared-libs=%libz3 | FileCheck %s --check-prefix=ORCOMMUTES
+//  ORCOMMUTES: Bound reached with no violations!
+
+hw.module @OrCommutes(in %i0: i1, in %i1: i1) {
+  %or0 = comb.or bin %i0, %i1 : i1
+  %or1 = comb.or bin %i1, %i0 : i1
+  // Condition
+  %cond = comb.icmp bin eq %or0, %or1 : i1
+  verif.assert %cond : i1
+}
+
+//  RUN: circt-bmc %s -b 10 --module demorgan --shared-libs=%libz3 | FileCheck %s --check-prefix=DEMORGAN
+//  DEMORGAN: Bound reached with no violations!
+
+hw.module @demorgan(in %i0: i1, in %i1: i1) {
+  %c1 = hw.constant 1 : i1
+  %ni0 = comb.xor bin %i0, %c1 : i1
+  %ni1 = comb.xor bin %i1, %c1 : i1
+  %or = comb.or bin %ni0, %ni1 : i1
+  // Condition
+  %and = comb.and bin %i0, %i1 : i1
+  %nand = comb.xor bin %and, %c1 : i1
+  %cond = comb.icmp bin eq %or, %nand : i1
+  verif.assert %cond : i1
+}

integration_test/circt-bmc/seq-errors.mlir

@@ -0,0 +1,19 @@
+// REQUIRES: libz3
+// REQUIRES: circt-bmc-jit
+
+//  RUN: circt-bmc %s -b 10 --module Counter --shared-libs=%libz3 | FileCheck %s --check-prefix=COUNTER
+//  COUNTER: Assertion can be violated!
+
+hw.module @Counter(in %clk: !seq.clock, out count: i2) {
+  %c1_i2 = hw.constant 1 : i2
+  %regPlusOne = comb.add %reg, %c1_i2 : i2
+  %reg = seq.compreg %regPlusOne, %clk : i2
+  // Condition - count should never reach 3 (deliberately not true)
+  // FIXME: add an initial condition here once we support them, currently it
+  // can be violated on the first cycle as 3 is a potential initial value.
+  // Can also use this to check bounds are behaving as expected.
+  %c3_i2 = hw.constant 3 : i2
+  %lt = comb.icmp ult %reg, %c3_i2 : i2
+  verif.assert %lt : i1
+  hw.output %reg : i2
+}

integration_test/circt-bmc/seq.mlir

@@ -0,0 +1,34 @@
+// REQUIRES: libz3
+// REQUIRES: circt-bmc-jit
+
+//  RUN: circt-bmc %s -b 10 --module ClkProp --shared-libs=%libz3 | FileCheck %s --check-prefix=CLKPROP
+//  CLKPROP: Bound reached with no violations!
+
+hw.module @ClkProp(in %clk: !seq.clock, in %i0: i1) {
+  %reg = seq.compreg %i0, %clk : i1
+  // Condition (equivalent to %clk -> %reg == %i0)
+  %c-1_i1 = hw.constant -1 : i1
+  %clk_i1 = seq.from_clock %clk
+  %nclk = comb.xor bin %clk_i1, %c-1_i1 : i1
+  %eq = comb.icmp bin eq %i0, %reg : i1
+  %imp = comb.or bin %nclk, %eq : i1
+  verif.assert %imp : i1
+}
+
+// Check propagation of state through comb ops
+
+//  RUN: circt-bmc %s -b 10 --module StateProp --shared-libs=%libz3 | FileCheck %s --check-prefix=STATEPROP
+//  STATEPROP: Bound reached with no violations!
+
+hw.module @StateProp(in %clk: !seq.clock, in %i0: i1) {
+  %c-1_i1 = hw.constant -1 : i1
+  %reg = seq.compreg %i0, %clk : i1
+  %not_reg = comb.xor bin %reg, %c-1_i1 : i1
+  %not_not_reg = comb.xor bin %not_reg, %c-1_i1 : i1
+  // Condition (equivalent to %clk -> %reg == %not_not_reg)
+  %clk_i1 = seq.from_clock %clk
+  %nclk = comb.xor bin %clk_i1, %c-1_i1 : i1
+  %eq = comb.icmp bin eq %not_not_reg, %reg : i1
+  %imp = comb.or bin %nclk, %eq : i1
+  verif.assert %imp : i1
+}

integration_test/lit.cfg.py

@@ -79,7 +79,8 @@
 ]
 tools = [
     'arcilator', 'circt-opt', 'circt-translate', 'firtool', 'circt-rtl-sim.py',
-    'equiv-rtl.sh', 'handshake-runner', 'hlstool', 'ibistool', 'circt-lec'
+    'equiv-rtl.sh', 'handshake-runner', 'hlstool', 'ibistool', 'circt-lec',
+    'circt-bmc'
 ]
 
 # Enable python if its path was configured
@@ -216,6 +217,7 @@
 if config.mlir_enable_execution_engine:
   config.available_features.add('mlir-cpu-runner')
   config.available_features.add('circt-lec-jit')
+  config.available_features.add('circt-bmc-jit')
   tools.append('mlir-cpu-runner')
 
 # Add circt-verilog if the Slang frontend is enabled.

tools/CMakeLists.txt

@@ -1,5 +1,6 @@
 add_subdirectory(arcilator)
 add_subdirectory(circt-as)
+add_subdirectory(circt-bmc)
 add_subdirectory(circt-cocotb-driver)
 add_subdirectory(circt-dis)
 add_subdirectory(circt-lec)

tools/circt-bmc/CMakeLists.txt

@@ -0,0 +1,40 @@
+if(MLIR_ENABLE_EXECUTION_ENGINE)
+  add_compile_definitions(CIRCT_BMC_ENABLE_JIT)
+  set(CIRCT_BMC_JIT_LLVM_COMPONENTS native)
+  set(CIRCT_BMC_JIT_DEPS
+    MLIRExecutionEngine
+    MLIRExecutionEngineUtils
+  )
+endif()
+
+set(LLVM_LINK_COMPONENTS Support ${CIRCT_BMC_JIT_LLVM_COMPONENTS})
+
+add_circt_tool(circt-bmc circt-bmc.cpp)
+target_link_libraries(circt-bmc
+  PRIVATE
+  CIRCTBMCTransforms
+  CIRCTSMTToZ3LLVM
+  CIRCTHWToSMT
+  CIRCTCombToSMT
+  CIRCTVerifToSMT
+  CIRCTComb
+  CIRCTHW
+  CIRCTSeq
+  CIRCTSMT
+  CIRCTVerif
+  CIRCTSupport
+  MLIRIR
+  MLIRFuncDialect
+  MLIRArithDialect
+  MLIRLLVMIRTransforms
+  MLIRLLVMToLLVMIRTranslation
+  MLIRTargetLLVMIRExport
+  MLIRFuncInlinerExtension
+  MLIRBuiltinToLLVMIRTranslation
+  LLVMSupport
+
+  ${CIRCT_BMC_JIT_DEPS}
+)
+
+llvm_update_compile_flags(circt-bmc)
+mlir_check_all_link_libraries(circt-bmc)