diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/main/scala/firrtl/backends/experimental/smt/FirrtlToTransitionSystem.scala | 19 | ||||
| -rw-r--r-- | src/test/scala/firrtl/backends/experimental/smt/end2end/AssertAssumeStopSpec.scala | 63 |
2 files changed, 78 insertions, 4 deletions
diff --git a/src/main/scala/firrtl/backends/experimental/smt/FirrtlToTransitionSystem.scala b/src/main/scala/firrtl/backends/experimental/smt/FirrtlToTransitionSystem.scala index 246f0172..726a8854 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 00000000..83432a00 --- /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) + } + +} |