Basic model checking API (#1653)

* Add assume, assert, cover statements
* Assert submodule assumptions
* Add warning when removing verification statements
* Remove System Verilog behaviour emitter warning
* Add option to disable AssertSubmoduleAssumptions
* Document verification statements in the spec

The syntax for the new statements is

    assert(clk, cond, en, msg)
    assume(clk, cond, en, msg)
    cover(clk, cond, en, msg)

With assert as a representative example, the semantics is as follows:
`clk` is the clock, `cond` is the expression being asserted, `en` is the
enable signal (if `en` is low then the assert is not checked) and `msg`
is a string message intended to be reported as an error message by the
model checker if the assertion fails.

In the Verilog emitter, the new statements are handled by a new
`formals` map, which groups the statements by clock domain. All model
checking statements are then emitted within the context of an `ifdef
FORMAL` block, which allows model checking tools (like Symbiyosys) to
utilize the statements while keeping them out of synthesis flows.

Co-authored-by: Albert Magyar <albert.magyar@gmail.com>

2 files changed, 25 insertions, 2 deletions

diff --git a/src/main/scala/firrtl/proto/FromProto.scala b/src/main/scala/firrtl/proto/FromProto.scala
index ea4cec1f..5de92b57 100644
--- a/src/main/scala/firrtl/proto/FromProto.scala
+++ b/src/main/scala/firrtl/proto/FromProto.scala
@@ -8,7 +8,7 @@ import java.io.{File, FileInputStream, InputStream}
 import collection.JavaConverters._
 import FirrtlProtos._
 import com.google.protobuf.CodedInputStream
-import Firrtl.Statement.ReadUnderWrite
+import Firrtl.Statement.{ReadUnderWrite, Formal}
 
 object FromProto {
 
@@ -181,6 +181,16 @@ object FromProto {
   def convert(stop: Firrtl.Statement.Stop, info: Firrtl.SourceInfo): ir.Stop =
     ir.Stop(convert(info), stop.getReturnValue, convert(stop.getClk), convert(stop.getEn))
 
+  def convert(formal: Formal): ir.Formal.Value = formal match {
+    case Formal.ASSERT => ir.Formal.Assert
+    case Formal.ASSUME => ir.Formal.Assume
+    case Formal.COVER => ir.Formal.Cover
+  }
+
+  def convert(ver: Firrtl.Statement.Verification, info: Firrtl.SourceInfo): ir.Verification =
+    ir.Verification(convert(ver.getOp), convert(info), convert(ver.getClk),
+      convert(ver.getCond), convert(ver.getEn), ir.StringLit(ver.getMsg))
+
   def convert(mem: Firrtl.Statement.Memory, info: Firrtl.SourceInfo): ir.DefMemory = {
     val dtype = convert(mem.getType)
     val rs = mem.getReaderIdList.asScala
diff --git a/src/main/scala/firrtl/proto/ToProto.scala b/src/main/scala/firrtl/proto/ToProto.scala
index e2481d08..6cc6d11f 100644
--- a/src/main/scala/firrtl/proto/ToProto.scala
+++ b/src/main/scala/firrtl/proto/ToProto.scala
@@ -6,7 +6,7 @@ package proto
 import java.io.OutputStream
 
 import FirrtlProtos._
-import Firrtl.Statement.ReadUnderWrite
+import Firrtl.Statement.{ReadUnderWrite, Formal}
 import Firrtl.Expression.PrimOp.Op
 import com.google.protobuf.{CodedOutputStream, WireFormat}
 import firrtl.PrimOps._
@@ -114,6 +114,12 @@ object ToProto {
     case ir.ReadUnderWrite.New => ReadUnderWrite.NEW
   }
 
+  def convert(formal: ir.Formal.Value): Formal = formal match {
+    case ir.Formal.Assert => Formal.ASSERT
+    case ir.Formal.Assume => Formal.ASSUME
+    case ir.Formal.Cover => Formal.COVER
+  }
+
   def convertToIntegerLiteral(value: BigInt): Firrtl.Expression.IntegerLiteral.Builder = {
     Firrtl.Expression.IntegerLiteral.newBuilder()
       .setValue(value.toString)
@@ -272,6 +278,13 @@ object ToProto {
               .setClk(convert(clk))
               .setEn(convert(en))
             sb.setStop(stopb)
+          case ir.Verification(op, _, clk, cond, en, msg) =>
+            val vb = Firrtl.Statement.Verification.newBuilder()
+              .setOp(convert(op))
+              .setClk(convert(clk))
+              .setCond(convert(cond))
+              .setEn(convert(en))
+              .setMsg(msg.string)
           case ir.IsInvalid(_, expr) =>
             val ib = Firrtl.Statement.IsInvalid.newBuilder()
               .setExpression(convert(expr))