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---
 core/src/main/scala/chisel3/internal/firrtl/Converter.scala | 8 ++++++++
 core/src/main/scala/chisel3/internal/firrtl/IR.scala        | 7 +++++++
 2 files changed, 15 insertions(+)

(limited to 'core/src/main/scala/chisel3/internal')

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