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

3 files changed, 56 insertions, 0 deletions

diff --git a/core/src/main/scala/chisel3/experimental/verification/package.scala b/core/src/main/scala/chisel3/experimental/verification/package.scala
new file mode 100644
index 00000000..a983a6fd
--- /dev/null
+++ b/core/src/main/scala/chisel3/experimental/verification/package.scala
@@ -0,0 +1,41 @@
+// See LICENSE for license details.
+
+package chisel3.experimental
+
+import chisel3.{Bool, CompileOptions}
+import chisel3.internal.Builder
+import chisel3.internal.Builder.pushCommand
+import chisel3.internal.firrtl.{Formal, Verification}
+import chisel3.internal.sourceinfo.SourceInfo
+
+package object verification {
+  object assert {
+    def apply(predicate: Bool, msg: String = "")(
+      implicit sourceInfo: SourceInfo,
+      compileOptions: CompileOptions): Unit = {
+      val clock = Builder.forcedClock
+      pushCommand(Verification(Formal.Assert, sourceInfo, clock.ref,
+        predicate.ref, msg))
+    }
+  }
+
+  object assume {
+    def apply(predicate: Bool, msg: String = "")(
+      implicit sourceInfo: SourceInfo,
+      compileOptions: CompileOptions): Unit = {
+      val clock = Builder.forcedClock
+      pushCommand(Verification(Formal.Assume, sourceInfo, clock.ref,
+        predicate.ref, msg))
+    }
+  }
+
+  object cover {
+    def apply(predicate: Bool, msg: String = "")(
+      implicit sourceInfo: SourceInfo,
+      compileOptions: CompileOptions): Unit = {
+      val clock = Builder.forcedClock
+      pushCommand(Verification(Formal.Cover, sourceInfo, clock.ref,
+        predicate.ref, msg))
+    }
+  }
+}
diff --git a/core/src/main/scala/chisel3/internal/firrtl/Converter.scala b/core/src/main/scala/chisel3/internal/firrtl/Converter.scala
index 67d87a68..304ddec6 100644
--- a/core/src/main/scala/chisel3/internal/firrtl/Converter.scala
+++ b/core/src/main/scala/chisel3/internal/firrtl/Converter.scala
@@ -125,6 +125,14 @@ private[chisel3] object Converter {
       val (fmt, args) = unpack(pable, ctx)
       Some(fir.Print(convert(info), fir.StringLit(fmt),
                      args.map(a => convert(a, ctx)), convert(clock, ctx), firrtl.Utils.one))
+    case Verification(op, info, clk, pred, msg) =>
+      val firOp = op match {
+        case Formal.Assert => fir.Formal.Assert
+        case Formal.Assume => fir.Formal.Assume
+        case Formal.Cover => fir.Formal.Cover
+      }
+      Some(fir.Verification(firOp, convert(info), convert(clk, ctx),
+        convert(pred, ctx), firrtl.Utils.one, fir.StringLit(msg)))
     case _ => None
   }
 
diff --git a/core/src/main/scala/chisel3/internal/firrtl/IR.scala b/core/src/main/scala/chisel3/internal/firrtl/IR.scala
index 89bc4a63..44fdb833 100644
--- a/core/src/main/scala/chisel3/internal/firrtl/IR.scala
+++ b/core/src/main/scala/chisel3/internal/firrtl/IR.scala
@@ -735,6 +735,13 @@ case class ConnectInit(sourceInfo: SourceInfo, loc: Node, exp: Arg) extends Comm
 case class Stop(sourceInfo: SourceInfo, clock: Arg, ret: Int) extends Command
 case class Port(id: Data, dir: SpecifiedDirection)
 case class Printf(sourceInfo: SourceInfo, clock: Arg, pable: Printable) extends Command
+object Formal extends Enumeration {
+  val Assert = Value("assert")
+  val Assume = Value("assume")
+  val Cover = Value("cover")
+}
+case class Verification(op: Formal.Value, sourceInfo: SourceInfo, clock: Arg,
+                        predicate: Arg, message: String) extends Command
 abstract class Component extends Arg {
   def id: BaseModule
   def name: String