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, 41 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))
+    }
+  }
+}