smt: refactor SMT expression library (#2347)

4 files changed, 15 insertions, 17 deletions

diff --git a/src/test/scala/firrtl/backends/experimental/smt/Btor2Spec.scala b/src/test/scala/firrtl/backends/experimental/smt/Btor2Spec.scala
index fdd51a37..21e8289e 100644
--- a/src/test/scala/firrtl/backends/experimental/smt/Btor2Spec.scala
+++ b/src/test/scala/firrtl/backends/experimental/smt/Btor2Spec.scala
@@ -26,9 +26,8 @@ class Btor2Spec extends AnyFlatSpec {
         |5 output 4 ; b
         |6 sort bitvec 1
         |7 uext 3 2 8
-        |8 eq 6 7 4
-        |9 not 6 8
-        |10 bad 9 ; a_eq_b
+        |8 neq 6 7 4
+        |9 bad 8 ; a_eq_b
         |""".stripMargin
 
     assert(SMTBackendHelpers.toBotr2Str(src) == expected)
@@ -46,17 +45,16 @@ class Btor2Spec extends AnyFlatSpec {
         |""".stripMargin
 
     val expected =
-      """; @ module 0:0
+      """; @[module 0:0]
         |1 sort bitvec 8
-        |2 input 1 a ; @ a 0:0
+        |2 input 1 a ; @[a 0:0]
         |3 sort bitvec 16
         |4 uext 3 2 8
-        |5 output 4 ; b @ b 0:0, b_a 0:0
+        |5 output 4 ; b @[b 0:0], @[b_a 0:0]
         |6 sort bitvec 1
         |7 uext 3 2 8
-        |8 eq 6 7 4
-        |9 not 6 8
-        |10 bad 9 ; assert_0 @ assert 0:0
+        |8 neq 6 7 4
+        |9 bad 8 ; assert_0 @[assert 0:0]
         |""".stripMargin
 
     assert(SMTBackendHelpers.toBotr2Str(src) == expected)
diff --git a/src/test/scala/firrtl/backends/experimental/smt/FirrtlModuleToTransitionSystemSpec.scala b/src/test/scala/firrtl/backends/experimental/smt/FirrtlModuleToTransitionSystemSpec.scala
index c100da56..1fd0e99b 100644
--- a/src/test/scala/firrtl/backends/experimental/smt/FirrtlModuleToTransitionSystemSpec.scala
+++ b/src/test/scala/firrtl/backends/experimental/smt/FirrtlModuleToTransitionSystemSpec.scala
@@ -94,8 +94,7 @@ class FirrtlModuleToTransitionSystemSpec extends AnyFlatSpec {
     assert(sym.indexWidth == 5)
     assert(sym.dataWidth == 8)
     assert(m.init.isEmpty)
-    //assert(m.next.get.toString.contains("m[m.w.addr := m.w.data]"))
-    assert(m.next.get.toString == "m[m.w.addr := m.w.data]")
+    assert(m.next.get.toString.contains("m[m.w.addr := m.w.data]"))
   }
 
   it should "support scalar initialization of a memory to 0" in {
@@ -170,7 +169,8 @@ class FirrtlModuleToTransitionSystemSpec extends AnyFlatSpec {
         |""".stripMargin
     val sys = SMTBackendHelpers.toSys(src)
     assert(sys.inputs.isEmpty, "Clock inputs should be ignored.")
-    assert(sys.outputs.isEmpty, "Clock outputs should be ignored.")
+    val outputs = sys.signals.filter(_.lbl == IsOutput)
+    assert(outputs.isEmpty, "Clock outputs should be ignored.")
     assert(sys.signals.isEmpty, "Connects of clock type should be ignored.")
   }
 
diff --git a/src/test/scala/firrtl/backends/experimental/smt/SMTBackendHelpers.scala b/src/test/scala/firrtl/backends/experimental/smt/SMTBackendHelpers.scala
index 71d1d38c..8f4486ab 100644
--- a/src/test/scala/firrtl/backends/experimental/smt/SMTBackendHelpers.scala
+++ b/src/test/scala/firrtl/backends/experimental/smt/SMTBackendHelpers.scala
@@ -38,7 +38,7 @@ private object SMTBackendHelpers {
     val circuit = if (modelUndef) compileUndef(src) else compile(src)
     val module = circuit.modules.find(_.name == mod).get.asInstanceOf[ir.Module]
     // println(module.serialize)
-    new ModuleToTransitionSystem().run(module, presetRegs = presetRegs, memInit = memInit)
+    new ModuleToTransitionSystem(presetRegs = presetRegs, memInit = memInit, uninterpreted = Map()).run(module)
   }
 
   def toBotr2(src: String, mod: String = "m"): Iterable[String] =
diff --git a/src/test/scala/firrtl/backends/experimental/smt/SMTLibSpec.scala b/src/test/scala/firrtl/backends/experimental/smt/SMTLibSpec.scala
index 338d760c..4d96631e 100644
--- a/src/test/scala/firrtl/backends/experimental/smt/SMTLibSpec.scala
+++ b/src/test/scala/firrtl/backends/experimental/smt/SMTLibSpec.scala
@@ -47,16 +47,16 @@ class SMTLibSpec extends AnyFlatSpec {
         |""".stripMargin
 
     val expected =
-      """; @ module 0:0
+      """; @[module 0:0]
         |(declare-sort m_s 0)
         |; firrtl-smt2-input a 8
-        |; @ a 0:0
+        |; @[a 0:0]
         |(declare-fun a_f (m_s) (_ BitVec 8))
         |; firrtl-smt2-output b 16
-        |; @ b 0:0, b_a 0:0
+        |; @[b 0:0], @[b_a 0:0]
         |(define-fun b_f ((state m_s)) (_ BitVec 16) ((_ zero_extend 8) (a_f state)))
         |; firrtl-smt2-assert assert_0 1
-        |; @ assert 0:0
+        |; @[assert 0:0]
         |(define-fun assert_0_f ((state m_s)) Bool (= ((_ zero_extend 8) (a_f state)) (b_f state)))
         |(define-fun m_t ((state m_s) (state_n m_s)) Bool true)
         |(define-fun m_i ((state m_s)) Bool true)