From 57c846b1389d507659fae8c7cad092fb83b5f909 Mon Sep 17 00:00:00 2001
From: Tom Alcorn
Date: Wed, 22 Jul 2020 12:08:10 -0700
Subject: 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---
 .../experimental/verification/package.scala        | 41 ++++++++++++++++++++++
 .../scala/chisel3/internal/firrtl/Converter.scala  |  8 +++++
 .../main/scala/chisel3/internal/firrtl/IR.scala    |  7 ++++
 3 files changed, 56 insertions(+)
 create mode 100644 core/src/main/scala/chisel3/experimental/verification/package.scala

(limited to 'core/src')

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
-- 
cgit v1.2.3