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

2 files changed, 40 insertions, 0 deletions

diff --git a/src/main/scala/chisel3/internal/firrtl/Emitter.scala b/src/main/scala/chisel3/internal/firrtl/Emitter.scala
index be8d8f2f..36ac8710 100644
--- a/src/main/scala/chisel3/internal/firrtl/Emitter.scala
+++ b/src/main/scala/chisel3/internal/firrtl/Emitter.scala
@@ -80,6 +80,8 @@ private class Emitter(circuit: Circuit) {
         val printfArgs = Seq(e.clock.fullName(ctx), "UInt<1>(1)",
           "\"" + printf.format(fmt) + "\"") ++ args
         printfArgs mkString ("printf(", ", ", ")")
+      case e: Verification => s"${e.op}(${e.clock.fullName(ctx)}, ${e.predicate.fullName(ctx)}, " +
+        s"UInt<1>(1), " + "\"" + s"${printf.format(e.message)}" + "\")"
       case e: DefInvalid => s"${e.arg.fullName(ctx)} is invalid"
       case e: DefInstance => s"inst ${e.name} of ${e.id.name}"
       case w: WhenBegin =>
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]")
+  }
+}