verification: emit mesage as Verilog comment (#1712)

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

2 files changed, 11 insertions, 5 deletions

diff --git a/src/main/scala/firrtl/Emitter.scala b/src/main/scala/firrtl/Emitter.scala
index 47d8c7d1..1044f047 100644
--- a/src/main/scala/firrtl/Emitter.scala
+++ b/src/main/scala/firrtl/Emitter.scala
@@ -459,7 +459,7 @@ class VerilogEmitter extends SeqTransform with Emitter {
 
   def addFormalStatement(formals: mutable.Map[Expression, ArrayBuffer[Seq[Any]]],
                                  clk: Expression, en: Expression,
-                                 stmt: Seq[Any], info: Info): Unit = {
+                                 stmt: Seq[Any], info: Info, msg: StringLit): Unit = {
     throw EmitterException("Cannot emit verification statements in Verilog" +
       "(2001). Use the SystemVerilog emitter instead.")
   }
@@ -828,8 +828,8 @@ 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 addFormal(clk: Expression, en: Expression, stmt: Seq[Any], info: Info, msg: StringLit): Unit = {
+      addFormalStatement(formals, clk, en, stmt, info, msg)
     }
 
     def formalStatement(op: Formal.Value, cond: Expression): Seq[Any] = {
@@ -940,7 +940,7 @@ class VerilogEmitter extends SeqTransform with Emitter {
         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)
+          addFormal(sx.clk, sx.en, formalStatement(sx.op, sx.pred), sx.info, sx.msg)
         // If we are emitting an Attach, it must not have been removable in VerilogPrep
         case sx: Attach =>
           // For Synthesis
@@ -1260,8 +1260,9 @@ class SystemVerilogEmitter extends VerilogEmitter {
 
   override def addFormalStatement(formals: mutable.Map[Expression, ArrayBuffer[Seq[Any]]],
                                   clk: Expression, en: Expression,
-                                  stmt: Seq[Any], info: Info): Unit = {
+                                  stmt: Seq[Any], info: Info, msg: StringLit): Unit = {
     val lines = formals.getOrElseUpdate(clk, ArrayBuffer[Seq[Any]]())
+    lines += Seq("// ", msg.serialize)
     lines += Seq("if (", en, ") begin")
     lines += Seq(tab, stmt, info)
     lines += Seq("end")
diff --git a/src/test/scala/firrtlTests/formal/VerificationSpec.scala b/src/test/scala/firrtlTests/formal/VerificationSpec.scala
index 0b160082..22dbc1f1 100644
--- a/src/test/scala/firrtlTests/formal/VerificationSpec.scala
+++ b/src/test/scala/firrtlTests/formal/VerificationSpec.scala
@@ -1,3 +1,5 @@
+// See LICENSE for license details.
+
 package firrtlTests.formal
 
 import firrtl.{SystemVerilogCompiler}
@@ -38,12 +40,15 @@ class VerificationSpec extends FirrtlFlatSpec {
         |  wire outputEquals0xAA = out == 8'haa;
         |  assign out = in;
         |  always @(posedge clock) begin
+        |    // assume input is 0xAA
         |    if (1'h1) begin
         |      assume(inputEquals0xAA);
         |    end
+        |    // assert that output equals input
         |    if (1'h1) begin
         |      assert(areEqual);
         |    end
+        |    // cover output is 0xAA
         |    if (1'h1) begin
         |      cover(outputEquals0xAA);
         |    end