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>

25 files changed, 545 insertions, 24 deletions

diff --git a/src/main/antlr4/FIRRTL.g4 b/src/main/antlr4/FIRRTL.g4
index 39988e18..f0ea5b10 100644
--- a/src/main/antlr4/FIRRTL.g4
+++ b/src/main/antlr4/FIRRTL.g4
@@ -107,6 +107,9 @@ stmt
   | 'printf(' exp exp StringLit ( exp)* ')' info?
   | 'skip' info?
   | 'attach' '(' exp+ ')' info?
+  | 'assert' '(' exp exp exp StringLit ')' info?
+  | 'assume' '(' exp exp exp StringLit ')' info?
+  | 'cover' '(' exp exp exp StringLit ')' info?
   ;
 
 memField
diff --git a/src/main/proto/firrtl.proto b/src/main/proto/firrtl.proto
index 3d2c89f1..b4c8f36d 100644
--- a/src/main/proto/firrtl.proto
+++ b/src/main/proto/firrtl.proto
@@ -188,6 +188,25 @@ message Firrtl {
       Expression en = 4;
     }
 
+    enum Formal {
+      ASSERT = 0;
+      ASSUME = 1;
+      COVER = 2;
+    }
+
+    message Verification {
+      // Required.
+      Formal op = 1;
+      // Required.
+      Expression clk = 2;
+      // Required.
+      Expression cond = 3;
+      // Required.
+      Expression en = 4;
+      // Required.
+      string msg = 5;
+    }
+
     message Skip {
       // Empty
     }
diff --git a/src/main/resources/META-INF/services/firrtl.options.RegisteredTransform b/src/main/resources/META-INF/services/firrtl.options.RegisteredTransform
index 638404be..bb72d45c 100644
--- a/src/main/resources/META-INF/services/firrtl.options.RegisteredTransform
+++ b/src/main/resources/META-INF/services/firrtl.options.RegisteredTransform
@@ -2,3 +2,4 @@ firrtl.transforms.DeadCodeElimination
 firrtl.transforms.CheckCombLoops
 firrtl.passes.InlineInstances
 firrtl.passes.clocklist.ClockListTransform
+firrtl.transforms.formal.AssertSubmoduleAssumptions
diff --git a/src/main/scala/firrtl/Emitter.scala b/src/main/scala/firrtl/Emitter.scala
index 3b065bf4..268841da 100644
--- a/src/main/scala/firrtl/Emitter.scala
+++ b/src/main/scala/firrtl/Emitter.scala
@@ -5,7 +5,6 @@ package firrtl
 import java.io.Writer
 
 import scala.collection.mutable
-
 import firrtl.ir._
 import firrtl.passes._
 import firrtl.transforms.LegalizeAndReductionsTransform
@@ -15,8 +14,9 @@ import firrtl.PrimOps._
 import firrtl.WrappedExpression._
 import Utils._
 import MemPortUtils.{memPortField, memType}
-import firrtl.options.{Dependency, HasShellOptions, ShellOption, StageUtils, PhaseException, Unserializable}
+import firrtl.options.{Dependency, HasShellOptions, PhaseException, ShellOption, Unserializable}
 import firrtl.stage.{RunFirrtlTransformAnnotation, TransformManager}
+import firrtl.transforms.formal.RemoveVerificationStatements
 // Datastructures
 import scala.collection.mutable.ArrayBuffer
 
@@ -182,6 +182,7 @@ class VerilogEmitter extends SeqTransform with Emitter {
   def outputForm = LowForm
 
   override def prerequisites =
+    Dependency[RemoveVerificationStatements] +:
     Dependency[LegalizeAndReductionsTransform] +:
     firrtl.stage.Forms.LowFormOptimized
 
@@ -454,6 +455,13 @@ class VerilogEmitter extends SeqTransform with Emitter {
       case m: Module => new VerilogRender(m, moduleMap)(writer)
     }
   }
+
+  def addFormalStatement(formals: mutable.Map[Expression, ArrayBuffer[Seq[Any]]],
+                                 clk: Expression, en: Expression,
+                                 stmt: Seq[Any], info: Info): Unit = {
+    throw EmitterException("Cannot emit verification statements in Verilog" +
+      "(2001). Use the SystemVerilog emitter instead.")
+  }
   
   /** 
     * Store Emission option per Target
@@ -594,6 +602,7 @@ class VerilogEmitter extends SeqTransform with Emitter {
     // memories need to be initialized even when randomization is disabled
     val memoryInitials = ArrayBuffer[Seq[Any]]()
     val simulates = ArrayBuffer[Seq[Any]]()
+    val formals = mutable.LinkedHashMap[Expression, ArrayBuffer[Seq[Any]]]()
 
     def bigIntToVLit(bi: BigInt): String =
       if (bi.isValidInt) bi.toString else s"${bi.bitLength}'d$bi"
@@ -818,6 +827,14 @@ class VerilogEmitter extends SeqTransform with Emitter {
       lines += Seq("`endif // SYNTHESIS")
     }
 
+    def addFormal(clk: Expression, en: Expression, stmt: Seq[Any], info: Info) = {
+      addFormalStatement(formals, clk, en, stmt, info)
+    }
+
+    def formalStatement(op: Formal.Value, cond: Expression): Seq[Any] = {
+      Seq(op.toString, "(", cond, ");")
+    }
+
     def stop(ret: Int): Seq[Any] = Seq(if (ret == 0) "$finish;" else "$fatal;")
 
     def printf(str: StringLit, args: Seq[Expression]): Seq[Any] = {
@@ -921,6 +938,8 @@ class VerilogEmitter extends SeqTransform with Emitter {
           simulate(sx.clk, sx.en, stop(sx.ret), Some("STOP_COND"), sx.info)
         case sx: Print =>
           simulate(sx.clk, sx.en, printf(sx.string, sx.args), Some("PRINTF_COND"), sx.info)
+        case sx: Verification =>
+          addFormal(sx.clk, sx.en, formalStatement(sx.op, sx.pred), sx.info)
         // If we are emitting an Attach, it must not have been removable in VerilogPrep
         case sx: Attach =>
           // For Synthesis
@@ -1120,6 +1139,14 @@ class VerilogEmitter extends SeqTransform with Emitter {
         emit(Seq("`endif // SYNTHESIS"))
       }
 
+      if (formals.keys.nonEmpty) {
+        for ((clk, content) <- formals if content.nonEmpty) {
+          emit(Seq(tab, "always @(posedge ", clk, ") begin"))
+          for (line <- content) emit(Seq(tab, tab, line))
+          emit(Seq(tab, "end"))
+        }
+      }
+
       emit(Seq("endmodule"))
     }
 
@@ -1213,6 +1240,7 @@ class VerilogEmitter extends SeqTransform with Emitter {
 class MinimumVerilogEmitter extends VerilogEmitter with Emitter {
 
   override def prerequisites =
+    Dependency[RemoveVerificationStatements] +:
     Dependency[LegalizeAndReductionsTransform] +:
     firrtl.stage.Forms.LowFormMinimumOptimized
 
@@ -1224,8 +1252,20 @@ class MinimumVerilogEmitter extends VerilogEmitter with Emitter {
 class SystemVerilogEmitter extends VerilogEmitter {
   override val outputSuffix: String = ".sv"
 
+  override def prerequisites =
+      Dependency[LegalizeAndReductionsTransform] +:
+      firrtl.stage.Forms.LowFormOptimized
+
+  override def addFormalStatement(formals: mutable.Map[Expression, ArrayBuffer[Seq[Any]]],
+                                  clk: Expression, en: Expression,
+                                  stmt: Seq[Any], info: Info): Unit = {
+    val lines = formals.getOrElseUpdate(clk, ArrayBuffer[Seq[Any]]())
+    lines += Seq("if (", en, ") begin")
+    lines += Seq(tab, stmt, info)
+    lines += Seq("end")
+  }
+
   override def execute(state: CircuitState): CircuitState = {
-    StageUtils.dramaticWarning("SystemVerilog Emitter is the same as the Verilog Emitter!")
     super.execute(state)
   }
 }
diff --git a/src/main/scala/firrtl/LoweringCompilers.scala b/src/main/scala/firrtl/LoweringCompilers.scala
index 14d222f6..19e7d8c6 100644
--- a/src/main/scala/firrtl/LoweringCompilers.scala
+++ b/src/main/scala/firrtl/LoweringCompilers.scala
@@ -3,7 +3,6 @@
 package firrtl
 
 import firrtl.transforms.IdentityTransform
-import firrtl.options.StageUtils
 import firrtl.stage.{Forms, TransformManager}
 
 @deprecated("Use a TransformManager or some other Stage/Phase class. Will be removed in 1.4.", "FIRRTL 1.2")
@@ -174,5 +173,4 @@ class MinimumVerilogCompiler extends Compiler {
 )
 class SystemVerilogCompiler extends VerilogCompiler {
   override val emitter = new SystemVerilogEmitter
-  StageUtils.dramaticWarning("SystemVerilog Compiler behaves the same as the Verilog Compiler!")
 }
diff --git a/src/main/scala/firrtl/Visitor.scala b/src/main/scala/firrtl/Visitor.scala
index 4033c0fd..48a887de 100644
--- a/src/main/scala/firrtl/Visitor.scala
+++ b/src/main/scala/firrtl/Visitor.scala
@@ -328,6 +328,17 @@ class Visitor(infoMode: InfoMode) extends AbstractParseTreeVisitor[FirrtlNode] w
         case "attach" => Attach(info, ctx_exp map visitExp)
         case "printf(" => Print(info, visitStringLit(ctx.StringLit), ctx_exp.drop(2).map(visitExp),
           visitExp(ctx_exp(0)), visitExp(ctx_exp(1)))
+        // formal
+        case "assert" => Verification(Formal.Assert, info, visitExp(ctx_exp(0)),
+          visitExp(ctx_exp(1)), visitExp(ctx_exp(2)),
+          visitStringLit(ctx.StringLit))
+        case "assume" => Verification(Formal.Assume, info, visitExp(ctx_exp(0)),
+          visitExp(ctx_exp(1)), visitExp(ctx_exp(2)),
+          visitStringLit(ctx.StringLit))
+        case "cover" => Verification(Formal.Cover, info, visitExp(ctx_exp(0)),
+          visitExp(ctx_exp(1)), visitExp(ctx_exp(2)),
+          visitStringLit(ctx.StringLit))
+        // end formal
         case "skip" => EmptyStmt
       }
       // If we don't match on the first child, try the next one
diff --git a/src/main/scala/firrtl/ir/IR.scala b/src/main/scala/firrtl/ir/IR.scala
index a47a4cea..9914ad45 100644
--- a/src/main/scala/firrtl/ir/IR.scala
+++ b/src/main/scala/firrtl/ir/IR.scala
@@ -541,6 +541,38 @@ case class Print(
   def foreachString(f: String => Unit): Unit = Unit
   def foreachInfo(f: Info => Unit): Unit = f(info)
 }
+
+// formal
+object Formal extends Enumeration {
+  val Assert = Value("assert")
+  val Assume = Value("assume")
+  val Cover = Value("cover")
+}
+
+case class Verification(
+  op: Formal.Value,
+  info: Info,
+  clk: Expression,
+  pred: Expression,
+  en: Expression,
+  msg: StringLit
+) extends Statement with HasInfo {
+  def serialize: String = op + "(" + Seq(clk, pred, en).map(_.serialize)
+    .mkString(", ") + ", \"" + msg.serialize + "\")" + info.serialize
+  def mapStmt(f: Statement => Statement): Statement = this
+  def mapExpr(f: Expression => Expression): Statement =
+    copy(clk = f(clk), pred = f(pred), en = f(en))
+  def mapType(f: Type => Type): Statement = this
+  def mapString(f: String => String): Statement = this
+  def mapInfo(f: Info => Info): Statement = copy(info = f(info))
+  def foreachStmt(f: Statement => Unit): Unit = Unit
+  def foreachExpr(f: Expression => Unit): Unit = { f(clk); f(pred); f(en); }
+  def foreachType(f: Type => Unit): Unit = Unit
+  def foreachString(f: String => Unit): Unit = Unit
+  def foreachInfo(f: Info => Unit): Unit = f(info)
+}
+// end formal
+
 case object EmptyStmt extends Statement {
   def serialize: String = "skip"
   def mapStmt(f: Statement => Statement): Statement = this
diff --git a/src/main/scala/firrtl/passes/CheckFlows.scala b/src/main/scala/firrtl/passes/CheckFlows.scala
index b4ce4d5f..3a9cc212 100644
--- a/src/main/scala/firrtl/passes/CheckFlows.scala
+++ b/src/main/scala/firrtl/passes/CheckFlows.scala
@@ -105,6 +105,10 @@ object CheckFlows extends Pass {
         case (s: Stop) =>
           check_flow(info, mname, flows, SourceFlow)(s.en)
           check_flow(info, mname, flows, SourceFlow)(s.clk)
+        case (s: Verification) =>
+          check_flow(info, mname, flows, SourceFlow)(s.clk)
+          check_flow(info, mname, flows, SourceFlow)(s.pred)
+          check_flow(info, mname, flows, SourceFlow)(s.en)
         case _ =>
       }
       s foreach check_flows_e(info, mname, flows)
diff --git a/src/main/scala/firrtl/passes/CheckTypes.scala b/src/main/scala/firrtl/passes/CheckTypes.scala
index 5173b8c4..601ee524 100644
--- a/src/main/scala/firrtl/passes/CheckTypes.scala
+++ b/src/main/scala/firrtl/passes/CheckTypes.scala
@@ -310,6 +310,10 @@ object CheckTypes extends Pass {
             errors.append(new PrintfArgNotGround(info, mname))
           if (wt(sx.clk.tpe) != wt(ClockType)) errors.append(new ReqClk(info, mname))
           if (wt(sx.en.tpe) != wt(ut)) errors.append(new EnNotUInt(info, mname))
+        case sx: Verification =>
+          if (wt(sx.clk.tpe) != wt(ClockType)) errors.append(new ReqClk(info, mname))
+          if (wt(sx.pred.tpe) != wt(ut)) errors.append(new PredNotUInt(info, mname))
+          if (wt(sx.en.tpe) != wt(ut)) errors.append(new EnNotUInt(info, mname))
         case sx: DefMemory => sx.dataType match {
           case AnalogType(w) => errors.append(new IllegalAnalogDeclaration(info, mname, sx.name))
           case t =>
diff --git a/src/main/scala/firrtl/passes/ExpandWhens.scala b/src/main/scala/firrtl/passes/ExpandWhens.scala
index 32fec4ed..75aad29a 100644
--- a/src/main/scala/firrtl/passes/ExpandWhens.scala
+++ b/src/main/scala/firrtl/passes/ExpandWhens.scala
@@ -156,6 +156,7 @@ object ExpandWhens extends Pass {
       case sx: Stop =>
         simlist += (if (weq(p, one)) sx else Stop(sx.info, sx.ret, sx.clk, AND(p, sx.en)))
         EmptyStmt
+      case sx: Verification => if (weq(p, one)) sx else sx.copy(en = AND(p, sx.en))
       // Expand conditionally, see comments below
       case sx: Conditionally =>
         /* 1) Recurse into conseq and alt with empty netlist, updated defaults, updated predicate
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))
diff --git a/src/main/scala/firrtl/stage/Forms.scala b/src/main/scala/firrtl/stage/Forms.scala
index 9cf711d8..e6ed9603 100644
--- a/src/main/scala/firrtl/stage/Forms.scala
+++ b/src/main/scala/firrtl/stage/Forms.scala
@@ -57,7 +57,8 @@ object Forms {
          Dependency[passes.ExpandWhensAndCheck],
          Dependency[passes.RemoveIntervals],
          Dependency(passes.ConvertFixedToSInt),
-         Dependency(passes.ZeroWidth) )
+         Dependency(passes.ZeroWidth),
+         Dependency[firrtl.transforms.formal.AssertSubmoduleAssumptions] )
 
   val LowForm: Seq[TransformDependency] = MidForm ++
     Seq( Dependency(passes.LowerTypes),
diff --git a/src/main/scala/firrtl/transforms/DeadCodeElimination.scala b/src/main/scala/firrtl/transforms/DeadCodeElimination.scala
index b8cfa54e..4182e496 100644
--- a/src/main/scala/firrtl/transforms/DeadCodeElimination.scala
+++ b/src/main/scala/firrtl/transforms/DeadCodeElimination.scala
@@ -154,6 +154,10 @@ class DeadCodeElimination extends Transform
         Seq(clk, en).flatMap(getDeps(_)).foreach(ref => depGraph.addPairWithEdge(circuitSink, ref))
       case Print(_, _, args, clk, en) =>
         (args :+ clk :+ en).flatMap(getDeps(_)).foreach(ref => depGraph.addPairWithEdge(circuitSink, ref))
+      case s: Verification =>
+        for (expr <- Seq(s.clk, s.pred, s.en)) {
+          getDeps(expr).foreach(ref => depGraph.addPairWithEdge(circuitSink, ref))
+        }
       case Block(stmts) => stmts.foreach(onStmt(_))
       case ignore @ (_: IsInvalid | _: WDefInstance | EmptyStmt) => // do nothing
       case other => throw new Exception(s"Unexpected Statement $other")
@@ -256,6 +260,7 @@ class DeadCodeElimination extends Transform
           else decl
         case print: Print => deleteIfNotEnabled(print, print.en)
         case stop: Stop => deleteIfNotEnabled(stop, stop.en)
+        case formal: Verification => deleteIfNotEnabled(formal, formal.en)
         case con: Connect =>
           val node = getDeps(con.loc) match { case Seq(elt) => elt }
           if (deadNodes.contains(node)) EmptyStmt else con
diff --git a/src/main/scala/firrtl/transforms/LegalizeClocks.scala b/src/main/scala/firrtl/transforms/LegalizeClocks.scala
index 333eb096..f439fdc9 100644
--- a/src/main/scala/firrtl/transforms/LegalizeClocks.scala
+++ b/src/main/scala/firrtl/transforms/LegalizeClocks.scala
@@ -45,6 +45,10 @@ object LegalizeClocksTransform {
         val node = DefNode(s.info, namespace.newTemp, s.clk)
         val sx = s.copy(clk = WRef(node))
         Block(Seq(node, sx))
+      case s: Verification if illegalClockExpr(s.clk) =>
+        val node = DefNode(s.info, namespace.newTemp, s.clk)
+        val sx = s.copy(clk = WRef(node))
+        Block(Seq(node, sx))
       case other => other
     }
 
diff --git a/src/main/scala/firrtl/transforms/RemoveWires.scala b/src/main/scala/firrtl/transforms/RemoveWires.scala
index 0504c19d..33daa8ce 100644
--- a/src/main/scala/firrtl/transforms/RemoveWires.scala
+++ b/src/main/scala/firrtl/transforms/RemoveWires.scala
@@ -124,7 +124,7 @@ class RemoveWires extends Transform with DependencyAPIMigration {
               netlist(we(expr)) = (Seq(ValidIf(Utils.zero, UIntLiteral(BigInt(0), width), expr.tpe)), info)
             case _ => otherStmts += invalid
           }
-        case other @ (_: Print | _: Stop | _: Attach) =>
+        case other @ (_: Print | _: Stop | _: Attach | _: Verification) =>
           otherStmts += other
         case EmptyStmt => // Dont bother keeping EmptyStmts around
         case block: Block => block.foreach(onStmt)
diff --git a/src/main/scala/firrtl/transforms/formal/AssertSubmoduleAssumptions.scala b/src/main/scala/firrtl/transforms/formal/AssertSubmoduleAssumptions.scala
new file mode 100644
index 00000000..7370fcfb
--- /dev/null
+++ b/src/main/scala/firrtl/transforms/formal/AssertSubmoduleAssumptions.scala
@@ -0,0 +1,68 @@
+
+package firrtl.transforms.formal
+
+import firrtl.ir.{Circuit, Formal, Statement, Verification}
+import firrtl.stage.TransformManager.TransformDependency
+import firrtl.{CircuitState, DependencyAPIMigration, Transform}
+import firrtl.annotations.NoTargetAnnotation
+import firrtl.options.{PreservesAll, RegisteredTransform, ShellOption}
+
+
+/**
+  * Assert Submodule Assumptions
+  *
+  * Converts `assume` statements to `assert` statements in all modules except
+  * the top module being compiled. This avoids a class of bugs in which an
+  * overly restrictive assume in a child module can prevent the model checker
+  * from searching valid inputs and states in the parent module.
+  */
+class AssertSubmoduleAssumptions extends Transform
+  with RegisteredTransform
+  with DependencyAPIMigration
+  with PreservesAll[Transform] {
+
+  override def prerequisites: Seq[TransformDependency] = Seq.empty
+  override def optionalPrerequisites: Seq[TransformDependency] = Seq.empty
+  override def optionalPrerequisiteOf: Seq[TransformDependency] =
+    firrtl.stage.Forms.MidEmitters
+
+  val options = Seq(
+    new ShellOption[Unit](
+      longOption = "no-asa",
+      toAnnotationSeq = (_: Unit) => Seq(
+        DontAssertSubmoduleAssumptionsAnnotation),
+      helpText = "Disable assert submodule assumptions" ) )
+
+  def assertAssumption(s: Statement): Statement = s match {
+    case Verification(Formal.Assume, info, clk, cond, en, msg) =>
+      Verification(Formal.Assert, info, clk, cond, en, msg)
+    case t => t.mapStmt(assertAssumption)
+  }
+
+  def run(c: Circuit): Circuit = {
+    c.mapModule(mod => {
+      if (mod.name != c.main) {
+        mod.mapStmt(assertAssumption)
+      } else {
+        mod
+      }
+    })
+  }
+
+  def execute(state: CircuitState): CircuitState = {
+    val noASA = state.annotations.contains(
+      DontAssertSubmoduleAssumptionsAnnotation)
+    if (noASA) {
+      logger.info("Skipping assert submodule assumptions")
+      state
+    } else {
+      state.copy(circuit = run(state.circuit))
+    }
+  }
+}
+
+case object AssertSubmoduleAssumptionsAnnotation extends NoTargetAnnotation {
+  val transform = new AssertSubmoduleAssumptions
+}
+
+case object DontAssertSubmoduleAssumptionsAnnotation extends NoTargetAnnotation
diff --git a/src/main/scala/firrtl/transforms/formal/RemoveVerificationStatements.scala b/src/main/scala/firrtl/transforms/formal/RemoveVerificationStatements.scala
new file mode 100644
index 00000000..9bf4f779
--- /dev/null
+++ b/src/main/scala/firrtl/transforms/formal/RemoveVerificationStatements.scala
@@ -0,0 +1,53 @@
+
+package firrtl.transforms.formal
+
+import firrtl.ir.{Circuit, EmptyStmt, Statement, Verification}
+import firrtl.{CircuitState, DependencyAPIMigration, MinimumVerilogEmitter, Transform, VerilogEmitter}
+import firrtl.options.{Dependency, PreservesAll, StageUtils}
+import firrtl.stage.TransformManager.TransformDependency
+
+
+/**
+  * Remove Verification Statements
+  *
+  * Replaces all verification statements in all modules with the empty statement.
+  * This is intended to be required by the Verilog emitter to ensure compatibility
+  * with the Verilog 2001 standard.
+  */
+class RemoveVerificationStatements extends Transform
+  with DependencyAPIMigration
+  with PreservesAll[Transform] {
+
+  override def prerequisites: Seq[TransformDependency] = Seq.empty
+  override def optionalPrerequisites: Seq[TransformDependency] = Seq.empty
+  override def optionalPrerequisiteOf: Seq[TransformDependency] =
+    Seq( Dependency[VerilogEmitter],
+      Dependency[MinimumVerilogEmitter])
+
+  private var removedCounter = 0
+
+  def removeVerification(s: Statement): Statement = s match {
+    case _: Verification => {
+      removedCounter += 1
+      EmptyStmt
+    }
+    case t => t.mapStmt(removeVerification)
+  }
+
+  def run(c: Circuit): Circuit = {
+    c.mapModule(mod => {
+      mod.mapStmt(removeVerification)
+    })
+  }
+
+  def execute(state: CircuitState): CircuitState = {
+    val newState = state.copy(circuit = run(state.circuit))
+    if (removedCounter > 0) {
+      StageUtils.dramaticWarning(s"$removedCounter verification statements " +
+        "were removed when compiling to Verilog because the basic Verilog " +
+        "standard does not support them. If this was not intended, compile " +
+        "to System Verilog instead using the `-X sverilog` compiler flag.")
+    }
+    newState
+  }
+}
diff --git a/src/test/scala/firrtlTests/CustomTransformSpec.scala b/src/test/scala/firrtlTests/CustomTransformSpec.scala
index d736ec3c..677aa6ff 100644
--- a/src/test/scala/firrtlTests/CustomTransformSpec.scala
+++ b/src/test/scala/firrtlTests/CustomTransformSpec.scala
@@ -6,12 +6,11 @@ import firrtl.ir.Circuit
 import firrtl._
 import firrtl.passes.Pass
 import firrtl.ir._
-
 import firrtl.stage.{FirrtlSourceAnnotation, FirrtlStage, Forms, RunFirrtlTransformAnnotation}
 import firrtl.options.Dependency
 import firrtl.transforms.{IdentityTransform, LegalizeAndReductionsTransform}
-
 import firrtl.testutils._
+import firrtl.transforms.formal.RemoveVerificationStatements
 
 import scala.reflect.runtime
 
@@ -173,10 +172,15 @@ class CustomTransformSpec extends FirrtlFlatSpec {
         .map(target => new firrtl.stage.transforms.Compiler(target))
         .map(_.flattenedTransformOrder.map(Dependency.fromTransform(_)))
 
-    Seq( (Seq(Dependency[LowFirrtlEmitter]),                                                  Seq(low.last)      ),
-         (Seq(Dependency[LegalizeAndReductionsTransform], Dependency[MinimumVerilogEmitter]), Seq(lowMinOpt.last)),
-         (Seq(Dependency[LegalizeAndReductionsTransform], Dependency[VerilogEmitter]),        Seq(lowOpt.last)    ),
-         (Seq(Dependency[LegalizeAndReductionsTransform], Dependency[SystemVerilogEmitter]),  Seq(lowOpt.last)   )
+    Seq( (Seq(Dependency[LowFirrtlEmitter]),             Seq(low.last)      ),
+         (Seq(Dependency[LegalizeAndReductionsTransform],
+           Dependency[RemoveVerificationStatements],
+           Dependency[MinimumVerilogEmitter]),           Seq(lowMinOpt.last)),
+         (Seq(Dependency[LegalizeAndReductionsTransform],
+           Dependency[RemoveVerificationStatements],
+           Dependency[VerilogEmitter]),                  Seq(lowOpt.last)    ),
+         (Seq(Dependency[LegalizeAndReductionsTransform],
+           Dependency[SystemVerilogEmitter]),            Seq(lowOpt.last)   )
     ).foreach((testOrder _).tupled)
   }
 
diff --git a/src/test/scala/firrtlTests/ExpandWhensSpec.scala b/src/test/scala/firrtlTests/ExpandWhensSpec.scala
index d4b3d0df..250a75d7 100644
--- a/src/test/scala/firrtlTests/ExpandWhensSpec.scala
+++ b/src/test/scala/firrtlTests/ExpandWhensSpec.scala
@@ -134,6 +134,20 @@ class ExpandWhensSpec extends FirrtlFlatSpec {
     val check = "mux(p, in[0], in[1])"
     executeTest(input, check, true)
   }
+  it should "handle asserts" in {
+    val input =
+      """circuit Test :
+        |  module Test :
+        |    input clock : Clock
+        |    input in : UInt<32>
+        |    input p : UInt<1>
+        |    when p :
+        |      assert(clock, eq(in, UInt<1>("h1")), UInt<1>("h1"), "assert0")
+        |    else :
+        |      skip""".stripMargin
+    val check = "assert(clock, eq(in, UInt<1>(\"h1\")), and(and(UInt<1>(\"h1\"), p), UInt<1>(\"h1\")), \"assert0\")"
+    executeTest(input, check, true)
+  }
 }
 
 class ExpandWhensExecutionTest extends ExecutionTest("ExpandWhens", "/passes/ExpandWhens")
diff --git a/src/test/scala/firrtlTests/LoweringCompilersSpec.scala b/src/test/scala/firrtlTests/LoweringCompilersSpec.scala
index cc4914f2..75f2ea02 100644
--- a/src/test/scala/firrtlTests/LoweringCompilersSpec.scala
+++ b/src/test/scala/firrtlTests/LoweringCompilersSpec.scala
@@ -173,7 +173,9 @@ class LoweringCompilersSpec extends FlatSpec with Matchers {
                   Dependency[firrtl.passes.InferWidths])),
       Del(14),
       Add(15, Seq(Dependency(firrtl.passes.ResolveKinds),
-                  Dependency(firrtl.passes.InferTypes)))
+                  Dependency(firrtl.passes.InferTypes))),
+      // TODO
+      Add(17, Seq(Dependency[firrtl.transforms.formal.AssertSubmoduleAssumptions]))
     )
     compare(legacyTransforms(new HighFirrtlToMiddleFirrtl), tm, patches)
   }
@@ -351,7 +353,9 @@ class LoweringCompilersSpec extends FlatSpec with Matchers {
         Seq(new Transforms.LowToLow, new firrtl.MinimumVerilogEmitter)
     val tm = (new TransformManager(Seq(Dependency[firrtl.MinimumVerilogEmitter], Dependency[Transforms.LowToLow])))
     val patches = Seq(
-      Add(62, Seq(Dependency[firrtl.transforms.LegalizeAndReductionsTransform]))
+      Add(63, Seq(
+        Dependency[firrtl.transforms.formal.RemoveVerificationStatements],
+        Dependency[firrtl.transforms.LegalizeAndReductionsTransform]))
     )
     compare(expected, tm, patches)
   }
@@ -362,7 +366,9 @@ class LoweringCompilersSpec extends FlatSpec with Matchers {
         Seq(new Transforms.LowToLow, new firrtl.VerilogEmitter)
     val tm = (new TransformManager(Seq(Dependency[firrtl.VerilogEmitter], Dependency[Transforms.LowToLow])))
     val patches = Seq(
-      Add(69, Seq(Dependency[firrtl.transforms.LegalizeAndReductionsTransform]))
+      Add(70, Seq(
+        Dependency[firrtl.transforms.formal.RemoveVerificationStatements],
+        Dependency[firrtl.transforms.LegalizeAndReductionsTransform]))
     )
     compare(expected, tm, patches)
   }
diff --git a/src/test/scala/firrtlTests/formal/AssertSubmoduleAssumptionsSpec.scala b/src/test/scala/firrtlTests/formal/AssertSubmoduleAssumptionsSpec.scala
new file mode 100644
index 00000000..edfd31d3
--- /dev/null
+++ b/src/test/scala/firrtlTests/formal/AssertSubmoduleAssumptionsSpec.scala
@@ -0,0 +1,108 @@
+
+package firrtlTests.formal
+
+import firrtl.{CircuitState, Parser, Transform, UnknownForm}
+import firrtl.testutils.FirrtlFlatSpec
+import firrtl.transforms.formal.AssertSubmoduleAssumptions
+import firrtl.stage.{Forms, TransformManager}
+
+class AssertSubmoduleAssumptionsSpec extends FirrtlFlatSpec {
+  behavior of "AssertSubmoduleAssumptions"
+
+  val transforms = new TransformManager(Forms.HighForm, Forms.MinimalHighForm)
+    .flattenedTransformOrder ++ Seq(new AssertSubmoduleAssumptions)
+
+  def run(input: String, check: Seq[String], debug: Boolean = false): Unit = {
+    val circuit = Parser.parse(input.split("\n").toIterator)
+    val result = transforms.foldLeft(CircuitState(circuit, UnknownForm)) {
+      (c: CircuitState, p: Transform) => p.runTransform(c)
+    }
+    val lines = result.circuit.serialize.split("\n") map normalized
+
+    if (debug) {
+      println(lines.mkString("\n"))
+    }
+
+    for (ch <- check) {
+      lines should contain (ch)
+    }
+  }
+
+  it should "convert `assume` to `assert` in a submodule" in {
+    val input =
+      """circuit Test :
+        |  module Test :
+        |    input clock : Clock
+        |    input reset : UInt<1>
+        |    input in : UInt<8>
+        |    output out : UInt<8>
+        |    inst sub of Sub
+        |    sub.clock <= clock
+        |    sub.reset <= reset
+        |    sub.in <= in
+        |    out <= sub.out
+        |    assume(clock, eq(in, UInt(0)), UInt(1), "assume0")
+        |    assert(clock, eq(out, UInt(0)), UInt(1), "assert0")
+        |
+        |  module Sub :
+        |    input clock : Clock
+        |    input reset : UInt<1>
+        |    input in : UInt<8>
+        |    output out : UInt<8>
+        |    out <= in
+        |    assume(clock, eq(in, UInt(1)), UInt(1), "assume1")
+        |    assert(clock, eq(out, UInt(1)), UInt(1), "assert1")
+        |""".stripMargin
+
+    val check = Seq(
+      "assert(clock, eq(in, UInt<1>(\"h1\")), UInt<1>(\"h1\"), \"assume1\")"
+    )
+    run(input, check)
+  }
+
+  it should "convert `assume` to `assert` in a nested submodule" in {
+    val input =
+      """circuit Test :
+        |  module Test :
+        |    input clock : Clock
+        |    input reset : UInt<1>
+        |    input in : UInt<8>
+        |    output out : UInt<8>
+        |    inst sub of Sub
+        |    sub.clock <= clock
+        |    sub.reset <= reset
+        |    sub.in <= in
+        |    out <= sub.out
+        |    assume(clock, eq(in, UInt(0)), UInt(1), "assume0")
+        |    assert(clock, eq(out, UInt(0)), UInt(1), "assert0")
+        |
+        |  module Sub :
+        |    input clock : Clock
+        |    input reset : UInt<1>
+        |    input in : UInt<8>
+        |    output out : UInt<8>
+        |    inst nestedSub of NestedSub
+        |    nestedSub.clock <= clock
+        |    nestedSub.reset <= reset
+        |    nestedSub.in <= in
+        |    out <= nestedSub.out
+        |    assume(clock, eq(in, UInt(1)), UInt(1), "assume1")
+        |    assert(clock, eq(out, UInt(1)), UInt(1), "assert1")
+        |
+        |  module NestedSub :
+        |    input clock : Clock
+        |    input reset : UInt<1>
+        |    input in : UInt<8>
+        |    output out : UInt<8>
+        |    out <= in
+        |    assume(clock, eq(in, UInt(2)), UInt(1), "assume2")
+        |    assert(clock, eq(out, UInt(2)), UInt(1), "assert2")
+        |""".stripMargin
+
+    val check = Seq(
+      "assert(clock, eq(in, UInt<1>(\"h1\")), UInt<1>(\"h1\"), \"assume1\")",
+      "assert(clock, eq(in, UInt<2>(\"h2\")), UInt<1>(\"h1\"), \"assume2\")"
+    )
+    run(input, check)
+  }
+}
diff --git a/src/test/scala/firrtlTests/formal/RemoveVerificationStatementsSpec.scala b/src/test/scala/firrtlTests/formal/RemoveVerificationStatementsSpec.scala
new file mode 100644
index 00000000..10e63ae4
--- /dev/null
+++ b/src/test/scala/firrtlTests/formal/RemoveVerificationStatementsSpec.scala
@@ -0,0 +1,70 @@
+
+package firrtlTests.formal
+
+import firrtl.{CircuitState, Parser, Transform, UnknownForm}
+import firrtl.stage.{Forms, TransformManager}
+import firrtl.testutils.FirrtlFlatSpec
+import firrtl.transforms.formal.RemoveVerificationStatements
+
+class RemoveVerificationStatementsSpec extends FirrtlFlatSpec {
+  behavior of "RemoveVerificationStatements"
+
+  val transforms = new TransformManager(Forms.HighForm, Forms.MinimalHighForm)
+    .flattenedTransformOrder ++ Seq(new RemoveVerificationStatements)
+
+  def run(input: String, antiCheck: Seq[String], debug: Boolean = false): Unit = {
+    val circuit = Parser.parse(input.split("\n").toIterator)
+    val result = transforms.foldLeft(CircuitState(circuit, UnknownForm)) {
+      (c: CircuitState, p: Transform) => p.runTransform(c)
+    }
+    val lines = result.circuit.serialize.split("\n") map normalized
+
+    if (debug) {
+      println(lines.mkString("\n"))
+    }
+
+    for (ch <- antiCheck) {
+      lines should not contain (ch)
+    }
+  }
+
+  it should "remove all verification statements" in {
+    val input =
+      """circuit Test :
+        |  module Test :
+        |    input clock : Clock
+        |    input reset : UInt<1>
+        |    input in : UInt<8>
+        |    output out : UInt<8>
+        |    inst sub of Sub
+        |    sub.clock <= clock
+        |    sub.reset <= reset
+        |    sub.in <= in
+        |    out <= sub.out
+        |    assume(clock, eq(in, UInt(0)), UInt(1), "assume0")
+        |    assert(clock, eq(out, UInt(0)), UInt(1), "assert0")
+        |    cover(clock, eq(out, UInt(0)), UInt(1), "cover0")
+        |
+        |  module Sub :
+        |    input clock : Clock
+        |    input reset : UInt<1>
+        |    input in : UInt<8>
+        |    output out : UInt<8>
+        |    out <= in
+        |    assume(clock, eq(in, UInt(1)), UInt(1), "assume1")
+        |    assert(clock, eq(out, UInt(1)), UInt(1), "assert1")
+        |    cover(clock, eq(out, UInt(1)), UInt(1), "cover1")
+        |""".stripMargin
+
+    val antiCheck = Seq(
+      "assume(clock, eq(in, UInt<1>(\"h0\")), UInt<1>(\"h1\"), \"assume0\")",
+      "assert(clock, eq(out, UInt<1>(\"h0\")), UInt<1>(\"h1\"), \"assert0\")",
+      "cover(clock, eq(out, UInt<1>(\"h0\")), UInt<1>(\"h1\"), \"cover0\")",
+      "assume(clock, eq(in, UInt<1>(\"h1\")), UInt<1>(\"h1\"), \"assume1\")",
+      "assert(clock, eq(out, UInt<1>(\"h1\")), UInt<1>(\"h1\"), \"assert1\")",
+      "cover(clock, eq(out, UInt<1>(\"h1\")), UInt<1>(\"h1\"), \"cover1\")"
+    )
+    run(input, antiCheck)
+  }
+
+}
diff --git a/src/test/scala/firrtlTests/formal/VerificationSpec.scala b/src/test/scala/firrtlTests/formal/VerificationSpec.scala
new file mode 100644
index 00000000..0b160082
--- /dev/null
+++ b/src/test/scala/firrtlTests/formal/VerificationSpec.scala
@@ -0,0 +1,55 @@
+package firrtlTests.formal
+
+import firrtl.{SystemVerilogCompiler}
+import firrtl.testutils.FirrtlFlatSpec
+import logger.{LogLevel, Logger}
+
+class VerificationSpec extends FirrtlFlatSpec {
+  behavior of "Formal"
+
+  it should "generate SystemVerilog verification statements" in {
+    val compiler = new SystemVerilogCompiler
+    val input =
+      """circuit Asserting :
+        |  module Asserting :
+        |    input clock: Clock
+        |    input reset: UInt<1>
+        |    input in: UInt<8>
+        |    output out: UInt<8>
+        |    wire areEqual: UInt<1>
+        |    wire inputEquals0xAA: UInt<1>
+        |    wire outputEquals0xAA: UInt<1>
+        |    out <= in
+        |    areEqual <= eq(out, in)
+        |    inputEquals0xAA <= eq(in, UInt<8>("hAA"))
+        |    outputEquals0xAA <= eq(out, UInt<8>("hAA"))
+        |    node true = UInt("b1")
+        |    assume(clock, inputEquals0xAA, true, "assume input is 0xAA")
+        |    assert(clock, areEqual, true, "assert that output equals input")
+        |    cover(clock, outputEquals0xAA, true, "cover output is 0xAA")
+        |""".stripMargin
+    val expected =
+      """module Asserting(
+        |  input [7:0] in,
+        |  output [7:0] out
+        |);
+        |  wire areEqual = out == in;
+        |  wire inputEquals0xAA = in == 8'haa;
+        |  wire outputEquals0xAA = out == 8'haa;
+        |  assign out = in;
+        |  always @(posedge clock) begin
+        |    if (1'h1) begin
+        |      assume(inputEquals0xAA);
+        |    end
+        |    if (1'h1) begin
+        |      assert(areEqual);
+        |    end
+        |    if (1'h1) begin
+        |      cover(outputEquals0xAA);
+        |    end
+        |  end
+        |endmodule
+        |""".stripMargin.split("\n") map normalized
+    executeTest(input, expected, compiler)
+  }
+}
diff --git a/src/test/scala/firrtlTests/stage/FirrtlMainSpec.scala b/src/test/scala/firrtlTests/stage/FirrtlMainSpec.scala
index bd6d3ac7..5c8f1129 100644
--- a/src/test/scala/firrtlTests/stage/FirrtlMainSpec.scala
+++ b/src/test/scala/firrtlTests/stage/FirrtlMainSpec.scala
@@ -200,8 +200,7 @@ class FirrtlMainSpec extends AnyFeatureSpec with GivenWhenThen with Matchers wit
       FirrtlMainTest(args   = Array("-X", "verilog", "-E", "verilog", "-foaf", "foo.anno"),
                       files  = Seq("Top.v", "foo.anno.anno.json")),
       FirrtlMainTest(args   = Array("-X", "sverilog", "-E", "sverilog", "-foaf", "foo.json"),
-                      files  = Seq("Top.sv", "foo.json.anno.json"),
-                      stdout = Some("SystemVerilog Compiler behaves the same as the Verilog Compiler!")),
+                      files  = Seq("Top.sv", "foo.json.anno.json")),
 
       /* Test all one file per module emitters */
       FirrtlMainTest(args   = Array("-X", "none", "-e", "chirrtl"),
@@ -215,8 +214,7 @@ class FirrtlMainSpec extends AnyFeatureSpec with GivenWhenThen with Matchers wit
       FirrtlMainTest(args   = Array("-X", "verilog", "-e", "verilog"),
                       files  = Seq("Top.v", "Child.v")),
       FirrtlMainTest(args   = Array("-X", "sverilog", "-e", "sverilog"),
-                      files  = Seq("Top.sv", "Child.sv"),
-                      stdout = Some("SystemVerilog Compiler behaves the same as the Verilog Compiler!")),
+                      files  = Seq("Top.sv", "Child.sv")),
 
       /* Test mixing of -E with -e */
       FirrtlMainTest(args     = Array("-X", "middle", "-E", "high", "-e", "middle"),
@@ -235,8 +233,7 @@ class FirrtlMainSpec extends AnyFeatureSpec with GivenWhenThen with Matchers wit
       FirrtlMainTest(args   = Array("-X", "verilog", "-E", "verilog", "-o", "foo.sv"),
                       files  = Seq("foo.sv.v")),
       FirrtlMainTest(args   = Array("-X", "sverilog", "-E", "sverilog", "-o", "Foo"),
-                      files  = Seq("Foo.sv"),
-                      stdout = Some("SystemVerilog Compiler behaves the same as the Verilog Compiler!"))
+                      files  = Seq("Foo.sv"))
     )
       .foreach(runStageExpectFiles)