smt: include firrtl statement names in SMT and btor2 output (#2270)

* smt: include firrtl statement names in SMT and btor2 output

* smt: remove println

* smt: make tests run again and fix stale ones

Apparently `private` classes aren't found by th sbt test runner.

6 files changed, 96 insertions, 169 deletions

diff --git a/src/main/scala/firrtl/backends/experimental/smt/FirrtlToTransitionSystem.scala b/src/main/scala/firrtl/backends/experimental/smt/FirrtlToTransitionSystem.scala
index cfab61b9..78ad3c80 100644
--- a/src/main/scala/firrtl/backends/experimental/smt/FirrtlToTransitionSystem.scala
+++ b/src/main/scala/firrtl/backends/experimental/smt/FirrtlToTransitionSystem.scala
@@ -14,7 +14,7 @@ import firrtl.passes.PassException
 import firrtl.passes.memlib.VerilogMemDelays
 import firrtl.stage.Forms
 import firrtl.stage.TransformManager.TransformDependency
-import firrtl.transforms.{DeadCodeElimination, PropagatePresetAnnotations}
+import firrtl.transforms.{DeadCodeElimination, EnsureNamedStatements, PropagatePresetAnnotations}
 import firrtl.{
   ir,
   CircuitState,
@@ -63,7 +63,12 @@ object FirrtlToTransitionSystem extends Transform with DependencyAPIMigration {
   // TODO: We also would like to run some optimization passes, but RemoveValidIf won't allow us to model DontCare
   //       precisely and PadWidths emits ill-typed firrtl.
   override def prerequisites: Seq[Dependency[Transform]] = Forms.LowForm ++
-    Seq(Dependency(InvalidToRandomPass), Dependency(UndefinedMemoryBehaviorPass), Dependency(VerilogMemDelays))
+    Seq(
+      Dependency(InvalidToRandomPass),
+      Dependency(UndefinedMemoryBehaviorPass),
+      Dependency(VerilogMemDelays),
+      Dependency(EnsureNamedStatements) // this is required to give assert/assume statements good names
+    )
   override def invalidates(a: Transform): Boolean = false
   // since this pass only runs on the main module, inlining needs to happen before
   override def optionalPrerequisites: Seq[TransformDependency] = Seq(Dependency[firrtl.passes.InlineInstances])
@@ -458,7 +463,7 @@ private class ModuleScanner(
       } else {
         insertDummyAssignsForUnusedOutputs(pred)
         insertDummyAssignsForUnusedOutputs(en)
-        val name = namespace.newName(msgToName(op.toString, msg.string))
+        val name = s.name
         val predicate = onExpression(pred)
         val enabled = onExpression(en)
         val e = BVImplies(enabled, predicate)
@@ -595,10 +600,6 @@ private class ModuleScanner(
     FirrtlExpressionSemantics.toSMT(e)
   }
 
-  private def msgToName(prefix: String, msg: String): String = {
-    // TODO: ensure that we can generate unique names
-    prefix + "_" + msg.replace(" ", "_").replace("|", "")
-  }
   private def error(msg:        String):  Unit = throw new RuntimeException(msg)
   private def isGroundType(tpe: ir.Type): Boolean = tpe.isInstanceOf[ir.GroundType]
   private def isClock(tpe:      ir.Type): Boolean = tpe == ir.ClockType
diff --git a/src/test/scala/firrtl/backends/experimental/smt/Btor2Spec.scala b/src/test/scala/firrtl/backends/experimental/smt/Btor2Spec.scala
index 32976d30..fdd51a37 100644
--- a/src/test/scala/firrtl/backends/experimental/smt/Btor2Spec.scala
+++ b/src/test/scala/firrtl/backends/experimental/smt/Btor2Spec.scala
@@ -2,7 +2,10 @@
 
 package firrtl.backends.experimental.smt
 
-private class Btor2Spec extends SMTBackendBaseSpec {
+import org.scalatest.flatspec.AnyFlatSpec
+
+class Btor2Spec extends AnyFlatSpec {
+  behavior.of("btor2 backend")
 
   it should "convert a hello world module" in {
     val src =
@@ -12,7 +15,7 @@ private class Btor2Spec extends SMTBackendBaseSpec {
         |    input a: UInt<8>
         |    output b: UInt<16>
         |    b <= a
-        |    assert(clock, eq(a, b), UInt(1), "")
+        |    assert(clock, eq(a, b), UInt(1), "") : a_eq_b
         |""".stripMargin
 
     val expected =
@@ -25,10 +28,10 @@ private class Btor2Spec extends SMTBackendBaseSpec {
         |7 uext 3 2 8
         |8 eq 6 7 4
         |9 not 6 8
-        |10 bad 9 ; assert_
+        |10 bad 9 ; a_eq_b
         |""".stripMargin
 
-    assert(toBotr2Str(src) == expected)
+    assert(SMTBackendHelpers.toBotr2Str(src) == expected)
   }
 
   it should "include FileInfo in the output" in {
@@ -53,9 +56,9 @@ private class Btor2Spec extends SMTBackendBaseSpec {
         |7 uext 3 2 8
         |8 eq 6 7 4
         |9 not 6 8
-        |10 bad 9 ; assert_ @ assert 0:0
+        |10 bad 9 ; assert_0 @ assert 0:0
         |""".stripMargin
 
-    assert(toBotr2Str(src) == expected)
+    assert(SMTBackendHelpers.toBotr2Str(src) == expected)
   }
 }
diff --git a/src/test/scala/firrtl/backends/experimental/smt/FirrtlExpressionSemanticsSpec.scala b/src/test/scala/firrtl/backends/experimental/smt/FirrtlExpressionSemanticsSpec.scala
index 5956cf03..6ce90eab 100644
--- a/src/test/scala/firrtl/backends/experimental/smt/FirrtlExpressionSemanticsSpec.scala
+++ b/src/test/scala/firrtl/backends/experimental/smt/FirrtlExpressionSemanticsSpec.scala
@@ -2,9 +2,11 @@
 
 package firrtl.backends.experimental.smt
 
-private class FirrtlExpressionSemanticsSpec extends SMTBackendBaseSpec {
+import org.scalatest.flatspec.AnyFlatSpec
 
-  def primop(op: String, resTpe: String, inTpes: Seq[String], consts: Seq[Int]): String = {
+class FirrtlExpressionSemanticsSpec extends AnyFlatSpec {
+
+  private def primopSys(op: String, resTpe: String, inTpes: Seq[String], consts: Seq[Int]): TransitionSystem = {
     val inputs = inTpes.zipWithIndex.map { case (tpe, ii) => s"    input i$ii : $tpe" }.mkString("\n")
     val args = (inTpes.zipWithIndex.map { case (_, ii) => s"i$ii" } ++ consts.map(_.toString)).mkString(", ")
     val src =
@@ -15,9 +17,27 @@ private class FirrtlExpressionSemanticsSpec extends SMTBackendBaseSpec {
          |    res <= $op($args)
          |
          |""".stripMargin
-    val sys = toSys(src)
-    assert(sys.signals.length == 1)
-    sys.signals.head.e.toString
+    SMTBackendHelpers.toSys(src)
+  }
+
+  def primop(op: String, resTpe: String, inTpes: Seq[String], consts: Seq[Int]): String = {
+    val sys = primopSys(op, resTpe, inTpes, consts)
+    assert(sys.signals.length >= 1)
+    sys.signals.last.e.toString
+  }
+
+  private def primopSys(
+    signed:            Boolean,
+    op:                String,
+    resWidth:          Int,
+    inWidth:           Seq[Int],
+    consts:            Seq[Int],
+    resAlwaysUnsigned: Boolean
+  ): TransitionSystem = {
+    val tpe = if (signed) "SInt" else "UInt"
+    val resTpe = if (resAlwaysUnsigned) "UInt" else tpe
+    val inTpes = inWidth.map(w => s"$tpe<$w>")
+    primopSys(op, s"$resTpe<$resWidth>", inTpes, consts)
   }
 
   def primop(
@@ -28,10 +48,9 @@ private class FirrtlExpressionSemanticsSpec extends SMTBackendBaseSpec {
     consts:            Seq[Int] = List(),
     resAlwaysUnsigned: Boolean = false
   ): String = {
-    val tpe = if (signed) "SInt" else "UInt"
-    val resTpe = if (resAlwaysUnsigned) "UInt" else tpe
-    val inTpes = inWidth.map(w => s"$tpe<$w>")
-    primop(op, s"$resTpe<$resWidth>", inTpes, consts)
+    val sys = primopSys(signed, op, resWidth, inWidth, consts, resAlwaysUnsigned)
+    assert(sys.signals.length >= 1)
+    sys.signals.last.e.toString
   }
 
   it should "correctly translate the add primitive operation with different operand sizes" in {
@@ -58,23 +77,26 @@ private class FirrtlExpressionSemanticsSpec extends SMTBackendBaseSpec {
 
   it should "correctly translate the `div` primitive operation" in {
     // division is a little bit more complicated because the result of division by zero is undefined
+    //val sys = primopSys(false, "div", 8, List(8, 8), List(), false)
+    //println(sys.serialize)
+
     assert(
       primop(false, "div", 8, List(8, 8)) ==
-        "ite(eq(i1, 8'b0), RANDOM.res, udiv(i0, i1))"
+        "ite(res_invalid_cond, res_invalid, udiv(i0, i1))"
     )
     assert(
       primop(false, "div", 8, List(8, 4)) ==
-        "ite(eq(i1, 4'b0), RANDOM.res, udiv(i0, zext(i1, 4)))"
+        "ite(res_invalid_cond, res_invalid, udiv(i0, zext(i1, 4)))"
     )
 
     // signed division increases result width by 1
     assert(
       primop(true, "div", 8, List(7, 7)) ==
-        "ite(eq(i1, 7'b0), RANDOM.res, sdiv(sext(i0, 1), sext(i1, 1)))"
+        "ite(res_invalid_cond, res_invalid, sdiv(sext(i0, 1), sext(i1, 1)))"
     )
     assert(
       primop(true, "div", 8, List(7, 4))
-        == "ite(eq(i1, 4'b0), RANDOM.res, sdiv(sext(i0, 1), sext(i1, 4)))"
+        == "ite(res_invalid_cond, res_invalid, sdiv(sext(i0, 1), sext(i1, 4)))"
     )
   }
 
@@ -173,8 +195,8 @@ private class FirrtlExpressionSemanticsSpec extends SMTBackendBaseSpec {
   }
 
   it should "correctly translate the `neg` primitive operation" in {
-    assert(primop(true, "neg", 4, List(3)) == "neg(sext(i0, 1))")
-    assert(primop("neg", "SInt<4>", List("UInt<3>"), List()) == "neg(zext(i0, 1))")
+    assert(primop(true, "neg", 4, List(3)) == "sub(sext(3'b0, 1), sext(i0, 1))")
+    assert(primop("neg", "SInt<4>", List("UInt<3>"), List()) == "sub(zext(3'b0, 1), zext(i0, 1))")
   }
 
   it should "correctly translate the `not` primitive operation" in {
diff --git a/src/test/scala/firrtl/backends/experimental/smt/FirrtlModuleToTransitionSystemSpec.scala b/src/test/scala/firrtl/backends/experimental/smt/FirrtlModuleToTransitionSystemSpec.scala
index a90e8506..7bc80102 100644
--- a/src/test/scala/firrtl/backends/experimental/smt/FirrtlModuleToTransitionSystemSpec.scala
+++ b/src/test/scala/firrtl/backends/experimental/smt/FirrtlModuleToTransitionSystemSpec.scala
@@ -3,8 +3,9 @@
 package firrtl.backends.experimental.smt
 
 import firrtl.{MemoryArrayInit, MemoryScalarInit, Utils}
+import org.scalatest.flatspec.AnyFlatSpec
 
-private class FirrtlModuleToTransitionSystemSpec extends SMTBackendBaseSpec {
+class FirrtlModuleToTransitionSystemSpec extends AnyFlatSpec {
   behavior.of("ModuleToTransitionSystem.run")
 
   it should "model registers as state" in {
@@ -24,7 +25,7 @@ private class FirrtlModuleToTransitionSystemSpec extends SMTBackendBaseSpec {
         |    out <= r
         |
         |""".stripMargin
-    val sys = toSys(src)
+    val sys = SMTBackendHelpers.toSys(src)
 
     assert(sys.signals.length == 2)
 
@@ -71,7 +72,7 @@ private class FirrtlModuleToTransitionSystemSpec extends SMTBackendBaseSpec {
        |""".stripMargin
 
   it should "model memories as state" in {
-    val sys = toSys(memCircuit())
+    val sys = SMTBackendHelpers.toSys(memCircuit())
 
     assert(sys.signals.length == 9 - 2 + 1, "9 connects - 2 clock connects + 1 combinatorial read port")
 
@@ -98,35 +99,35 @@ private class FirrtlModuleToTransitionSystemSpec extends SMTBackendBaseSpec {
   }
 
   it should "support scalar initialization of a memory to 0" in {
-    val sys = toSys(memCircuit(), memInit = Map("m" -> MemoryScalarInit(0)))
+    val sys = SMTBackendHelpers.toSys(memCircuit(), memInit = Map("m" -> MemoryScalarInit(0)))
     val m = sys.states.find(_.sym.name == "m").get
     assert(m.init.isDefined)
     assert(m.init.get.toString == "([8'b0] x 32)")
   }
 
   it should "support scalar initialization of a memory to 127" in {
-    val sys = toSys(memCircuit(31), memInit = Map("m" -> MemoryScalarInit(127)))
+    val sys = SMTBackendHelpers.toSys(memCircuit(31), memInit = Map("m" -> MemoryScalarInit(127)))
     val m = sys.states.find(_.sym.name == "m").get
     assert(m.init.isDefined)
     assert(m.init.get.toString == "([8'b1111111] x 32)")
   }
 
   it should "support array initialization of a memory to Seq(0, 1, 2, 3)" in {
-    val sys = toSys(memCircuit(4), memInit = Map("m" -> MemoryArrayInit(Seq(0, 1, 2, 3))))
+    val sys = SMTBackendHelpers.toSys(memCircuit(4), memInit = Map("m" -> MemoryArrayInit(Seq(0, 1, 2, 3))))
     val m = sys.states.find(_.sym.name == "m").get
     assert(m.init.isDefined)
     assert(m.init.get.toString == "([8'b0] x 4)[2'b1 := 8'b1][2'b10 := 8'b10][2'b11 := 8'b11]")
   }
 
   it should "support array initialization of a memory to Seq(1, 0, 1, 0)" in {
-    val sys = toSys(memCircuit(4), memInit = Map("m" -> MemoryArrayInit(Seq(1, 0, 1, 0))))
+    val sys = SMTBackendHelpers.toSys(memCircuit(4), memInit = Map("m" -> MemoryArrayInit(Seq(1, 0, 1, 0))))
     val m = sys.states.find(_.sym.name == "m").get
     assert(m.init.isDefined)
     assert(m.init.get.toString == "([8'b1] x 4)[2'b1 := 8'b0][2'b11 := 8'b0]")
   }
 
   it should "support array initialization of a memory to Seq(1, 0, 0, 0)" in {
-    val sys = toSys(memCircuit(4), memInit = Map("m" -> MemoryArrayInit(Seq(1, 0, 0, 0))))
+    val sys = SMTBackendHelpers.toSys(memCircuit(4), memInit = Map("m" -> MemoryArrayInit(Seq(1, 0, 0, 0))))
     val m = sys.states.find(_.sym.name == "m").get
     assert(m.init.isDefined)
     assert(m.init.get.toString == "([8'b0] x 4)[2'b0 := 8'b1]")
@@ -136,108 +137,6 @@ private class FirrtlModuleToTransitionSystemSpec extends SMTBackendBaseSpec {
     assert(false, "TODO")
   }
 
-  it should "support memories with registered read port" in {
-    def src(readUnderWrite: String) =
-      s"""circuit m:
-         |  module m:
-         |    input reset : UInt<1>
-         |    input clock : Clock
-         |    input addr : UInt<5>
-         |    input in : UInt<8>
-         |    output out : UInt<8>
-         |
-         |    mem m:
-         |      data-type => UInt<8>
-         |      depth => 32
-         |      reader => r
-         |      writer => w1, w2
-         |      read-latency => 1
-         |      write-latency => 1
-         |      read-under-write => $readUnderWrite
-         |
-         |    m.w1.clk <= clock
-         |    m.w1.mask <= UInt(1)
-         |    m.w1.en <= UInt(1)
-         |    m.w1.data <= in
-         |    m.w1.addr <= addr
-         |    m.w2.clk <= clock
-         |    m.w2.mask <= UInt(1)
-         |    m.w2.en <= UInt(1)
-         |    m.w2.data <= in
-         |    m.w2.addr <= addr
-         |
-         |    m.r.clk <= clock
-         |    m.r.en <= UInt(1)
-         |    out <= m.r.data
-         |    m.r.addr <= addr
-         |
-         |""".stripMargin
-
-    val oldValue = toSys(src("old"))
-    val oldMData = oldValue.states.find(_.sym.name == "m.r.data").get
-    assert(oldMData.sym.toString == "m.r.data")
-    assert(oldMData.next.get.toString == "m[m.r.addr]", "we just need to read the current value")
-    val readDataSignal = oldValue.signals.find(_.name == "m.r.data")
-    assert(readDataSignal.isEmpty, s"${readDataSignal.map(_.toString)} should not exist")
-
-    val undefinedValue = toSys(src("undefined"))
-    val undefinedMData = undefinedValue.states.find(_.sym.name == "m.r.data").get
-    assert(undefinedMData.sym.toString == "m.r.data")
-    val undefined = "RANDOM.m_r_read_under_write_undefined"
-    assert(
-      undefinedMData.next.get.toString ==
-        s"ite(or(eq(m.r.addr, m.w1.addr), eq(m.r.addr, m.w2.addr)), $undefined, m[m.r.addr])",
-      "randomize result if there is a write"
-    )
-  }
-
-  it should "support memories with potential write-write conflicts" in {
-    val src =
-      s"""circuit m:
-         |  module m:
-         |    input reset : UInt<1>
-         |    input clock : Clock
-         |    input addr : UInt<5>
-         |    input in : UInt<8>
-         |    output out : UInt<8>
-         |
-         |    mem m:
-         |      data-type => UInt<8>
-         |      depth => 32
-         |      reader => r
-         |      writer => w1, w2
-         |      read-latency => 1
-         |      write-latency => 1
-         |      read-under-write => undefined
-         |
-         |    m.w1.clk <= clock
-         |    m.w1.mask <= UInt(1)
-         |    m.w1.en <= UInt(1)
-         |    m.w1.data <= in
-         |    m.w1.addr <= addr
-         |    m.w2.clk <= clock
-         |    m.w2.mask <= UInt(1)
-         |    m.w2.en <= UInt(1)
-         |    m.w2.data <= in
-         |    m.w2.addr <= addr
-         |
-         |    m.r.clk <= clock
-         |    m.r.en <= UInt(1)
-         |    out <= m.r.data
-         |    m.r.addr <= addr
-         |
-         |""".stripMargin
-
-    val sys = toSys(src)
-    val m = sys.states.find(_.sym.name == "m").get
-
-    val regularUpdate = "m[m.w1.addr := m.w1.data][m.w2.addr := m.w2.data]"
-    val collision = "eq(m.w1.addr, m.w2.addr)"
-    val collisionUpdate = "m[m.w1.addr := RANDOM.m_w1_write_write_collision]"
-
-    assert(m.next.get.toString == s"ite($collision, $collisionUpdate, $regularUpdate)")
-  }
-
   it should "model invalid signals as inputs" in {
     // if a signal is invalid, it could take on an arbitrary value in that cycle
     val src =
@@ -249,11 +148,11 @@ private class FirrtlModuleToTransitionSystemSpec extends SMTBackendBaseSpec {
         |    when en:
         |      o <= UInt<8>(0)
         |""".stripMargin
-    val sys = toSys(src)
+    val sys = SMTBackendHelpers.toSys(src)
     assert(sys.inputs.length == 2)
-    val random = sys.inputs.filter(_.name.contains("RANDOM"))
-    assert(random.length == 1)
-    assert(random.head.width == 8)
+    val invalids = sys.inputs.filter(_.name.contains("_invalid"))
+    assert(invalids.length == 1)
+    assert(invalids.head.width == 8)
   }
 
   it should "ignore assignments, ports, wires and nodes of clock type" in {
@@ -269,7 +168,7 @@ private class FirrtlModuleToTransitionSystemSpec extends SMTBackendBaseSpec {
         |    o <= x
         |    w <= clk
         |""".stripMargin
-    val sys = toSys(src)
+    val sys = SMTBackendHelpers.toSys(src)
     assert(sys.inputs.isEmpty, "Clock inputs should be ignored.")
     assert(sys.outputs.isEmpty, "Clock outputs should be ignored.")
     assert(sys.signals.isEmpty, "Connects of clock type should be ignored.")
@@ -288,14 +187,14 @@ private class FirrtlModuleToTransitionSystemSpec extends SMTBackendBaseSpec {
         |    inst c of c
         |""".stripMargin
     val err = intercept[MultiClockException] {
-      toSys(src)
+      SMTBackendHelpers.toSys(src)
     }
     assert(err.getMessage.contains("clk, c.clk"))
   }
 
   it should "throw an error on async reset" in {
     val err = intercept[AsyncResetException] {
-      toSys(
+      SMTBackendHelpers.toSys(
         """circuit m:
           |  module m:
           |    input reset : AsyncReset
@@ -307,7 +206,7 @@ private class FirrtlModuleToTransitionSystemSpec extends SMTBackendBaseSpec {
 
   it should "throw an error on casting to async reset" in {
     val err = intercept[AssertionError] {
-      toSys(
+      SMTBackendHelpers.toSys(
         """circuit m:
           |  module m:
           |    input reset : UInt<1>
@@ -320,7 +219,7 @@ private class FirrtlModuleToTransitionSystemSpec extends SMTBackendBaseSpec {
 
   it should "throw an error on multiple clocks" in {
     val err = intercept[MultiClockException] {
-      toSys(
+      SMTBackendHelpers.toSys(
         """circuit m:
           |  module m:
           |    input clk1 : Clock
@@ -335,7 +234,7 @@ private class FirrtlModuleToTransitionSystemSpec extends SMTBackendBaseSpec {
     // While this could potentially be supported in the future, for now we do not allow
     // a clock to be used for anything besides updating registers and memories.
     val err = intercept[AssertionError] {
-      toSys(
+      SMTBackendHelpers.toSys(
         """circuit m:
           |  module m:
           |    input clk : Clock
@@ -358,7 +257,7 @@ private class FirrtlModuleToTransitionSystemSpec extends SMTBackendBaseSpec {
         |    assert(c, i, UInt(1), "")
         |    assert(c, i, UInt(1), "")
         |""".stripMargin
-    assertUniqueSignalNames(toSys(src0))
+    assertUniqueSignalNames(SMTBackendHelpers.toSys(src0))
 
     val src1 =
       """circuit m:
@@ -369,7 +268,7 @@ private class FirrtlModuleToTransitionSystemSpec extends SMTBackendBaseSpec {
         |    assert(c, i, UInt(1), "")
         |    node assert_ = i
         |""".stripMargin
-    assertUniqueSignalNames(toSys(src1))
+    assertUniqueSignalNames(SMTBackendHelpers.toSys(src1))
   }
 
   private def assertUniqueSignalNames(sys: TransitionSystem): Unit = {
diff --git a/src/test/scala/firrtl/backends/experimental/smt/SMTBackendBaseSpec.scala b/src/test/scala/firrtl/backends/experimental/smt/SMTBackendHelpers.scala
index a82767ae..4d212ad4 100644
--- a/src/test/scala/firrtl/backends/experimental/smt/SMTBackendBaseSpec.scala
+++ b/src/test/scala/firrtl/backends/experimental/smt/SMTBackendHelpers.scala
@@ -5,18 +5,17 @@ package firrtl.backends.experimental.smt
 import firrtl.annotations.Annotation
 import firrtl.{ir, MemoryInitValue}
 import firrtl.stage.{Forms, TransformManager}
-import org.scalatest.flatspec.AnyFlatSpec
 
-private abstract class SMTBackendBaseSpec extends AnyFlatSpec {
-  private val dependencies = Forms.LowForm
+private object SMTBackendHelpers {
+  private val dependencies = Forms.LowForm ++ FirrtlToTransitionSystem.prerequisites
   private val compiler = new TransformManager(dependencies)
 
-  protected def compile(src: String, annos: Seq[Annotation] = List()): ir.Circuit = {
+  def compile(src: String, annos: Seq[Annotation] = List()): ir.Circuit = {
     val c = firrtl.Parser.parse(src)
     compiler.runTransform(firrtl.CircuitState(c, annos)).circuit
   }
 
-  protected def toSys(
+  def toSys(
     src:        String,
     mod:        String = "m",
     presetRegs: Set[String] = Set(),
@@ -28,15 +27,15 @@ private abstract class SMTBackendBaseSpec extends AnyFlatSpec {
     new ModuleToTransitionSystem().run(module, presetRegs = presetRegs, memInit = memInit)
   }
 
-  protected def toBotr2(src: String, mod: String = "m"): Iterable[String] =
+  def toBotr2(src: String, mod: String = "m"): Iterable[String] =
     Btor2Serializer.serialize(toSys(src, mod))
 
-  protected def toBotr2Str(src: String, mod: String = "m"): String =
+  def toBotr2Str(src: String, mod: String = "m"): String =
     toBotr2(src, mod).mkString("\n") + "\n"
 
-  protected def toSMTLib(src: String, mod: String = "m"): Iterable[String] =
+  def toSMTLib(src: String, mod: String = "m"): Iterable[String] =
     SMTTransitionSystemEncoder.encode(toSys(src, mod)).map(SMTLibSerializer.serialize)
 
-  protected def toSMTLibStr(src: String, mod: String = "m"): String =
+  def toSMTLibStr(src: String, mod: String = "m"): String =
     toSMTLib(src, mod).mkString("\n") + "\n"
 }
diff --git a/src/test/scala/firrtl/backends/experimental/smt/SMTLibSpec.scala b/src/test/scala/firrtl/backends/experimental/smt/SMTLibSpec.scala
index b970484e..338d760c 100644
--- a/src/test/scala/firrtl/backends/experimental/smt/SMTLibSpec.scala
+++ b/src/test/scala/firrtl/backends/experimental/smt/SMTLibSpec.scala
@@ -2,7 +2,10 @@
 
 package firrtl.backends.experimental.smt
 
-private class SMTLibSpec extends SMTBackendBaseSpec {
+import org.scalatest.flatspec.AnyFlatSpec
+
+class SMTLibSpec extends AnyFlatSpec {
+  behavior.of("SMTLib backend")
 
   it should "convert a hello world module" in {
     val src =
@@ -12,7 +15,7 @@ private class SMTLibSpec extends SMTBackendBaseSpec {
         |    input a: UInt<8>
         |    output b: UInt<16>
         |    b <= a
-        |    assert(clock, eq(a, b), UInt(1), "")
+        |    assert(clock, eq(a, b), UInt(1), "") : a_eq_b
         |""".stripMargin
 
     val expected =
@@ -21,15 +24,15 @@ private class SMTLibSpec extends SMTBackendBaseSpec {
         |(declare-fun a_f (m_s) (_ BitVec 8))
         |; firrtl-smt2-output b 16
         |(define-fun b_f ((state m_s)) (_ BitVec 16) ((_ zero_extend 8) (a_f state)))
-        |; firrtl-smt2-assert assert_ 1
-        |(define-fun assert__f ((state m_s)) Bool (= ((_ zero_extend 8) (a_f state)) (b_f state)))
+        |; firrtl-smt2-assert a_eq_b 1
+        |(define-fun a_eq_b_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)
-        |(define-fun m_a ((state m_s)) Bool (assert__f state))
+        |(define-fun m_a ((state m_s)) Bool (a_eq_b_f state))
         |(define-fun m_u ((state m_s)) Bool true)
         |""".stripMargin
 
-    assert(toSMTLibStr(src) == expected)
+    assert(SMTBackendHelpers.toSMTLibStr(src) == expected)
   }
 
   it should "include FileInfo in the output" in {
@@ -52,15 +55,15 @@ private class SMTLibSpec extends SMTBackendBaseSpec {
         |; firrtl-smt2-output b 16
         |; @ 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_ 1
+        |; firrtl-smt2-assert assert_0 1
         |; @ assert 0:0
-        |(define-fun assert__f ((state m_s)) Bool (= ((_ zero_extend 8) (a_f state)) (b_f state)))
+        |(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)
-        |(define-fun m_a ((state m_s)) Bool (assert__f state))
+        |(define-fun m_a ((state m_s)) Bool (assert_0_f state))
         |(define-fun m_u ((state m_s)) Bool true)
         |""".stripMargin
 
-    assert(toSMTLibStr(src) == expected)
+    assert(SMTBackendHelpers.toSMTLibStr(src) == expected)
   }
 }