diff options
| -rw-r--r-- | .github/workflows/test.yml | 29 | ||||
| -rw-r--r-- | build.sbt | 13 | ||||
| -rw-r--r-- | integration-tests/src/test/scala/chiselTests/util/experimental/DecoderSpec.scala | 53 | ||||
| -rw-r--r-- | integration-tests/src/test/scala/chiselTests/util/experimental/minimizer/EspressoSpec.scala (renamed from src/test/scala/chiselTests/util/experimental/minimizer/EspressoSpec.scala) | 0 | ||||
| -rw-r--r-- | integration-tests/src/test/scala/chiselTests/util/experimental/minimizer/MinimizerSpec.scala (renamed from src/test/scala/chiselTests/util/experimental/minimizer/MinimizerSpec.scala) | 26 | ||||
| -rw-r--r-- | integration-tests/src/test/scala/chiselTests/util/experimental/minimizer/QMCSpec.scala (renamed from src/test/scala/chiselTests/util/experimental/minimizer/QMCSpec.scala) | 0 | ||||
| -rw-r--r-- | src/test/scala/chiselTests/SMTModelCheckingSpec.scala | 104 | ||||
| -rw-r--r-- | src/test/scala/chiselTests/util/experimental/DecoderSpec.scala | 61 |
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! @@ -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 - ) - ) - ) - } -} |