From 3840fec3d918f23df07a18311136ac6a1bc365e1 Mon Sep 17 00:00:00 2001
From: Kevin Laeufer
Date: Wed, 25 Aug 2021 12:38:56 -0700
Subject: 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>---
 .../util/experimental/DecoderSpec.scala            | 53 ++++++++++++++++++++++
 1 file changed, 53 insertions(+)
 create mode 100644 integration-tests/src/test/scala/chiselTests/util/experimental/DecoderSpec.scala

(limited to 'integration-tests/src/test/scala/chiselTests/util/experimental/DecoderSpec.scala')

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)
+  }
+}
-- 
cgit v1.2.3