All of src/ formatted with scalafmt

8 files changed, 261 insertions, 222 deletions

diff --git a/src/test/scala/firrtl/backends/experimental/smt/FirrtlExpressionSemanticsSpec.scala b/src/test/scala/firrtl/backends/experimental/smt/FirrtlExpressionSemanticsSpec.scala
index 015ac4a9..f7ce9914 100644
--- a/src/test/scala/firrtl/backends/experimental/smt/FirrtlExpressionSemanticsSpec.scala
+++ b/src/test/scala/firrtl/backends/experimental/smt/FirrtlExpressionSemanticsSpec.scala
@@ -20,10 +20,16 @@ private class FirrtlExpressionSemanticsSpec extends SMTBackendBaseSpec {
     sys.signals.head.e.toString
   }
 
-  def primop(signed: Boolean, op: String, resWidth: Int, inWidth: Seq[Int], consts: Seq[Int] = List(),
-             resAlwaysUnsigned: Boolean = false): String = {
-    val tpe = if(signed) "SInt" else "UInt"
-    val resTpe = if(resAlwaysUnsigned) "UInt" else tpe
+  def primop(
+    signed:            Boolean,
+    op:                String,
+    resWidth:          Int,
+    inWidth:           Seq[Int],
+    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)
   }
@@ -52,16 +58,24 @@ 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
-    assert(primop(false, "div", 8, List(8, 8)) ==
-      "ite(eq(i1, 8'b0), RANDOM.res, udiv(i0, i1))")
-    assert(primop(false, "div", 8, List(8, 4)) ==
-      "ite(eq(i1, 4'b0), RANDOM.res, udiv(i0, zext(i1, 4)))")
+    assert(
+      primop(false, "div", 8, List(8, 8)) ==
+        "ite(eq(i1, 8'b0), RANDOM.res, udiv(i0, i1))"
+    )
+    assert(
+      primop(false, "div", 8, List(8, 4)) ==
+        "ite(eq(i1, 4'b0), RANDOM.res, 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)))")
-    assert(primop(true, "div", 8, List(7, 4))
-      == "ite(eq(i1, 4'b0), RANDOM.res, sdiv(sext(i0, 1), sext(i1, 4)))")
+    assert(
+      primop(true, "div", 8, List(7, 7)) ==
+        "ite(eq(i1, 7'b0), RANDOM.res, 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)))"
+    )
   }
 
   it should "correctly translate the `rem` primitive operation" in {
@@ -134,15 +148,19 @@ private class FirrtlExpressionSemanticsSpec extends SMTBackendBaseSpec {
   it should "correctly translate the `dshl` primitive operation" in {
     assert(primop(false, "dshl", 31, List(16, 4)) == "logical_shift_left(zext(i0, 15), zext(i1, 27))")
     assert(primop(false, "dshl", 19, List(16, 2)) == "logical_shift_left(zext(i0, 3), zext(i1, 17))")
-    assert(primop("dshl", "SInt<19>", List("SInt<16>", "UInt<2>"), List()) ==
-      "logical_shift_left(sext(i0, 3), zext(i1, 17))")
+    assert(
+      primop("dshl", "SInt<19>", List("SInt<16>", "UInt<2>"), List()) ==
+        "logical_shift_left(sext(i0, 3), zext(i1, 17))"
+    )
   }
 
   it should "correctly translate the `dshr` primitive operation" in {
     assert(primop(false, "dshr", 16, List(16, 4)) == "logical_shift_right(i0, zext(i1, 12))")
     assert(primop(false, "dshr", 16, List(16, 2)) == "logical_shift_right(i0, zext(i1, 14))")
-    assert(primop("dshr", "SInt<16>", List("SInt<16>", "UInt<2>"), List()) ==
-      "arithmetic_shift_right(i0, zext(i1, 14))")
+    assert(
+      primop("dshr", "SInt<16>", List("SInt<16>", "UInt<2>"), List()) ==
+        "arithmetic_shift_right(i0, zext(i1, 14))"
+    )
   }
 
   it should "correctly translate the `cvt` primitive operation" in {
@@ -197,15 +215,15 @@ private class FirrtlExpressionSemanticsSpec extends SMTBackendBaseSpec {
   }
 
   it should "correctly translate the `bits` primitive operation" in {
-    assert(primop(false, "bits", 1, List(4), List(2,2)) == "i0[2]")
-    assert(primop(false, "bits", 2, List(4), List(2,1)) == "i0[2:1]")
-    assert(primop(false, "bits", 1, List(4), List(2,1)) == "i0[2:1][0]")
-    assert(primop(false, "bits", 3, List(4), List(2,1)) == "zext(i0[2:1], 1)")
+    assert(primop(false, "bits", 1, List(4), List(2, 2)) == "i0[2]")
+    assert(primop(false, "bits", 2, List(4), List(2, 1)) == "i0[2:1]")
+    assert(primop(false, "bits", 1, List(4), List(2, 1)) == "i0[2:1][0]")
+    assert(primop(false, "bits", 3, List(4), List(2, 1)) == "zext(i0[2:1], 1)")
 
-    assert(primop(true, "bits", 1, List(4), List(2,2), resAlwaysUnsigned = true) == "i0[2]")
-    assert(primop(true, "bits", 2, List(4), List(2,1), resAlwaysUnsigned = true) == "i0[2:1]")
-    assert(primop(true, "bits", 1, List(4), List(2,1), resAlwaysUnsigned = true) == "i0[2:1][0]")
-    assert(primop(true, "bits", 3, List(4), List(2,1), resAlwaysUnsigned = true) == "zext(i0[2:1], 1)")
+    assert(primop(true, "bits", 1, List(4), List(2, 2), resAlwaysUnsigned = true) == "i0[2]")
+    assert(primop(true, "bits", 2, List(4), List(2, 1), resAlwaysUnsigned = true) == "i0[2:1]")
+    assert(primop(true, "bits", 1, List(4), List(2, 1), resAlwaysUnsigned = true) == "i0[2:1][0]")
+    assert(primop(true, "bits", 3, List(4), List(2, 1), resAlwaysUnsigned = true) == "zext(i0[2:1], 1)")
   }
 
   it should "correctly translate the `head` primitive operation" in {
@@ -221,4 +239,4 @@ private class FirrtlExpressionSemanticsSpec extends SMTBackendBaseSpec {
     assert(primop(false, "tail", 4, List(5), List(1)) == "i0[3:0]")
     assert(primop(false, "tail", 2, List(5), List(3)) == "i0[1:0]")
   }
-}
\ No newline at end of file
+}
diff --git a/src/test/scala/firrtl/backends/experimental/smt/FirrtlModuleToTransitionSystemSpec.scala b/src/test/scala/firrtl/backends/experimental/smt/FirrtlModuleToTransitionSystemSpec.scala
index ca7974c5..b41313e3 100644
--- a/src/test/scala/firrtl/backends/experimental/smt/FirrtlModuleToTransitionSystemSpec.scala
+++ b/src/test/scala/firrtl/backends/experimental/smt/FirrtlModuleToTransitionSystemSpec.scala
@@ -5,8 +5,7 @@ package firrtl.backends.experimental.smt
 import firrtl.{MemoryArrayInit, MemoryScalarInit, Utils}
 
 private class FirrtlModuleToTransitionSystemSpec extends SMTBackendBaseSpec {
-  behavior of "ModuleToTransitionSystem.run"
-
+  behavior.of("ModuleToTransitionSystem.run")
 
   it should "model registers as state" in {
     // if a signal is invalid, it could take on an arbitrary value in that cycle
@@ -42,39 +41,39 @@ private class FirrtlModuleToTransitionSystemSpec extends SMTBackendBaseSpec {
 
   private def memCircuit(depth: Int = 32) =
     s"""circuit m:
-      |  module m:
-      |    input reset : UInt<1>
-      |    input clock : Clock
-      |    input addr : UInt<${Utils.getUIntWidth(depth)}>
-      |    input in : UInt<8>
-      |    output out : UInt<8>
-      |
-      |    mem m:
-      |      data-type => UInt<8>
-      |      depth => $depth
-      |      reader => r
-      |      writer => w
-      |      read-latency => 0
-      |      write-latency => 1
-      |      read-under-write => new
-      |
-      |    m.w.clk <= clock
-      |    m.w.mask <= UInt(1)
-      |    m.w.en <= UInt(1)
-      |    m.w.data <= in
-      |    m.w.addr <= addr
-      |
-      |    m.r.clk <= clock
-      |    m.r.en <= UInt(1)
-      |    out <= m.r.data
-      |    m.r.addr <= addr
-      |
-      |""".stripMargin
+       |  module m:
+       |    input reset : UInt<1>
+       |    input clock : Clock
+       |    input addr : UInt<${Utils.getUIntWidth(depth)}>
+       |    input in : UInt<8>
+       |    output out : UInt<8>
+       |
+       |    mem m:
+       |      data-type => UInt<8>
+       |      depth => $depth
+       |      reader => r
+       |      writer => w
+       |      read-latency => 0
+       |      write-latency => 1
+       |      read-under-write => new
+       |
+       |    m.w.clk <= clock
+       |    m.w.mask <= UInt(1)
+       |    m.w.en <= UInt(1)
+       |    m.w.data <= in
+       |    m.w.addr <= addr
+       |
+       |    m.r.clk <= clock
+       |    m.r.en <= UInt(1)
+       |    out <= m.r.data
+       |    m.r.addr <= addr
+       |
+       |""".stripMargin
 
   it should "model memories as state" in {
     val sys = toSys(memCircuit())
 
-    assert(sys.signals.length == 9-2+1, "9 connects - 2 clock connects + 1 combinatorial read port")
+    assert(sys.signals.length == 9 - 2 + 1, "9 connects - 2 clock connects + 1 combinatorial read port")
 
     val sig = sys.signals.map(s => s.name -> s.e).toMap
 
@@ -140,40 +139,39 @@ private class FirrtlModuleToTransitionSystemSpec extends SMTBackendBaseSpec {
   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
-
+         |  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
@@ -186,9 +184,11 @@ private class FirrtlModuleToTransitionSystemSpec extends SMTBackendBaseSpec {
     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")
+    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 {
@@ -228,7 +228,6 @@ private class FirrtlModuleToTransitionSystemSpec extends SMTBackendBaseSpec {
          |
          |""".stripMargin
 
-
     val sys = toSys(src)
     val m = sys.states.find(_.sym.name == "m").get
 
diff --git a/src/test/scala/firrtl/backends/experimental/smt/SMTBackendBaseSpec.scala b/src/test/scala/firrtl/backends/experimental/smt/SMTBackendBaseSpec.scala
index 6bfb5437..209279fd 100644
--- a/src/test/scala/firrtl/backends/experimental/smt/SMTBackendBaseSpec.scala
+++ b/src/test/scala/firrtl/backends/experimental/smt/SMTBackendBaseSpec.scala
@@ -3,7 +3,7 @@
 package firrtl.backends.experimental.smt
 
 import firrtl.annotations.Annotation
-import firrtl.{MemoryInitValue, ir}
+import firrtl.{ir, MemoryInitValue}
 import firrtl.stage.{Forms, TransformManager}
 import org.scalatest.flatspec.AnyFlatSpec
 
@@ -16,8 +16,12 @@ private abstract class SMTBackendBaseSpec extends AnyFlatSpec {
     compiler.runTransform(firrtl.CircuitState(c, annos)).circuit
   }
 
-  protected def toSys(src: String, mod: String = "m", presetRegs: Set[String] = Set(),
-                      memInit: Map[String, MemoryInitValue] = Map()): TransitionSystem = {
+  protected def toSys(
+    src:        String,
+    mod:        String = "m",
+    presetRegs: Set[String] = Set(),
+    memInit:    Map[String, MemoryInitValue] = Map()
+  ): TransitionSystem = {
     val circuit = compile(src)
     val module = circuit.modules.find(_.name == mod).get.asInstanceOf[ir.Module]
     // println(module.serialize)
@@ -35,4 +39,4 @@ private abstract class SMTBackendBaseSpec extends AnyFlatSpec {
 
   protected def toSMTLibStr(src: String, mod: String = "m"): String =
     toSMTLib(src, mod).mkString("\n") + "\n"
-}
\ No newline at end of file
+}
diff --git a/src/test/scala/firrtl/backends/experimental/smt/end2end/AsyncResetSpec.scala b/src/test/scala/firrtl/backends/experimental/smt/end2end/AsyncResetSpec.scala
index 4c6901ea..e7c8d534 100644
--- a/src/test/scala/firrtl/backends/experimental/smt/end2end/AsyncResetSpec.scala
+++ b/src/test/scala/firrtl/backends/experimental/smt/end2end/AsyncResetSpec.scala
@@ -10,9 +10,10 @@ import firrtl.stage.RunFirrtlTransformAnnotation
 class AsyncResetSpec extends EndToEndSMTBaseSpec {
   def annos(name: String) = Seq(
     RunFirrtlTransformAnnotation(Dependency[StutteringClockTransform]),
-    GlobalClockAnnotation(CircuitTarget(name).module(name).ref("global_clock")))
+    GlobalClockAnnotation(CircuitTarget(name).module(name).ref("global_clock"))
+  )
 
-  "a module with asynchronous reset" should "allow a register to change between clock edges" taggedAs(RequiresZ3) in {
+  "a module with asynchronous reset" should "allow a register to change between clock edges" taggedAs (RequiresZ3) in {
     def in(resetType: String) =
       s"""circuit AsyncReset00:
          |  module AsyncReset00:
@@ -39,8 +40,8 @@ class AsyncResetSpec extends EndToEndSMTBaseSpec {
          |    ; can the value of r change without the count changing?
          |    assert(global_clock, or(not(eq(count, past_count)), eq(r, past_r)), past_valid, "count = past(count) |-> r = past(r)")
          |""".stripMargin
-    test(in("AsyncReset"), MCFail(1), kmax=2, annos=annos("AsyncReset00"))
-    test(in("UInt<1>"), MCSuccess, kmax=2, annos=annos("AsyncReset00"))
+    test(in("AsyncReset"), MCFail(1), kmax = 2, annos = annos("AsyncReset00"))
+    test(in("UInt<1>"), MCSuccess, kmax = 2, annos = annos("AsyncReset00"))
   }
 
 }
diff --git a/src/test/scala/firrtl/backends/experimental/smt/end2end/EndToEndSMTSpec.scala b/src/test/scala/firrtl/backends/experimental/smt/end2end/EndToEndSMTSpec.scala
index 2227719b..974d2e81 100644
--- a/src/test/scala/firrtl/backends/experimental/smt/end2end/EndToEndSMTSpec.scala
+++ b/src/test/scala/firrtl/backends/experimental/smt/end2end/EndToEndSMTSpec.scala
@@ -16,24 +16,23 @@ import org.scalatest.matchers.must.Matchers
 import scala.sys.process._
 
 class EndToEndSMTSpec extends EndToEndSMTBaseSpec with LazyLogging {
-  "we" should "check if Z3 is available" taggedAs(RequiresZ3) in {
+  "we" should "check if Z3 is available" taggedAs (RequiresZ3) in {
     val log = ProcessLogger(_ => (), logger.warn(_))
     val ret = Process(Seq("which", "z3")).run(log).exitValue()
-    if(ret != 0) {
-      logger.error(
-        """The z3 SMT-Solver seems not to be installed.
-          |You can exclude the end-to-end smt backend tests which rely on z3 like this:
-          |sbt testOnly -- -l RequiresZ3
-          |""".stripMargin)
+    if (ret != 0) {
+      logger.error("""The z3 SMT-Solver seems not to be installed.
+                     |You can exclude the end-to-end smt backend tests which rely on z3 like this:
+                     |sbt testOnly -- -l RequiresZ3
+                     |""".stripMargin)
     }
     assert(ret == 0)
   }
 
-  "Z3" should "be available in version 4" taggedAs(RequiresZ3) in {
+  "Z3" should "be available in version 4" taggedAs (RequiresZ3) in {
     assert(Z3ModelChecker.getZ3Version.startsWith("4."))
   }
 
-  "a simple combinatorial check" should "pass" taggedAs(RequiresZ3) in {
+  "a simple combinatorial check" should "pass" taggedAs (RequiresZ3) in {
     val in =
       """circuit CC00:
         |  module CC00:
@@ -45,7 +44,7 @@ class EndToEndSMTSpec extends EndToEndSMTBaseSpec with LazyLogging {
     test(in, MCSuccess)
   }
 
-  "a simple combinatorial check" should "fail immediately" taggedAs(RequiresZ3) in {
+  "a simple combinatorial check" should "fail immediately" taggedAs (RequiresZ3) in {
     val in =
       """circuit CC01:
         |  module CC01:
@@ -57,7 +56,7 @@ class EndToEndSMTSpec extends EndToEndSMTBaseSpec with LazyLogging {
     test(in, MCFail(0))
   }
 
-  "adding the right assumption" should "make a test pass" taggedAs(RequiresZ3) in {
+  "adding the right assumption" should "make a test pass" taggedAs (RequiresZ3) in {
     val in0 =
       """circuit CC01:
         |  module CC01:
@@ -75,8 +74,8 @@ class EndToEndSMTSpec extends EndToEndSMTBaseSpec with LazyLogging {
         |    assert(c, neq(add(a, b), UInt(0)), UInt(1), "a + b != 0")
         |    assume(c, neq(a, UInt(0)), UInt(1), "a != 0")
         |""".stripMargin
-      test(in0, MCFail(0))
-      test(in1, MCSuccess)
+    test(in0, MCFail(0))
+    test(in1, MCSuccess)
 
     val in2 =
       """circuit CC01:
@@ -91,20 +90,20 @@ class EndToEndSMTSpec extends EndToEndSMTBaseSpec with LazyLogging {
     test(in2, MCFail(0))
   }
 
-  "a register connected to preset reset" should "be initialized with the reset value" taggedAs(RequiresZ3) in {
+  "a register connected to preset reset" should "be initialized with the reset value" taggedAs (RequiresZ3) in {
     def in(rEq: Int) =
       s"""circuit Preset00:
-        |  module Preset00:
-        |    input c: Clock
-        |    input preset: AsyncReset
-        |    reg r: UInt<4>, c with: (reset => (preset, UInt(3)))
-        |    assert(c, eq(r, UInt($rEq)), UInt(1), "r = $rEq")
-        |""".stripMargin
+         |  module Preset00:
+         |    input c: Clock
+         |    input preset: AsyncReset
+         |    reg r: UInt<4>, c with: (reset => (preset, UInt(3)))
+         |    assert(c, eq(r, UInt($rEq)), UInt(1), "r = $rEq")
+         |""".stripMargin
     test(in(3), MCSuccess, kmax = 1)
     test(in(2), MCFail(0))
   }
 
-  "a register's initial value" should "should not change" taggedAs(RequiresZ3) in {
+  "a register's initial value" should "should not change" taggedAs (RequiresZ3) in {
     val in =
       """circuit Preset00:
         |  module Preset00:
@@ -127,24 +126,29 @@ class EndToEndSMTSpec extends EndToEndSMTBaseSpec with LazyLogging {
 abstract class EndToEndSMTBaseSpec extends AnyFlatSpec with Matchers {
   def test(src: String, expected: MCResult, kmax: Int = 0, clue: String = "", annos: Seq[Annotation] = Seq()): Unit = {
     expected match {
-      case MCFail(k) => assert(kmax >= k, s"Please set a kmax that includes the expected failing step! ($kmax < $expected)")
+      case MCFail(k) =>
+        assert(kmax >= k, s"Please set a kmax that includes the expected failing step! ($kmax < $expected)")
       case _ =>
     }
     val fir = firrtl.Parser.parse(src)
     val name = fir.main
     val testDir = BackendCompilationUtilities.createTestDirectory("EndToEndSMT." + name)
     // we automagically add a preset annotation if an input called preset exists
-    val presetAnno = if(!src.contains("input preset")) { None } else {
+    val presetAnno = if (!src.contains("input preset")) { None }
+    else {
       Some(PresetAnnotation(CircuitTarget(name).module(name).ref("preset")))
     }
-    val res = (new FirrtlStage).execute(Array(), Seq(
-      LogLevelAnnotation(LogLevel.Error), // silence warnings for tests
-      RunFirrtlTransformAnnotation(new SMTLibEmitter),
-      RunFirrtlTransformAnnotation(new Btor2Emitter),
-      FirrtlCircuitAnnotation(fir),
-      TargetDirAnnotation(testDir.getAbsolutePath)
-    ) ++ presetAnno ++ annos)
-    assert(res.collectFirst{ case _: OutputFileAnnotation => true }.isDefined)
+    val res = (new FirrtlStage).execute(
+      Array(),
+      Seq(
+        LogLevelAnnotation(LogLevel.Error), // silence warnings for tests
+        RunFirrtlTransformAnnotation(new SMTLibEmitter),
+        RunFirrtlTransformAnnotation(new Btor2Emitter),
+        FirrtlCircuitAnnotation(fir),
+        TargetDirAnnotation(testDir.getAbsolutePath)
+      ) ++ presetAnno ++ annos
+    )
+    assert(res.collectFirst { case _: OutputFileAnnotation => true }.isDefined)
     val r = Z3ModelChecker.bmc(testDir, name, kmax)
     assert(r == expected, clue + "\n" + s"$testDir")
   }
@@ -153,7 +157,7 @@ abstract class EndToEndSMTBaseSpec extends AnyFlatSpec with Matchers {
 /** Minimal implementation of a Z3 based bounded model checker.
   * A more complete version of this with better use feedback should eventually be provided by a
   * chisel3 formal verification library. Do not use this implementation outside of the firrtl test suite!
-  * */
+  */
 private object Z3ModelChecker extends LazyLogging {
   def getZ3Version: String = {
     val (out, ret) = executeCmd("-version")
@@ -164,14 +168,15 @@ private object Z3ModelChecker extends LazyLogging {
   }
 
   def bmc(testDir: File, main: String, kmax: Int): MCResult = {
-    assert(kmax >=0 && kmax < 50, "Trying to keep kmax in a reasonable range.")
+    assert(kmax >= 0 && kmax < 50, "Trying to keep kmax in a reasonable range.")
     val smtFile = new File(testDir, main + ".smt2")
     val header = read(smtFile)
     val steps = (0 to kmax).map(k => new File(testDir, main + s"_step$k.smt2")).zipWithIndex
-    steps.foreach { case (f,k) =>
-      writeStep(f, main, header, k)
-      val success = executeStep(f.getAbsolutePath)
-      if(!success) return MCFail(k)
+    steps.foreach {
+      case (f, k) =>
+        writeStep(f, main, header, k)
+        val success = executeStep(f.getAbsolutePath)
+        if (!success) return MCFail(k)
     }
     MCSuccess
   }
@@ -200,21 +205,22 @@ private object Z3ModelChecker extends LazyLogging {
   private def step(main: String, k: Int): Iterable[String] = {
     // define all states
     (0 to k).map(ii => s"(declare-fun s$ii () $main$StateTpe)") ++
-    // assert that init holds in state 0
-    List(s"(assert ($main$Init s0))") ++
-    // assert transition relation
-    (0 until k).map(ii => s"(assert ($main$Transition s$ii s${ii+1}))") ++
-    // assert that assumptions hold in all states
-    (0 to k).map(ii =>  s"(assert ($main$Assumes s$ii))") ++
-    // assert that assertions hold for all but last state
-    (0 until k).map(ii =>  s"(assert ($main$Asserts s$ii))") ++
-    // check to see if we can violate the assertions in the last state
-    List(s"(assert (not ($main$Asserts s$k)))")
+      // assert that init holds in state 0
+      List(s"(assert ($main$Init s0))") ++
+      // assert transition relation
+      (0 until k).map(ii => s"(assert ($main$Transition s$ii s${ii + 1}))") ++
+      // assert that assumptions hold in all states
+      (0 to k).map(ii => s"(assert ($main$Assumes s$ii))") ++
+      // assert that assertions hold for all but last state
+      (0 until k).map(ii => s"(assert ($main$Asserts s$ii))") ++
+      // check to see if we can violate the assertions in the last state
+      List(s"(assert (not ($main$Asserts s$k)))")
   }
 
   private def read(f: File): Iterable[String] = {
     val source = scala.io.Source.fromFile(f)
-    try source.getLines().toVector finally source.close()
+    try source.getLines().toVector
+    finally source.close()
   }
 
   // the following suffixes have to match the ones in [[SMTTransitionSystemEncoder]]
diff --git a/src/test/scala/firrtl/backends/experimental/smt/end2end/MemorySpec.scala b/src/test/scala/firrtl/backends/experimental/smt/end2end/MemorySpec.scala
index 10de9cda..61e1f0f8 100644
--- a/src/test/scala/firrtl/backends/experimental/smt/end2end/MemorySpec.scala
+++ b/src/test/scala/firrtl/backends/experimental/smt/end2end/MemorySpec.scala
@@ -9,43 +9,43 @@ class MemorySpec extends EndToEndSMTBaseSpec {
     registeredTestMem(name, cmds.split("\n"), readUnderWrite)
   private def registeredTestMem(name: String, cmds: Iterable[String], readUnderWrite: String): String =
     s"""circuit $name:
-      |  module $name:
-      |    input reset : UInt<1>
-      |    input clock : Clock
-      |    input preset: AsyncReset
-      |    input write_addr : UInt<5>
-      |    input read_addr : UInt<5>
-      |    input in : UInt<8>
-      |    output out : UInt<8>
-      |
-      |    mem m:
-      |      data-type => UInt<8>
-      |      depth => 32
-      |      reader => r
-      |      writer => w
-      |      read-latency => 1
-      |      write-latency => 1
-      |      read-under-write => $readUnderWrite
-      |
-      |    m.w.clk <= clock
-      |    m.w.mask <= UInt(1)
-      |    m.w.en <= UInt(1)
-      |    m.w.data <= in
-      |    m.w.addr <= write_addr
-      |
-      |    m.r.clk <= clock
-      |    m.r.en <= UInt(1)
-      |    out <= m.r.data
-      |    m.r.addr <= read_addr
-      |
-      |    reg cycle: UInt<8>, clock with: (reset => (preset, UInt(0)))
-      |    cycle <= add(cycle, UInt(1))
-      |    node past_valid = geq(cycle, UInt(1))
-      |
-      |    ${cmds.mkString("\n    ")}
-      |""".stripMargin
+       |  module $name:
+       |    input reset : UInt<1>
+       |    input clock : Clock
+       |    input preset: AsyncReset
+       |    input write_addr : UInt<5>
+       |    input read_addr : UInt<5>
+       |    input in : UInt<8>
+       |    output out : UInt<8>
+       |
+       |    mem m:
+       |      data-type => UInt<8>
+       |      depth => 32
+       |      reader => r
+       |      writer => w
+       |      read-latency => 1
+       |      write-latency => 1
+       |      read-under-write => $readUnderWrite
+       |
+       |    m.w.clk <= clock
+       |    m.w.mask <= UInt(1)
+       |    m.w.en <= UInt(1)
+       |    m.w.data <= in
+       |    m.w.addr <= write_addr
+       |
+       |    m.r.clk <= clock
+       |    m.r.en <= UInt(1)
+       |    out <= m.r.data
+       |    m.r.addr <= read_addr
+       |
+       |    reg cycle: UInt<8>, clock with: (reset => (preset, UInt(0)))
+       |    cycle <= add(cycle, UInt(1))
+       |    node past_valid = geq(cycle, UInt(1))
+       |
+       |    ${cmds.mkString("\n    ")}
+       |""".stripMargin
 
-  "Registered test memory" should "return written data after two cycles" taggedAs(RequiresZ3) in {
+  "Registered test memory" should "return written data after two cycles" taggedAs (RequiresZ3) in {
     val cmds =
       """node past_past_valid = geq(cycle, UInt(2))
         |reg past_in: UInt<8>, clock
@@ -85,23 +85,29 @@ class MemorySpec extends EndToEndSMTBaseSpec {
        |""".stripMargin
   private def m(num: Int) = CircuitTarget(s"Mem0$num").module(s"Mem0$num").ref("m")
 
-  "read-only memory" should "always return 0" taggedAs(RequiresZ3) in {
-    test(readOnlyMem("eq(out, UInt(0))", 1), MCSuccess, kmax=2,
-      annos=Seq(MemoryScalarInitAnnotation(m(1), 0)))
+  "read-only memory" should "always return 0" taggedAs (RequiresZ3) in {
+    test(readOnlyMem("eq(out, UInt(0))", 1), MCSuccess, kmax = 2, annos = Seq(MemoryScalarInitAnnotation(m(1), 0)))
   }
 
-  "read-only memory" should "not always return 1" taggedAs(RequiresZ3) in {
-    test(readOnlyMem("eq(out, UInt(1))", 2), MCFail(0), kmax=2,
-      annos=Seq(MemoryScalarInitAnnotation(m(2), 0)))
+  "read-only memory" should "not always return 1" taggedAs (RequiresZ3) in {
+    test(readOnlyMem("eq(out, UInt(1))", 2), MCFail(0), kmax = 2, annos = Seq(MemoryScalarInitAnnotation(m(2), 0)))
   }
 
-  "read-only memory" should "always return 1 or 2" taggedAs(RequiresZ3) in {
-    test(readOnlyMem("or(eq(out, UInt(1)), eq(out, UInt(2)))", 3), MCSuccess, kmax=2,
-      annos=Seq(MemoryArrayInitAnnotation(m(3), Seq(1, 2, 2, 1))))
+  "read-only memory" should "always return 1 or 2" taggedAs (RequiresZ3) in {
+    test(
+      readOnlyMem("or(eq(out, UInt(1)), eq(out, UInt(2)))", 3),
+      MCSuccess,
+      kmax = 2,
+      annos = Seq(MemoryArrayInitAnnotation(m(3), Seq(1, 2, 2, 1)))
+    )
   }
 
-  "read-only memory" should "not always return 1 or 2 or 3" taggedAs(RequiresZ3) in {
-    test(readOnlyMem("or(eq(out, UInt(1)), eq(out, UInt(2)))", 4), MCFail(0), kmax=2,
-      annos=Seq(MemoryArrayInitAnnotation(m(4), Seq(1, 2, 2, 3))))
+  "read-only memory" should "not always return 1 or 2 or 3" taggedAs (RequiresZ3) in {
+    test(
+      readOnlyMem("or(eq(out, UInt(1)), eq(out, UInt(2)))", 4),
+      MCFail(0),
+      kmax = 2,
+      annos = Seq(MemoryArrayInitAnnotation(m(4), Seq(1, 2, 2, 3)))
+    )
   }
 }
diff --git a/src/test/scala/firrtl/backends/experimental/smt/end2end/SMTCompilationTest.scala b/src/test/scala/firrtl/backends/experimental/smt/end2end/SMTCompilationTest.scala
index cbf194dd..8ece0e23 100644
--- a/src/test/scala/firrtl/backends/experimental/smt/end2end/SMTCompilationTest.scala
+++ b/src/test/scala/firrtl/backends/experimental/smt/end2end/SMTCompilationTest.scala
@@ -13,15 +13,17 @@ import scala.sys.process.{Process, ProcessLogger}
 
 /** compiles the regression tests to SMTLib and parses the result with z3 */
 class SMTCompilationTest extends AnyFlatSpec with LazyLogging {
-  it should "generate valid SMTLib for AddNot" taggedAs(RequiresZ3) in { compileAndParse("AddNot") }
-  it should "generate valid SMTLib for FPU" taggedAs(RequiresZ3) in { compileAndParse("FPU") }
+  it should "generate valid SMTLib for AddNot" taggedAs (RequiresZ3) in { compileAndParse("AddNot") }
+  it should "generate valid SMTLib for FPU" taggedAs (RequiresZ3) in { compileAndParse("FPU") }
   // we get a stack overflow in Scala 2.11 because of a deeply nested and(...) expression in the sequencer
-  it should "generate valid SMTLib for HwachaSequencer" taggedAs(RequiresZ3) ignore { compileAndParse("HwachaSequencer") }
-  it should "generate valid SMTLib for ICache" taggedAs(RequiresZ3) in { compileAndParse("ICache") }
-  it should "generate valid SMTLib for Ops" taggedAs(RequiresZ3) in { compileAndParse("Ops") }
+  it should "generate valid SMTLib for HwachaSequencer" taggedAs (RequiresZ3) ignore {
+    compileAndParse("HwachaSequencer")
+  }
+  it should "generate valid SMTLib for ICache" taggedAs (RequiresZ3) in { compileAndParse("ICache") }
+  it should "generate valid SMTLib for Ops" taggedAs (RequiresZ3) in { compileAndParse("Ops") }
   // TODO: enable Rob test once we support more than 2 write ports on a memory
-  it should "generate valid SMTLib for Rob" taggedAs(RequiresZ3) ignore { compileAndParse("Rob") }
-  it should "generate valid SMTLib for RocketCore" taggedAs(RequiresZ3) in { compileAndParse("RocketCore") }
+  it should "generate valid SMTLib for Rob" taggedAs (RequiresZ3) ignore { compileAndParse("Rob") }
+  it should "generate valid SMTLib for RocketCore" taggedAs (RequiresZ3) in { compileAndParse("RocketCore") }
 
   private def compileAndParse(name: String): Unit = {
     val testDir = BackendCompilationUtilities.createTestDirectory(name + "-smt")
@@ -29,14 +31,18 @@ class SMTCompilationTest extends AnyFlatSpec with LazyLogging {
     BackendCompilationUtilities.copyResourceToFile(s"/regress/${name}.fir", inputFile)
 
     val args = Array(
-      "-ll", "error", // surpress warnings to keep test output clean
-      "--target-dir", testDir.toString,
-      "-i", inputFile.toString,
-      "-E", "experimental-smt2"
+      "-ll",
+      "error", // surpress warnings to keep test output clean
+      "--target-dir",
+      testDir.toString,
+      "-i",
+      inputFile.toString,
+      "-E",
+      "experimental-smt2"
       // "-fct", "firrtl.backends.experimental.smt.StutteringClockTransform"
     )
     val res = (new FirrtlStage).execute(args, Seq())
-    val fileName = res.collectFirst{ case OutputFileAnnotation(file) => file }.get
+    val fileName = res.collectFirst { case OutputFileAnnotation(file) => file }.get
 
     val smtFile = testDir.toString + "/" + fileName + ".smt2"
     val log = ProcessLogger(_ => (), logger.error(_))
diff --git a/src/test/scala/firrtl/backends/experimental/smt/end2end/UndefinedFirrtlSpec.scala b/src/test/scala/firrtl/backends/experimental/smt/end2end/UndefinedFirrtlSpec.scala
index 8fa80b4c..8682c2ce 100644
--- a/src/test/scala/firrtl/backends/experimental/smt/end2end/UndefinedFirrtlSpec.scala
+++ b/src/test/scala/firrtl/backends/experimental/smt/end2end/UndefinedFirrtlSpec.scala
@@ -5,27 +5,26 @@ package firrtl.backends.experimental.smt.end2end
 /** undefined values in firrtl are modelled as fresh auxiliary variables (inputs) */
 class UndefinedFirrtlSpec extends EndToEndSMTBaseSpec {
 
-  "division by zero" should "result in an arbitrary value" taggedAs(RequiresZ3) in {
+  "division by zero" should "result in an arbitrary value" taggedAs (RequiresZ3) in {
     // the SMTLib spec defines the result of division by zero to be all 1s
     // https://cs.nyu.edu/pipermail/smt-lib/2015/000977.html
     def in(dEq: Int) =
-     s"""circuit CC00:
-        |  module CC00:
-        |    input c: Clock
-        |    input a: UInt<2>
-        |    input b: UInt<2>
-        |    assume(c, eq(b, UInt(0)), UInt(1), "b = 0")
-        |    node d = div(a, b)
-        |    assert(c, eq(d, UInt($dEq)), UInt(1), "d = $dEq")
-        |""".stripMargin
+      s"""circuit CC00:
+         |  module CC00:
+         |    input c: Clock
+         |    input a: UInt<2>
+         |    input b: UInt<2>
+         |    assume(c, eq(b, UInt(0)), UInt(1), "b = 0")
+         |    node d = div(a, b)
+         |    assert(c, eq(d, UInt($dEq)), UInt(1), "d = $dEq")
+         |""".stripMargin
     // we try to assert that (d = a / 0) is any fixed value which should be false
     (0 until 4).foreach { ii => test(in(ii), MCFail(0), 0, s"d = a / 0 = $ii") }
   }
 
   // TODO: rem should probably also be undefined, but the spec isn't 100% clear here
 
-
-  "invalid signals" should "have an arbitrary values" taggedAs(RequiresZ3) in {
+  "invalid signals" should "have an arbitrary values" taggedAs (RequiresZ3) in {
     def in(aEq: Int) =
       s"""circuit CC00:
          |  module CC00: