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>

26 files changed, 591 insertions, 24 deletions

diff --git a/spec/spec.tex b/spec/spec.tex
index 6b410ab1..c65deca1 100644
--- a/spec/spec.tex
+++ b/spec/spec.tex
@@ -1024,6 +1024,52 @@ Format strings support the following escape characters:
 \item \verb|\'| : Single quote
 \end{itemize}
 
+\subsection{Verification}
+
+To facilitate simulation, model checking and formal methods, there are three non-synthesizable verification statements available: assert, assume and cover. Each type of verification statement requires a clock signal, a predicate signal, an enable signal and an explanatory message string literal. The predicate and enable signals must have single bit unsigned integer type. When an assert is violated the explanatory message may be issued as guidance. The explanatory message may be phrased as if prefixed by the words ``Verifies that...''.
+
+Backends are free to generate the corresponding model checking constructs in the target language, but this is not required by the FIRRTL specification. Backends that do not generate such constructs should issue a warning. For example, the SystemVerilog emitter produces SystemVerilog assert, assume and cover statements, but the Verilog emitter does not and instead warns the user if any verification statements are encountered.
+
+
+\subsubsection{Assert}
+
+The assert statement verifies that the predicate is true on the rising edge of any clock cycle when the enable is true. In other words, it verifies that enable implies predicate.
+
+\begin{lstlisting}
+wire clk:Clock
+wire pred:UInt<1>
+wire en:UInt<1>
+pred <= eq(X, Y)
+en <= Z_valid
+assert(clk, pred, en, "X equals Y when Z is valid")
+\end{lstlisting}
+
+\subsubsection{Assume}
+
+The assume statement directs the model checker to disregard any states where the enable is true and the predicate is not true at the rising edge of the clock cycle. In other words, it reduces the states to be checked to only those where enable implies predicate is true by definition. In simulation, assume is treated as an assert.
+
+\begin{lstlisting}
+wire clk:Clock
+wire pred:UInt<1>
+wire en:UInt<1>
+pred <= eq(X, Y)
+en <= Z_valid
+assume(clk, pred, en, "X equals Y when Z is valid")
+\end{lstlisting}
+
+\subsubsection{Cover}
+
+The cover statement verifies that the predicate is true on the rising edge of some clock cycle when the enable is true. In other words, it directs the model checker to find some way to make enable implies predicate true at some time step.
+
+\begin{lstlisting}
+wire clk:Clock
+wire pred:UInt<1>
+wire en:UInt<1>
+pred <= eq(X, Y)
+en <= Z_valid
+cover(clk, pred, en, "X equals Y when Z is valid")
+\end{lstlisting}
+
 \section{Expressions}
 
 FIRRTL expressions are used for creating literal unsigned and signed integers, for referring to a declared circuit component, for statically and dynamically accessing a nested element within a component, for creating multiplexers and conditionally valid signals, and for performing primitive operations.
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)