All of src/ formatted with scalafmt

5 files changed, 142 insertions, 124 deletions

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: