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>

5 files changed, 0 insertions, 460 deletions

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
-        )
-      )
-    )
-  }
-}
diff --git a/src/test/scala/chiselTests/util/experimental/minimizer/EspressoSpec.scala b/src/test/scala/chiselTests/util/experimental/minimizer/EspressoSpec.scala
deleted file mode 100644
index f3270cae..00000000
--- a/src/test/scala/chiselTests/util/experimental/minimizer/EspressoSpec.scala
+++ /dev/null
@@ -1,9 +0,0 @@
-// SPDX-License-Identifier: Apache-2.0
-
-package chiselTests.util.experimental.minimizer
-import chisel3.util.experimental.decode.EspressoMinimizer
-import chisel3.util.experimental.decode.Minimizer
-
-class EspressoSpec extends MinimizerSpec {
-  override def minimizer: Minimizer = EspressoMinimizer
-}
diff --git a/src/test/scala/chiselTests/util/experimental/minimizer/MinimizerSpec.scala b/src/test/scala/chiselTests/util/experimental/minimizer/MinimizerSpec.scala
deleted file mode 100644
index 5e3be9a6..00000000
--- a/src/test/scala/chiselTests/util/experimental/minimizer/MinimizerSpec.scala
+++ /dev/null
@@ -1,277 +0,0 @@
-// SPDX-License-Identifier: Apache-2.0
-
-package chiselTests.util.experimental.minimizer
-
-import chisel3._
-import chisel3.util._
-import chisel3.util.experimental.decode._
-import chisel3.util.pla
-import chiselTests.SMTModelCheckingSpec
-
-class DecodeTestModule(minimizer: Minimizer, table: TruthTable) extends Module {
-  val i = IO(Input(UInt(table.table.head._1.getWidth.W)))
-  val (unminimizedI, unminimizedO) = pla(table.table.toSeq)
-  unminimizedI := i
-  val minimizedO: UInt = decoder(minimizer, i, table)
-
-  chisel3.experimental.verification.assert(
-    // for each instruction, if input matches, output should match, not no matched, fallback to default
-    (table.table.map { case (key, value) => (i === key) && (minimizedO === value) } ++
-      Seq(table.table.keys.map(i =/= _).reduce(_ && _) && minimizedO === table.default)).reduce(_ || _)
-  )
-}
-
-trait MinimizerSpec extends SMTModelCheckingSpec {
-  def minimizer: Minimizer
-
-  def minimizerTest(testcase: TruthTable, caseName: String) = {
-    test(
-      () => new DecodeTestModule(minimizer, table = testcase),
-      s"${minimizer.getClass.getSimpleName}.$caseName",
-      success
-    )
-  }
-
-  // Term that being commented out is the result of which is same as default,
-  // making optimization opportunities to decoder algorithms
-
-  "case0" should "pass" in {
-    minimizerTest(TruthTable(
-      Map(
-        // BitPat("b000") -> BitPat("b0"),
-        BitPat("b001") -> BitPat("b?"),
-        BitPat("b010") -> BitPat("b?"),
-        // BitPat("b011") -> BitPat("b0"),
-        BitPat("b100") -> BitPat("b1"),
-        BitPat("b101") -> BitPat("b1"),
-        // BitPat("b110") -> BitPat("b0"),
-        BitPat("b111") -> BitPat("b1")
-      ),
-      BitPat("b0")
-    ), "case0")
-  }
-
-  "case1" should "pass" in {
-    minimizerTest(TruthTable(
-      Map(
-        BitPat("b000") -> BitPat("b0"),
-        BitPat("b001") -> BitPat("b?"),
-        BitPat("b010") -> BitPat("b?"),
-        BitPat("b011") -> BitPat("b0"),
-        // BitPat("b100") -> BitPat("b1"),
-        // BitPat("b101") -> BitPat("b1"),
-        BitPat("b110") -> BitPat("b0"),
-        // BitPat("b111") -> BitPat("b1")
-      ),
-      BitPat("b1")
-    ), "case1")
-  }
-
-  "caseX" should "pass" in {
-    minimizerTest(TruthTable(
-      Map(
-        BitPat("b000") -> BitPat("b0"),
-        // BitPat("b001") -> BitPat("b?"),
-        // BitPat("b010") -> BitPat("b?"),
-        BitPat("b011") -> BitPat("b0"),
-        BitPat("b100") -> BitPat("b1"),
-        BitPat("b101") -> BitPat("b1"),
-        BitPat("b110") -> BitPat("b0"),
-        BitPat("b111") -> BitPat("b1")
-      ),
-      BitPat("b?")
-    ), "caseX")
-  }
-
-  "caseMultiDefault" should "pass" in {
-    minimizerTest(TruthTable(
-      Map(
-        BitPat("b000") -> BitPat("b0100"),
-        BitPat("b001") -> BitPat("b?111"),
-        BitPat("b010") -> BitPat("b?000"),
-        BitPat("b011") -> BitPat("b0101"),
-        BitPat("b111") -> BitPat("b1101")
-      ),
-      BitPat("b?100")
-    ), "caseMultiDefault")
-  }
-
-  "case7SegDecoder" should "pass" in {
-    minimizerTest(TruthTable(
-      Map(
-        BitPat("b0000") -> BitPat("b111111001"),
-        BitPat("b0001") -> BitPat("b011000001"),
-        BitPat("b0010") -> BitPat("b110110101"),
-        BitPat("b0011") -> BitPat("b111100101"),
-        BitPat("b0100") -> BitPat("b011001101"),
-        BitPat("b0101") -> BitPat("b101101101"),
-        BitPat("b0110") -> BitPat("b101111101"),
-        BitPat("b0111") -> BitPat("b111000001"),
-        BitPat("b1000") -> BitPat("b111111101"),
-        BitPat("b1001") -> BitPat("b111101101"),
-      ),
-      BitPat("b???????10")
-    ), "case7SegDecoder")
-  }
-
-  // A simple RV32I decode table example
-  "caseRV32I" should "pass" in {
-    val BEQ = "?????????????????000?????1100011"
-    val BNE = "?????????????????001?????1100011"
-    val BLT = "?????????????????100?????1100011"
-    val BGE = "?????????????????101?????1100011"
-    val BLTU = "?????????????????110?????1100011"
-    val BGEU = "?????????????????111?????1100011"
-    val JALR = "?????????????????000?????1100111"
-    val JAL = "?????????????????????????1101111"
-    val LUI = "?????????????????????????0110111"
-    val AUIPC = "?????????????????????????0010111"
-    val ADDI = "?????????????????000?????0010011"
-    val SLTI = "?????????????????010?????0010011"
-    val SLTIU = "?????????????????011?????0010011"
-    val XORI = "?????????????????100?????0010011"
-    val ORI = "?????????????????110?????0010011"
-    val ANDI = "?????????????????111?????0010011"
-    val ADD = "0000000??????????000?????0110011"
-    val SUB = "0100000??????????000?????0110011"
-    val SLL = "0000000??????????001?????0110011"
-    val SLT = "0000000??????????010?????0110011"
-    val SLTU = "0000000??????????011?????0110011"
-    val XOR = "0000000??????????100?????0110011"
-    val SRL = "0000000??????????101?????0110011"
-    val SRA = "0100000??????????101?????0110011"
-    val OR = "0000000??????????110?????0110011"
-    val AND = "0000000??????????111?????0110011"
-    val LB = "?????????????????000?????0000011"
-    val LH = "?????????????????001?????0000011"
-    val LW = "?????????????????010?????0000011"
-    val LBU = "?????????????????100?????0000011"
-    val LHU = "?????????????????101?????0000011"
-    val SB = "?????????????????000?????0100011"
-    val SH = "?????????????????001?????0100011"
-    val SW = "?????????????????010?????0100011"
-    val FENCE = "?????????????????000?????0001111"
-    val MRET = "00110000001000000000000001110011"
-    val WFI = "00010000010100000000000001110011"
-    val CEASE = "00110000010100000000000001110011"
-    val CSRRW = "?????????????????001?????1110011"
-    val CSRRS = "?????????????????010?????1110011"
-    val CSRRC = "?????????????????011?????1110011"
-    val CSRRWI = "?????????????????101?????1110011"
-    val CSRRSI = "?????????????????110?????1110011"
-    val CSRRCI = "?????????????????111?????1110011"
-    val SCALL = "00000000000000000000000001110011"
-    val SBREAK = "00000000000100000000000001110011"
-    val SLLI_RV32 = "0000000??????????001?????0010011"
-    val SRLI_RV32 = "0000000??????????101?????0010011"
-    val SRAI_RV32 = "0100000??????????101?????0010011"
-
-    val A1_X = "??"
-    val A1_ZERO = "00"
-    val A1_RS1 = "01"
-    val A1_PC = "10"
-
-    val IMM_X = "???"
-    val IMM_S = "000"
-    val IMM_SB = "001"
-    val IMM_U = "010"
-    val IMM_UJ = "011"
-    val IMM_I = "100"
-    val IMM_Z = "101"
-
-    val A2_X = "??"
-    val A2_ZERO = "00"
-    val A2_SIZE = "01"
-    val A2_RS2 = "10"
-    val A2_IMM = "11"
-
-    val X = "?"
-    val N = "0"
-    val Y = "1"
-
-    val DW_X = X
-    val DW_XPR = Y
-
-    val M_X = "?????"
-    val M_XRD = "00000"
-    val M_XWR = "00001"
-
-    val CSR_X = "???"
-    val CSR_N = "000"
-    val CSR_I = "100"
-    val CSR_W = "101"
-    val CSR_S = "110"
-    val CSR_C = "111"
-
-    val FN_X = "????"
-    val FN_ADD = "0000"
-    val FN_SL = "0001"
-    val FN_SEQ = "0010"
-    val FN_SNE = "0011"
-    val FN_XOR = "0100"
-    val FN_SR = "0101"
-    val FN_OR = "0110"
-    val FN_AND = "0111"
-    val FN_SUB = "1010"
-    val FN_SRA = "1011"
-    val FN_SLT = "1100"
-    val FN_SGE = "1101"
-    val FN_SLTU = "1110"
-    val FN_SGEU = "1111"
-
-    minimizerTest(TruthTable(
-      Map(
-        BNE -> Seq(Y, N, N, Y, N, N, Y, Y, N, A2_RS2, A1_RS1, IMM_SB, DW_X, FN_SNE, N, M_X, N, N, N, N, N, N, N, CSR_N, N, N, N, N),
-        BEQ -> Seq(Y, N, N, Y, N, N, Y, Y, N, A2_RS2, A1_RS1, IMM_SB, DW_X, FN_SEQ, N, M_X, N, N, N, N, N, N, N, CSR_N, N, N, N, N),
-        BLT -> Seq(Y, N, N, Y, N, N, Y, Y, N, A2_RS2, A1_RS1, IMM_SB, DW_X, FN_SLT, N, M_X, N, N, N, N, N, N, N, CSR_N, N, N, N, N),
-        BLTU -> Seq(Y, N, N, Y, N, N, Y, Y, N, A2_RS2, A1_RS1, IMM_SB, DW_X, FN_SLTU, N, M_X, N, N, N, N, N, N, N, CSR_N, N, N, N, N),
-        BGE -> Seq(Y, N, N, Y, N, N, Y, Y, N, A2_RS2, A1_RS1, IMM_SB, DW_X, FN_SGE, N, M_X, N, N, N, N, N, N, N, CSR_N, N, N, N, N),
-        BGEU -> Seq(Y, N, N, Y, N, N, Y, Y, N, A2_RS2, A1_RS1, IMM_SB, DW_X, FN_SGEU, N, M_X, N, N, N, N, N, N, N, CSR_N, N, N, N, N),
-        JAL -> Seq(Y, N, N, N, Y, N, N, N, N, A2_SIZE, A1_PC, IMM_UJ, DW_XPR, FN_ADD, N, M_X, N, N, N, N, N, N, Y, CSR_N, N, N, N, N),
-        JALR -> Seq(Y, N, N, N, N, Y, N, Y, N, A2_IMM, A1_RS1, IMM_I, DW_XPR, FN_ADD, N, M_X, N, N, N, N, N, N, Y, CSR_N, N, N, N, N),
-        AUIPC -> Seq(Y, N, N, N, N, N, N, N, N, A2_IMM, A1_PC, IMM_U, DW_XPR, FN_ADD, N, M_X, N, N, N, N, N, N, Y, CSR_N, N, N, N, N),
-        LB -> Seq(Y, N, N, N, N, N, N, Y, N, A2_IMM, A1_RS1, IMM_I, DW_XPR, FN_ADD, Y, M_XRD, N, N, N, N, N, N, Y, CSR_N, N, N, N, N),
-        LH -> Seq(Y, N, N, N, N, N, N, Y, N, A2_IMM, A1_RS1, IMM_I, DW_XPR, FN_ADD, Y, M_XRD, N, N, N, N, N, N, Y, CSR_N, N, N, N, N),
-        LW -> Seq(Y, N, N, N, N, N, N, Y, N, A2_IMM, A1_RS1, IMM_I, DW_XPR, FN_ADD, Y, M_XRD, N, N, N, N, N, N, Y, CSR_N, N, N, N, N),
-        LBU -> Seq(Y, N, N, N, N, N, N, Y, N, A2_IMM, A1_RS1, IMM_I, DW_XPR, FN_ADD, Y, M_XRD, N, N, N, N, N, N, Y, CSR_N, N, N, N, N),
-        LHU -> Seq(Y, N, N, N, N, N, N, Y, N, A2_IMM, A1_RS1, IMM_I, DW_XPR, FN_ADD, Y, M_XRD, N, N, N, N, N, N, Y, CSR_N, N, N, N, N),
-        SB -> Seq(Y, N, N, N, N, N, Y, Y, N, A2_IMM, A1_RS1, IMM_S, DW_XPR, FN_ADD, Y, M_XWR, N, N, N, N, N, N, N, CSR_N, N, N, N, N),
-        SH -> Seq(Y, N, N, N, N, N, Y, Y, N, A2_IMM, A1_RS1, IMM_S, DW_XPR, FN_ADD, Y, M_XWR, N, N, N, N, N, N, N, CSR_N, N, N, N, N),
-        SW -> Seq(Y, N, N, N, N, N, Y, Y, N, A2_IMM, A1_RS1, IMM_S, DW_XPR, FN_ADD, Y, M_XWR, N, N, N, N, N, N, N, CSR_N, N, N, N, N),
-        LUI -> Seq(Y, N, N, N, N, N, N, N, N, A2_IMM, A1_ZERO, IMM_U, DW_XPR, FN_ADD, N, M_X, N, N, N, N, N, N, Y, CSR_N, N, N, N, N),
-        ADDI -> Seq(Y, N, N, N, N, N, N, Y, N, A2_IMM, A1_RS1, IMM_I, DW_XPR, FN_ADD, N, M_X, N, N, N, N, N, N, Y, CSR_N, N, N, N, N),
-        SLTI -> Seq(Y, N, N, N, N, N, N, Y, N, A2_IMM, A1_RS1, IMM_I, DW_XPR, FN_SLT, N, M_X, N, N, N, N, N, N, Y, CSR_N, N, N, N, N),
-        SLTIU -> Seq(Y, N, N, N, N, N, N, Y, N, A2_IMM, A1_RS1, IMM_I, DW_XPR, FN_SLTU, N, M_X, N, N, N, N, N, N, Y, CSR_N, N, N, N, N),
-        ANDI -> Seq(Y, N, N, N, N, N, N, Y, N, A2_IMM, A1_RS1, IMM_I, DW_XPR, FN_AND, N, M_X, N, N, N, N, N, N, Y, CSR_N, N, N, N, N),
-        ORI -> Seq(Y, N, N, N, N, N, N, Y, N, A2_IMM, A1_RS1, IMM_I, DW_XPR, FN_OR, N, M_X, N, N, N, N, N, N, Y, CSR_N, N, N, N, N),
-        XORI -> Seq(Y, N, N, N, N, N, N, Y, N, A2_IMM, A1_RS1, IMM_I, DW_XPR, FN_XOR, N, M_X, N, N, N, N, N, N, Y, CSR_N, N, N, N, N),
-        ADD -> Seq(Y, N, N, N, N, N, Y, Y, N, A2_RS2, A1_RS1, IMM_X, DW_XPR, FN_ADD, N, M_X, N, N, N, N, N, N, Y, CSR_N, N, N, N, N),
-        SUB -> Seq(Y, N, N, N, N, N, Y, Y, N, A2_RS2, A1_RS1, IMM_X, DW_XPR, FN_SUB, N, M_X, N, N, N, N, N, N, Y, CSR_N, N, N, N, N),
-        SLT -> Seq(Y, N, N, N, N, N, Y, Y, N, A2_RS2, A1_RS1, IMM_X, DW_XPR, FN_SLT, N, M_X, N, N, N, N, N, N, Y, CSR_N, N, N, N, N),
-        SLTU -> Seq(Y, N, N, N, N, N, Y, Y, N, A2_RS2, A1_RS1, IMM_X, DW_XPR, FN_SLTU, N, M_X, N, N, N, N, N, N, Y, CSR_N, N, N, N, N),
-        AND -> Seq(Y, N, N, N, N, N, Y, Y, N, A2_RS2, A1_RS1, IMM_X, DW_XPR, FN_AND, N, M_X, N, N, N, N, N, N, Y, CSR_N, N, N, N, N),
-        OR -> Seq(Y, N, N, N, N, N, Y, Y, N, A2_RS2, A1_RS1, IMM_X, DW_XPR, FN_OR, N, M_X, N, N, N, N, N, N, Y, CSR_N, N, N, N, N),
-        XOR -> Seq(Y, N, N, N, N, N, Y, Y, N, A2_RS2, A1_RS1, IMM_X, DW_XPR, FN_XOR, N, M_X, N, N, N, N, N, N, Y, CSR_N, N, N, N, N),
-        SLL -> Seq(Y, N, N, N, N, N, Y, Y, N, A2_RS2, A1_RS1, IMM_X, DW_XPR, FN_SL, N, M_X, N, N, N, N, N, N, Y, CSR_N, N, N, N, N),
-        SRL -> Seq(Y, N, N, N, N, N, Y, Y, N, A2_RS2, A1_RS1, IMM_X, DW_XPR, FN_SR, N, M_X, N, N, N, N, N, N, Y, CSR_N, N, N, N, N),
-        SRA -> Seq(Y, N, N, N, N, N, Y, Y, N, A2_RS2, A1_RS1, IMM_X, DW_XPR, FN_SRA, N, M_X, N, N, N, N, N, N, Y, CSR_N, N, N, N, N),
-        FENCE -> Seq(Y, N, N, N, N, N, N, N, N, A2_X, A1_X, IMM_X, DW_X, FN_X, N, M_X, N, N, N, N, N, N, N, CSR_N, N, Y, N, N),
-        SCALL -> Seq(Y, N, N, N, N, N, N, X, N, A2_X, A1_X, IMM_X, DW_X, FN_X, N, M_X, N, N, N, N, N, N, N, CSR_I, N, N, N, N),
-        SBREAK -> Seq(Y, N, N, N, N, N, N, X, N, A2_X, A1_X, IMM_X, DW_X, FN_X, N, M_X, N, N, N, N, N, N, N, CSR_I, N, N, N, N),
-        MRET -> Seq(Y, N, N, N, N, N, N, X, N, A2_X, A1_X, IMM_X, DW_X, FN_X, N, M_X, N, N, N, N, N, N, N, CSR_I, N, N, N, N),
-        WFI -> Seq(Y, N, N, N, N, N, N, X, N, A2_X, A1_X, IMM_X, DW_X, FN_X, N, M_X, N, N, N, N, N, N, N, CSR_I, N, N, N, N),
-        CEASE -> Seq(Y, N, N, N, N, N, N, X, N, A2_X, A1_X, IMM_X, DW_X, FN_X, N, M_X, N, N, N, N, N, N, N, CSR_I, N, N, N, N),
-        CSRRW -> Seq(Y, N, N, N, N, N, N, Y, N, A2_ZERO, A1_RS1, IMM_X, DW_XPR, FN_ADD, N, M_X, N, N, N, N, N, N, Y, CSR_W, N, N, N, N),
-        CSRRS -> Seq(Y, N, N, N, N, N, N, Y, N, A2_ZERO, A1_RS1, IMM_X, DW_XPR, FN_ADD, N, M_X, N, N, N, N, N, N, Y, CSR_S, N, N, N, N),
-        CSRRC -> Seq(Y, N, N, N, N, N, N, Y, N, A2_ZERO, A1_RS1, IMM_X, DW_XPR, FN_ADD, N, M_X, N, N, N, N, N, N, Y, CSR_C, N, N, N, N),
-        CSRRWI -> Seq(Y, N, N, N, N, N, N, N, N, A2_IMM, A1_ZERO, IMM_Z, DW_XPR, FN_ADD, N, M_X, N, N, N, N, N, N, Y, CSR_W, N, N, N, N),
-        CSRRSI -> Seq(Y, N, N, N, N, N, N, N, N, A2_IMM, A1_ZERO, IMM_Z, DW_XPR, FN_ADD, N, M_X, N, N, N, N, N, N, Y, CSR_S, N, N, N, N),
-        CSRRCI -> Seq(Y, N, N, N, N, N, N, N, N, A2_IMM, A1_ZERO, IMM_Z, DW_XPR, FN_ADD, N, M_X, N, N, N, N, N, N, Y, CSR_C, N, N, N, N),
-        SLLI_RV32 -> Seq(Y, N, N, N, N, N, N, Y, N, A2_IMM, A1_RS1, IMM_I, DW_XPR, FN_SL, N, M_X, N, N, N, N, N, N, Y, CSR_N, N, N, N, N),
-        SRLI_RV32 -> Seq(Y, N, N, N, N, N, N, Y, N, A2_IMM, A1_RS1, IMM_I, DW_XPR, FN_SR, N, M_X, N, N, N, N, N, N, Y, CSR_N, N, N, N, N),
-        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/src/test/scala/chiselTests/util/experimental/minimizer/QMCSpec.scala
deleted file mode 100644
index fc770202..00000000
--- a/src/test/scala/chiselTests/util/experimental/minimizer/QMCSpec.scala
+++ /dev/null
@@ -1,9 +0,0 @@
-// SPDX-License-Identifier: Apache-2.0
-
-package chiselTests.util.experimental.minimizer
-import chisel3.util.experimental.decode.Minimizer
-import chisel3.util.experimental.decode.QMCMinimizer
-
-class QMCSpec extends MinimizerSpec {
-  override def minimizer: Minimizer = QMCMinimizer
-}