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>

7 files changed, 269 insertions, 15 deletions

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)