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>

1 files changed, 0 insertions, 61 deletions

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
-        )
-      )
-    )
-  }
-}