replace custom model checker with chiseltest formal verify command (#2075)

* replace custom model checker with chiseltest formal verify command

* integration-tests can make use of chiseltest

This is a compromise solution to avoid issues
with binary compatibility breaking changes in chisel3.

* ci: move integration tests into separate job

* run integration tests only for one scala version

* ci: install espresso for integration tests

* Update build.sbt

Co-authored-by: Jack Koenig <jack.koenig3@gmail.com>

Co-authored-by: Jack Koenig <jack.koenig3@gmail.com>

8 files changed, 105 insertions, 181 deletions

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index 3438dcf9..a2240ff8 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -113,13 +113,40 @@ jobs:
       - name: Binary compatibility
         run: sbt ++${{ matrix.scala }} mimaReportBinaryIssues
 
+  integration:
+    name: Integration Tests (w/ chiseltest)
+    runs-on: ubuntu-20.04
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v2
+      - name: Install Verilator and Z3
+        run: |
+          sudo apt-get install -y verilator z3
+          verilator --version
+          z3 --version
+      - name: Install Espresso
+        run: |
+          cd /tmp
+          wget https://github.com/chipsalliance/espresso/releases/download/v2.4/x86_64-linux-gnu-espresso
+          chmod +x x86_64-linux-gnu-espresso
+          sudo mv x86_64-linux-gnu-espresso /usr/local/bin/espresso
+          espresso || true
+      - name: Setup Scala
+        uses: olafurpg/setup-scala@v10
+        with:
+          java-version: "adopt@1.11"
+      - name: Cache Scala
+        uses: coursier/cache-action@v5
+      - name: Integration Tests
+        run: sbt integrationTests/test
+
   # Sentinel job to simplify how we specify which checks need to pass in branch
   # protection and in Mergify
   #
   # When adding new jobs, please add them to `needs` below
   all_tests_passed:
     name: "all tests passed"
-    needs: [ci]
+    needs: [ci, integration]
     runs-on: ubuntu-20.04
     steps:
       - run: echo Success!
diff --git a/build.sbt b/build.sbt
index 5d7fad2d..54bf87f0 100644
--- a/build.sbt
+++ b/build.sbt
@@ -4,7 +4,8 @@ enablePlugins(SiteScaladocPlugin)
 
 val defaultVersions = Map(
   "firrtl" -> "edu.berkeley.cs" %% "firrtl" % "1.5-SNAPSHOT",
-  "treadle" -> "edu.berkeley.cs" %% "treadle" % "1.5-SNAPSHOT"
+  "treadle" -> "edu.berkeley.cs" %% "treadle" % "1.5-SNAPSHOT",
+  "chiseltest" -> "edu.berkeley.cs" %% "chiseltest" % "0.5-SNAPSHOT",
 )
 
 lazy val commonSettings = Seq (
@@ -225,6 +226,16 @@ lazy val noPluginTests = (project in file ("no-plugin-tests")).
     libraryDependencies += defaultVersions("firrtl"),
   ))
 
+// tests elaborating and executing/formally verifying a Chisel circuit with chiseltest
+lazy val integrationTests = (project in file ("integration-tests")).
+  dependsOn(chisel).
+  settings(commonSettings: _*).
+  settings(chiselSettings: _*).
+  settings(usePluginSettings: _*).
+  settings(Seq(
+    libraryDependencies += defaultVersions("chiseltest") % "test",
+  ))
+
 lazy val docs = project       // new documentation project
   .in(file("docs-target")) // important: it must not be docs/
   .dependsOn(chisel)
diff --git a/integration-tests/src/test/scala/chiselTests/util/experimental/DecoderSpec.scala b/integration-tests/src/test/scala/chiselTests/util/experimental/DecoderSpec.scala
new file mode 100644
index 00000000..c31fdee0
--- /dev/null
+++ b/integration-tests/src/test/scala/chiselTests/util/experimental/DecoderSpec.scala
@@ -0,0 +1,53 @@
+// SPDX-License-Identifier: Apache-2.0
+
+package chiselTests.util.experimental
+
+import chisel3.util.experimental.decode.{DecodeTableAnnotation, Minimizer, QMCMinimizer, TruthTable}
+import chiselTests.util.experimental.minimizer.DecodeTestModule
+import firrtl.annotations.ReferenceTarget
+import org.scalatest.flatspec.AnyFlatSpec
+import chiseltest._
+import chiseltest.formal._
+
+class DecoderSpec extends AnyFlatSpec with ChiselScalatestTester with Formal  {
+  val xor = TruthTable(
+    """10->1
+      |01->1
+      |    0""".stripMargin)
+
+  def minimizer: Minimizer = QMCMinimizer
+
+  "decoder" should "pass without DecodeTableAnnotation" in {
+    verify(new DecodeTestModule(minimizer, table = xor), Seq(BoundedCheck(1)))
+  }
+
+  "decoder" should "fail with a incorrect DecodeTableAnnotation" in {
+    val annos = Seq(
+      DecodeTableAnnotation(ReferenceTarget("", "", Nil, "", Nil),
+        """10->1
+          |01->1
+          |    0""".stripMargin,
+        """10->1
+          |    0""".stripMargin
+      )
+    )
+    assertThrows[FailedBoundedCheckException] {
+      verify(new DecodeTestModule(minimizer, table = xor), BoundedCheck(1) +: annos)
+    }
+  }
+
+  "decoder" should "success with a correct DecodeTableAnnotation" in {
+    val annos = Seq(
+      DecodeTableAnnotation(ReferenceTarget("", "", Nil, "", Nil),
+        """10->1
+          |01->1
+          |    0""".stripMargin,
+        QMCMinimizer.minimize(TruthTable(
+          """10->1
+            |01->1
+            |    0""".stripMargin)).toString
+      )
+    )
+    verify(new DecodeTestModule(minimizer, table = xor), BoundedCheck(1) +: annos)
+  }
+}
diff --git a/src/test/scala/chiselTests/util/experimental/minimizer/EspressoSpec.scala b/integration-tests/src/test/scala/chiselTests/util/experimental/minimizer/EspressoSpec.scala
index f3270cae..f3270cae 100644
--- a/src/test/scala/chiselTests/util/experimental/minimizer/EspressoSpec.scala
+++ b/integration-tests/src/test/scala/chiselTests/util/experimental/minimizer/EspressoSpec.scala
diff --git a/src/test/scala/chiselTests/util/experimental/minimizer/MinimizerSpec.scala b/integration-tests/src/test/scala/chiselTests/util/experimental/minimizer/MinimizerSpec.scala
index 5e3be9a6..a932eb77 100644
--- a/src/test/scala/chiselTests/util/experimental/minimizer/MinimizerSpec.scala
+++ b/integration-tests/src/test/scala/chiselTests/util/experimental/minimizer/MinimizerSpec.scala
@@ -6,7 +6,9 @@ import chisel3._
 import chisel3.util._
 import chisel3.util.experimental.decode._
 import chisel3.util.pla
-import chiselTests.SMTModelCheckingSpec
+import chiseltest._
+import chiseltest.formal._
+import org.scalatest.flatspec.AnyFlatSpec
 
 class DecodeTestModule(minimizer: Minimizer, table: TruthTable) extends Module {
   val i = IO(Input(UInt(table.table.head._1.getWidth.W)))
@@ -21,15 +23,11 @@ class DecodeTestModule(minimizer: Minimizer, table: TruthTable) extends Module {
   )
 }
 
-trait MinimizerSpec extends SMTModelCheckingSpec {
+trait MinimizerSpec extends AnyFlatSpec with ChiselScalatestTester with Formal {
   def minimizer: Minimizer
 
-  def minimizerTest(testcase: TruthTable, caseName: String) = {
-    test(
-      () => new DecodeTestModule(minimizer, table = testcase),
-      s"${minimizer.getClass.getSimpleName}.$caseName",
-      success
-    )
+  def minimizerTest(testcase: TruthTable) = {
+    verify(new DecodeTestModule(minimizer, table = testcase), Seq(BoundedCheck(1)))
   }
 
   // Term that being commented out is the result of which is same as default,
@@ -48,7 +46,7 @@ trait MinimizerSpec extends SMTModelCheckingSpec {
         BitPat("b111") -> BitPat("b1")
       ),
       BitPat("b0")
-    ), "case0")
+    ))
   }
 
   "case1" should "pass" in {
@@ -64,7 +62,7 @@ trait MinimizerSpec extends SMTModelCheckingSpec {
         // BitPat("b111") -> BitPat("b1")
       ),
       BitPat("b1")
-    ), "case1")
+    ))
   }
 
   "caseX" should "pass" in {
@@ -80,7 +78,7 @@ trait MinimizerSpec extends SMTModelCheckingSpec {
         BitPat("b111") -> BitPat("b1")
       ),
       BitPat("b?")
-    ), "caseX")
+    ))
   }
 
   "caseMultiDefault" should "pass" in {
@@ -93,7 +91,7 @@ trait MinimizerSpec extends SMTModelCheckingSpec {
         BitPat("b111") -> BitPat("b1101")
       ),
       BitPat("b?100")
-    ), "caseMultiDefault")
+    ))
   }
 
   "case7SegDecoder" should "pass" in {
@@ -111,7 +109,7 @@ trait MinimizerSpec extends SMTModelCheckingSpec {
         BitPat("b1001") -> BitPat("b111101101"),
       ),
       BitPat("b???????10")
-    ), "case7SegDecoder")
+    ))
   }
 
   // A simple RV32I decode table example
@@ -272,6 +270,6 @@ trait MinimizerSpec extends SMTModelCheckingSpec {
         SRAI_RV32 -> Seq(Y, N, N, N, N, N, N, Y, N, A2_IMM, A1_RS1, IMM_I, DW_XPR, FN_SRA, N, M_X, N, N, N, N, N, N, Y, CSR_N, N, N, N, N),
       ).map { case (k, v) => BitPat(s"b$k") -> BitPat(s"b${v.reduce(_ + _)}") },
       BitPat(s"b${Seq(N, X, X, X, X, X, X, X, X, A2_X, A1_X, IMM_X, DW_X, FN_X, N, M_X, X, X, X, X, X, X, X, CSR_X, X, X, X, X).reduce(_ + _)}")
-    ), "rv32i")
+    ))
   }
 }
diff --git a/src/test/scala/chiselTests/util/experimental/minimizer/QMCSpec.scala b/integration-tests/src/test/scala/chiselTests/util/experimental/minimizer/QMCSpec.scala
index fc770202..fc770202 100644
--- a/src/test/scala/chiselTests/util/experimental/minimizer/QMCSpec.scala
+++ b/integration-tests/src/test/scala/chiselTests/util/experimental/minimizer/QMCSpec.scala
diff --git a/src/test/scala/chiselTests/SMTModelCheckingSpec.scala b/src/test/scala/chiselTests/SMTModelCheckingSpec.scala
deleted file mode 100644
index 0a752b10..00000000
--- a/src/test/scala/chiselTests/SMTModelCheckingSpec.scala
+++ /dev/null
@@ -1,104 +0,0 @@
-package chiselTests
-
-import chisel3.Module
-import chisel3.stage.{ChiselGeneratorAnnotation, ChiselStage}
-import firrtl.annotations.Annotation
-import firrtl.options.{OutputAnnotationFileAnnotation, TargetDirAnnotation}
-import firrtl.stage.OutputFileAnnotation
-import firrtl.util.BackendCompilationUtilities.timeStamp
-import logger.{LazyLogging, LogLevel, LogLevelAnnotation}
-import org.scalatest.flatspec.AnyFlatSpec
-import os._
-import scala.util.Properties
-
-/** [[SMTModelCheckingSpec]] use z3 and [[firrtl.backends.experimental.smt]] library
-  * to solve `assert/assume` in [[chisel3.experimental.verification]],
-  * It is a copy&paste version from `firrtl.backends.experimental.smt.end2end.EndToEndSMTBaseSpec` from firrtl
-  * Useful to check combinational logic and some small test.
-  */
-abstract class SMTModelCheckingSpec extends AnyFlatSpec {
-  def success = MCSuccess
-
-  def fail(k: Int) = MCFail(k)
-
-  def test(dut: () => Module, name: String, expected: MCResult, kmax: Int = 0, 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 _ =>
-    }
-    // @todo rewrite BackendCompilationUtilities
-    val testBaseDir = os.pwd / "test_run_dir" / name
-    os.makeDir.all(testBaseDir)
-    val testDir = os.temp.dir(testBaseDir, timeStamp, deleteOnExit = false)
-    val res = (new ChiselStage).execute(
-      Array("-E", "experimental-smt2"),
-      Seq(
-        LogLevelAnnotation(LogLevel.Error), // silence warnings for tests
-        ChiselGeneratorAnnotation(dut),
-        TargetDirAnnotation(testDir.toString)
-      ) ++ annos
-    )
-    val top = res.collectFirst{case OutputAnnotationFileAnnotation(top) => top}.get
-    assert(res.collectFirst { case _: OutputFileAnnotation => true }.isDefined)
-    val r = Z3ModelChecker.bmc(testDir, top, kmax)
-    assert(r == expected)
-  }
-}
-
-private object Z3ModelChecker extends LazyLogging {
-  def bmc(testDir: Path, main: String, kmax: Int): MCResult = {
-    assert(kmax >= 0 && kmax < 50, "Trying to keep kmax in a reasonable range.")
-    Seq.tabulate(kmax + 1) { k =>
-      val stepFile = testDir / s"${main}_step$k.smt2"
-      os.copy(testDir / s"$main.smt2", stepFile)
-      os.write.append(stepFile,
-        s"""${step(main, k)}
-           |(check-sat)
-           |""".stripMargin)
-      val success = executeStep(stepFile)
-      if (!success) return MCFail(k)
-    }
-    MCSuccess
-  }
-
-  private def executeStep(path: Path): Boolean = {
-    val (out, ret) = executeCmd(path.toString)
-    assert(ret == 0, s"expected success (0), not $ret: `$out`\nz3 ${path.toString}")
-    assert(out == "sat" + Properties.lineSeparator || out == "unsat" + Properties.lineSeparator, s"Unexpected output: $out")
-    out == "unsat" + Properties.lineSeparator
-  }
-
-  private def executeCmd(cmd: String): (String, Int) = {
-    val process = os.proc("z3", cmd).call(stderr = ProcessOutput.Readlines(logger.warn(_)))
-    (process.out.chunks.mkString, process.exitCode)
-  }
-
-  private def step(main: String, k: Int): 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)))")
-  }.mkString("\n")
-
-  // the following suffixes have to match the ones in [[SMTTransitionSystemEncoder]]
-  private val Transition = "_t"
-  private val Init = "_i"
-  private val Asserts = "_a"
-  private val Assumes = "_u"
-  private val StateTpe = "_s"
-}
-sealed trait MCResult
-
-case object MCSuccess extends MCResult
-
-case class MCFail(k: Int) extends MCResult
-
diff --git a/src/test/scala/chiselTests/util/experimental/DecoderSpec.scala b/src/test/scala/chiselTests/util/experimental/DecoderSpec.scala
deleted file mode 100644
index 3c9d490d..00000000
--- a/src/test/scala/chiselTests/util/experimental/DecoderSpec.scala
+++ /dev/null
@@ -1,61 +0,0 @@
-// SPDX-License-Identifier: Apache-2.0
-
-package chiselTests.util.experimental
-
-import chisel3.util.experimental.decode.{DecodeTableAnnotation, Minimizer, QMCMinimizer, TruthTable}
-import chiselTests.SMTModelCheckingSpec
-import chiselTests.util.experimental.minimizer.DecodeTestModule
-import firrtl.annotations.ReferenceTarget
-
-class DecoderSpec extends SMTModelCheckingSpec {
-  val xor = TruthTable(
-    """10->1
-      |01->1
-      |    0""".stripMargin)
-
-  def minimizer: Minimizer = QMCMinimizer
-
-  "decoder" should "pass without DecodeTableAnnotation" in {
-    test(
-      () => new DecodeTestModule(minimizer, table = xor),
-      s"${minimizer.getClass.getSimpleName}.noAnno",
-      success
-    )
-  }
-
-  "decoder" should "fail with a incorrect DecodeTableAnnotation" in {
-    test(
-      () => new DecodeTestModule(minimizer, table = xor),
-      s"${minimizer.getClass.getSimpleName}.incorrectAnno",
-      fail(0),
-      annos = Seq(
-        DecodeTableAnnotation(ReferenceTarget("", "", Nil, "", Nil),
-          """10->1
-            |01->1
-            |    0""".stripMargin,
-          """10->1
-            |    0""".stripMargin
-        )
-      )
-    )
-  }
-
-  "decoder" should "success with a correct DecodeTableAnnotation" in {
-    test(
-      () => new DecodeTestModule(minimizer, table = xor),
-      s"${minimizer.getClass.getSimpleName}.correctAnno",
-      success,
-      annos = Seq(
-        DecodeTableAnnotation(ReferenceTarget("", "", Nil, "", Nil),
-          """10->1
-            |01->1
-            |    0""".stripMargin,
-          QMCMinimizer.minimize(TruthTable(
-            """10->1
-              |01->1
-              |    0""".stripMargin)).toString
-        )
-      )
-    )
-  }
-}