[firtool] Integrate AssertProperty lowering into BTOR2 pipeline (#6975)

* Add lowering for AssertProperty operations * removed nl at start of file * integrated ltl lowering into --btor2 * sorted cmake and removed unreachable branches * reordered cmake * cleaned up test * added pass registration
llvm · May 3, 2024 · 800209c · 800209c
1 parent 00036d7
commit 800209c
Show file tree

Hide file tree

Showing 4 changed files with 83 additions and 0 deletions.
diff --git a/lib/Firtool/CMakeLists.txt b/lib/Firtool/CMakeLists.txt
@@ -7,6 +7,7 @@ add_circt_library(CIRCTFirtool
   CIRCTFIRRTLToHW
   CIRCTFIRRTLTransforms
   CIRCTHWTransforms
+  CIRCTLTLToCore
   CIRCTOMTransforms
   CIRCTSeqToSV
   CIRCTSimToSV

diff --git a/lib/Firtool/Firtool.cpp b/lib/Firtool/Firtool.cpp
@@ -386,6 +386,7 @@ LogicalResult firtool::populateFinalizeIR(mlir::PassManager &pm,
 LogicalResult firtool::populateHWToBTOR2(mlir::PassManager &pm,
                                          const FirtoolOptions &opt,
                                          llvm::raw_ostream &os) {
+  pm.addNestedPass<hw::HWModuleOp>(circt::createLowerLTLToCorePass());
   pm.addNestedPass<hw::HWModuleOp>(circt::createConvertHWToBTOR2Pass(os));
   return success();
 }

diff --git a/test/firtool/btor2-assertproperty.fir b/test/firtool/btor2-assertproperty.fir
@@ -0,0 +1,80 @@
+; RUN: firtool --btor2 %s | FileCheck %s
+
+FIRRTL version 3.2.0
+circuit Counter :
+  intmodule HasBeenResetIntrinsic :
+    input clock : Clock
+    input reset : Reset
+    output out : UInt<1>
+    intrinsic = circt_has_been_reset
+
+  intmodule LTLDisableIntrinsic :
+    input in : UInt<1>
+    input condition : UInt<1>
+    output out : UInt<1>
+    intrinsic = circt_ltl_disable
+
+  intmodule LTLClockIntrinsic :
+    input in : UInt<1>
+    input clock : Clock
+    output out : UInt<1>
+    intrinsic = circt_ltl_clock
+
+  intmodule VerifAssertIntrinsic :
+    input property : UInt<1>
+    intrinsic = circt_verif_assert
+
+  module Counter :
+    input clock : Clock
+    input reset : UInt<1>
+
+    regreset count : UInt<32>, clock, reset, UInt<32>(0h0) 
+    node _T = eq(count, UInt<5>(0h16)) 
+    when _T :
+      connect count, UInt<1>(0h0) 
+    node _T_1 = neq(count, UInt<5>(0h16)) 
+    when _T_1 :
+      node _count_T = add(count, UInt<1>(0h1))
+      node _count_T_1 = tail(_count_T, 1) 
+      connect count, _count_T_1 
+    node _T_2 = neq(count, UInt<4>(0ha)) 
+    inst HasBeenResetIntrinsic of HasBeenResetIntrinsic 
+    connect HasBeenResetIntrinsic.clock, clock 
+    connect HasBeenResetIntrinsic.reset, reset 
+    node disable = eq(HasBeenResetIntrinsic.out, UInt<1>(0h0)) 
+    inst ltl_disable of LTLDisableIntrinsic
+    connect ltl_disable.in, _T_2 
+    connect ltl_disable.condition, disable 
+    inst ltl_clock of LTLClockIntrinsic
+    connect ltl_clock.in, ltl_disable.out 
+    connect ltl_clock.clock, clock
+    inst verif of VerifAssertIntrinsic
+    connect verif.property, ltl_clock.out 
+
+; CHECK:  1 sort bitvec 1
+; CHECK:  2 input 1 reset
+; CHECK:  3 sort bitvec 32
+; CHECK:  4 state 3 count
+; CHECK:  5 constd 1 0
+; CHECK:  6 state 1 hbr
+; CHECK:  7 init 1 6 5
+; CHECK:  8 constd 3 1
+; CHECK:  9 constd 3 10
+; CHECK:  10 constd 3 22
+; CHECK:  11 constd 1 -1
+; CHECK:  12 constd 3 0
+; CHECK:  13 eq 1 4 10
+; CHECK:  14 add 3 4 8
+; CHECK:  15 ite 3 13 12 14
+; CHECK:  16 neq 1 4 9
+; CHECK:  17 constd 1 -1
+; CHECK:  18 or 1 2 6
+; CHECK:  19 xor 1 2 17
+; CHECK:  20 and 1 6 19
+; CHECK:  21 xor 1 20 11
+; CHECK:  22 or 1 21 16
+; CHECK:  23 not 1 22
+; CHECK:  24 bad 23
+; CHECK:  25 ite 3 2 12 15
+; CHECK:  26 next 3 4 25
+; CHECK:  28 next 1 6 27
diff --git a/tools/firtool/firtool.cpp b/tools/firtool/firtool.cpp
@@ -725,6 +725,7 @@ int main(int argc, char **argv) {
     registerLowerSeqToSVPass();
     registerLowerSimToSVPass();
     registerLowerVerifToSVPass();
+    registerLowerLTLToCorePass();
     registerConvertHWToBTOR2Pass();
   }