Basic model checking API (#1499)

* Add `check(...)` affordance

* Add assert (renamed from check and fixed)

* Add verification statements

* Move formal to experimental.verification

* Make test use ChiselStage

`generateFirrtl` has been cut from Chisel

* Fix newly introduced style warnings

* Fix some old style warnings for good measure

* Revert "Fix some old style warnings for good measure"

This reverts commit 31d51726c2faa4c277230104bd469ff7ffefc890.

* Cut scalastyle comments

* Cut formal delimiter comments

1 files changed, 38 insertions, 0 deletions

diff --git a/src/test/scala/chiselTests/experimental/verification/VerificationSpec.scala b/src/test/scala/chiselTests/experimental/verification/VerificationSpec.scala
new file mode 100644
index 00000000..521c16a3
--- /dev/null
+++ b/src/test/scala/chiselTests/experimental/verification/VerificationSpec.scala
@@ -0,0 +1,38 @@
+// See LICENSE for license details.
+
+package chiselTests.experimental.verification
+
+import chisel3._
+import chisel3.experimental.{verification => formal}
+import chisel3.stage.ChiselStage
+import chiselTests.ChiselPropSpec
+
+class VerificationModule extends Module {
+  val io = IO(new Bundle{
+    val in = Input(UInt(8.W))
+    val out = Output(UInt(8.W))
+  })
+  io.out := io.in
+  formal.cover(io.in === 3.U)
+  when (io.in === 3.U) {
+    formal.assume(io.in =/= 2.U)
+    formal.assert(io.out === io.in)
+  }
+}
+
+class VerificationSpec extends ChiselPropSpec {
+
+  def assertContains[T](s: Seq[T], x: T): Unit = {
+    val containsLine = s.map(_ == x).reduce(_ || _)
+    assert(containsLine, s"\n  $x\nwas not found in`\n  ${s.mkString("\n  ")}``")
+  }
+
+  property("basic equality check should work") {
+    val stage = new ChiselStage
+    val fir = stage.emitFirrtl(new VerificationModule)
+    val lines = fir.split("\n").map(_.trim)
+    assertContains(lines, "cover(clock, _T, UInt<1>(\"h1\"), \"\") @[VerificationSpec.scala 16:15]")
+    assertContains(lines, "assume(clock, _T_2, UInt<1>(\"h1\"), \"\") @[VerificationSpec.scala 18:18]")
+    assertContains(lines, "assert(clock, _T_3, UInt<1>(\"h1\"), \"\") @[VerificationSpec.scala 19:18]")
+  }
+}