From de56a19b0a240e39366dc2d979ec05c65e0ada63 Mon Sep 17 00:00:00 2001
From: Kevin Laeufer <laeufer@cs.berkeley.edu>
Date: Mon, 30 Aug 2021 13:41:24 -0700
Subject: [PATCH] [smt] treat stop with non-zero ret like an assertion (#2338)

We treat it as an assertion that the stop will
never be enabled. stop(0) will still be ignored
(but now demoted to a info from a warning).
---
 .../smt/FirrtlToTransitionSystem.scala        | 19 ++++--
 .../smt/end2end/AssertAssumeStopSpec.scala    | 63 +++++++++++++++++++
 2 files changed, 78 insertions(+), 4 deletions(-)
 create mode 100644 src/test/scala/firrtl/backends/experimental/smt/end2end/AssertAssumeStopSpec.scala

diff --git a/src/main/scala/firrtl/backends/experimental/smt/FirrtlToTransitionSystem.scala b/src/main/scala/firrtl/backends/experimental/smt/FirrtlToTransitionSystem.scala
index 246f0172b95..726a88542e1 100644
--- a/src/main/scala/firrtl/backends/experimental/smt/FirrtlToTransitionSystem.scala
+++ b/src/main/scala/firrtl/backends/experimental/smt/FirrtlToTransitionSystem.scala
@@ -446,7 +446,7 @@ private class ModuleScanner(
     case ir.DefInstance(info, name, module, tpe) => onInstance(info, name, module, tpe)
     case s @ ir.Verification(op, info, _, pred, en, msg) =>
       if (op == ir.Formal.Cover) {
-        logger.warn(s"WARN: Cover statement was ignored: ${s.serialize}")
+        logger.info(s"[info] Cover statement was ignored: ${s.serialize}")
       } else {
         insertDummyAssignsForUnusedOutputs(pred)
         insertDummyAssignsForUnusedOutputs(en)
@@ -469,10 +469,21 @@ private class ModuleScanner(
     case s: ir.Attach =>
       error(s"Analog wires are not supported in the SMT backend: ${s.serialize}")
     case s: ir.Stop =>
-      // we could wire up the stop condition as output for debug reasons
-      logger.warn(s"WARN: Stop statements are currently not supported. Ignoring: ${s.serialize}")
+      if (s.ret == 0) {
+        logger.info(
+          s"[info] Stop statements with a return code of 0 are currently not supported. Ignoring: ${s.serialize}"
+        )
+      } else {
+        // we treat Stop statements with a non-zero exit value as assertions that en will always be false!
+        insertDummyAssignsForUnusedOutputs(s.en)
+        val name = s.name
+        infos.append(name -> s.info)
+        val enabled = onExpression(s.en)
+        connects.append(name -> BVNot(enabled))
+        asserts.append(name)
+      }
     case s: ir.Print =>
-      logger.warn(s"WARN: Print statements are not supported. Ignoring: ${s.serialize}")
+      logger.info(s"Info: ignoring: ${s.serialize}")
     case other => other.foreachStmt(onStatement)
   }
 
diff --git a/src/test/scala/firrtl/backends/experimental/smt/end2end/AssertAssumeStopSpec.scala b/src/test/scala/firrtl/backends/experimental/smt/end2end/AssertAssumeStopSpec.scala
new file mode 100644
index 00000000000..83432a00705
--- /dev/null
+++ b/src/test/scala/firrtl/backends/experimental/smt/end2end/AssertAssumeStopSpec.scala
@@ -0,0 +1,63 @@
+// SPDX-License-Identifier: Apache-2.0
+
+package firrtl.backends.experimental.smt.end2end
+
+class AssertAssumeStopSpec extends EndToEndSMTBaseSpec {
+  behavior.of("the SMT backend")
+
+  private def prefix(ii: Int): String =
+    s"""circuit AssertAssumStop$ii:
+       |  module AssertAssumStop$ii:
+       |    input clock: Clock
+       |    input a: UInt<8>
+       |    output b: UInt<8>
+       |
+       |    b <= add(a, UInt(16))
+       |
+       |""".stripMargin
+
+  it should "support assertions" in {
+    val src = prefix(0) +
+      """    assert(clock, gt(b, a), lt(a, UInt(240)), "") : b_gt_a
+        |""".stripMargin
+    test(src, MCSuccess, kmax = 2)
+  }
+
+  it should "support assumptions" in {
+    val src = prefix(1) +
+      """    assert(clock, gt(b, a), UInt(1), "") : b_gt_a
+        |""".stripMargin
+    val srcWithAssume = prefix(2) +
+      """    assert(clock, gt(b, a), UInt(1), "") : b_gt_a
+        |    assume(clock, lt(a, UInt(240)), UInt(1), "") : a_lt_240
+        |""".stripMargin
+    // the assertion alone fails because of potential overflow
+    test(src, MCFail(0), kmax = 2)
+    // with the assumption that a is not too big, it works!
+    test(srcWithAssume, MCSuccess, kmax = 2)
+  }
+
+  it should "treat stop with ret =/= 0 as assertion" in {
+    val src = prefix(3) +
+      """    stop(clock, not(gt(b, a)), 1) : b_gt_a
+        |""".stripMargin
+    val srcWithAssume = prefix(4) +
+      """    stop(clock, not(gt(b, a)), 1) : b_gt_a
+        |    assume(clock, lt(a, UInt(240)), UInt(1), "") : a_lt_240
+        |""".stripMargin
+    // the assertion alone fails because of potential overflow
+    test(src, MCFail(0), kmax = 2)
+    // with the assumption that a is not too big, it works!
+    test(srcWithAssume, MCSuccess, kmax = 2)
+  }
+
+  it should "ignore stop with ret === 0" in {
+    val src = prefix(5) +
+      """    stop(clock, not(gt(b, a)), 1) : b_gt_a
+        |    assume(clock, lt(a, UInt(240)), UInt(1), "") : a_lt_240
+        |    stop(clock, UInt(1), 0) : always_stop
+        |""".stripMargin
+    test(src, MCSuccess, kmax = 2)
+  }
+
+}