When cover

fault/assert_immediate.py

@@ -1,11 +1,12 @@
 import magma as m
-from magma.when import get_curr_block as get_curr_when_block, no_when
-from fault.property import Posedge
-from fault.assert_utils import add_compile_guards
+from fault.assert_utils import add_compile_guards, get_when_cond
 
 
 def _make_assert(type_, cond, success_msg=None, failure_msg=None,
                  severity="error", name=None, compile_guard=None, delay=False):
+    if (when_cond := get_when_cond()) is not None:
+        cond = ~when_cond | cond
+
     success_msg_str = ""
     if success_msg is not None:
         success_msg_str = f" $display(\"{success_msg}\");"
@@ -62,15 +63,6 @@ def _add_docstr(fn):
 @_add_docstr
 def assert_immediate(cond, success_msg=None, failure_msg=None, severity="error",
                      name=None, compile_guard=None):
-    if get_curr_when_block():
-        # guard condition by current active when using a boolean with default 0
-        # and assigned inside when
-        with no_when():
-            when_cond = m.Bit()
-            when_cond @= 0
-        when_cond @= 1
-        cond = ~when_cond | cond
-
     _make_assert("always @(*)", cond, success_msg, failure_msg, severity, name,
                  compile_guard)
 

fault/assert_utils.py

@@ -1,3 +1,7 @@
+from magma.bit import Bit
+from magma.when import get_curr_block as get_curr_when_block, no_when
+
+
 def add_compile_guards(compile_guard, verilog_str):
     if compile_guard is None:
         return verilog_str
@@ -14,3 +18,16 @@ def add_compile_guards(compile_guard, verilog_str):
 `endif
 """
     return verilog_str
+
+
+def get_when_cond():
+    """If active when cond, return a boolean that is true when the when
+    condition is true.
+    """
+    if not get_curr_when_block():
+        return None
+    with no_when():
+        when_cond = Bit()
+        when_cond @= 0
+    when_cond @= 1
+    return when_cond

fault/property.py

@@ -3,7 +3,7 @@
 from fault.sva import SVAProperty
 from fault.expression import Expression, UnaryOp, BinaryOp
 from fault.infix import Infix
-from fault.assert_utils import add_compile_guards
+from fault.assert_utils import add_compile_guards, get_when_cond
 
 
 class Property:
@@ -221,6 +221,8 @@ def _compile(self, value):
             # Double escape on curly braces since this will run through format
             # inside inline_verilog logic
             return f"{{{{{contents}}}}}"
+        if isinstance(value, bool):
+            return f"1'b{int(value)}"
         if isinstance(value, int):
             return str(value)
         if isinstance(value, BinaryOp):
@@ -246,6 +248,9 @@ def compile(self, prop):
 
 
 def _make_statement(statement, prop, on, disable_iff, compile_guard, name):
+    if (when_cond := get_when_cond()) is not None:
+        prop = when_cond | implies | prop
+
     format_args = {}
     _compiler = _Compiler(format_args)
     prop = _compiler.compile(prop)

tests/test_property.py

@@ -876,3 +876,151 @@ class Foo(m.Circuit):
         assert not should_pass
     else:
         assert should_pass
+
+
+@requires_ncsim
+def test_cover_when(capsys):
+    class Main(m.Circuit):
+        io = m.IO(I=m.In(m.Bit), S=m.In(m.Bit), O=m.Out(m.Bit)) + m.ClockIO()
+        io.O @= m.Register(T=m.Bit)()(io.I)
+        with m.when(io.S):
+            f.cover(io.I | f.delay[1] | ~io.I, on=f.posedge(io.CLK))
+        with m.otherwise():
+            f.cover(io.I | f.delay[1] | io.I, on=f.posedge(io.CLK))
+    tester = f.SynchronousTester(Main, Main.CLK)
+    tester.circuit.S = 0
+    tester.circuit.I = 1
+    tester.advance_cycle()
+    tester.circuit.I = 1
+    tester.advance_cycle()
+    tester.compile_and_run("system-verilog",
+                           simulator="ncsim",
+                           magma_output="mlir-verilog",
+                           flags=["-sv"],
+                           magma_opts={"sv": True,
+                                       "disable_initial_blocks": True},
+                           disp_type="realtime",
+                           coverage=True)
+
+    out, _ = capsys.readouterr()
+    assert """\
+  Disabled Finish Failed   Assertion Name
+         0      0      0   Main_tb.dut.__cover1
+         0      1      0   Main_tb.dut.__cover2
+  Total Assertions = 2,  Failing Assertions = 0,  Unchecked Assertions = 1\
+""" in out, out
+    tester.clear()
+    tester.circuit.CLK = 0
+    tester.circuit.S = 0
+    tester.circuit.I = 1
+    tester.advance_cycle()
+    tester.circuit.I = 0
+    tester.advance_cycle()
+    tester.compile_and_run("system-verilog", simulator="ncsim",
+                           magma_output="mlir-verilog", flags=["-sv"],
+                           skip_compile=True, disp_type="realtime",
+                           magma_opts={"sv": True,
+                                       "disable_initial_blocks": True},
+                           coverage=True)
+
+    out, _ = capsys.readouterr()
+    assert """\
+  Disabled Finish Failed   Assertion Name
+         0      0      0   Main_tb.dut.__cover1
+         0      0      0   Main_tb.dut.__cover2
+  Total Assertions = 2,  Failing Assertions = 0,  Unchecked Assertions = 2\
+""" in out, out
+    tester.clear()
+    tester.circuit.CLK = 0
+    tester.circuit.S = 1
+    tester.circuit.I = 0
+    tester.advance_cycle()
+    tester.circuit.I = 0
+    tester.advance_cycle()
+    tester.compile_and_run("system-verilog", simulator="ncsim",
+                           flags=["-sv"], skip_compile=True,
+                           magma_opts={"sv": True,
+                                       "disable_initial_blocks": True},
+                           disp_type="realtime", coverage=True)
+
+    out, _ = capsys.readouterr()
+    assert """\
+  Disabled Finish Failed   Assertion Name
+         0      0      0   Main_tb.dut.__cover1
+         0      0      0   Main_tb.dut.__cover2
+  Total Assertions = 2,  Failing Assertions = 0,  Unchecked Assertions = 2\
+""" in out, out
+    tester.clear()
+    tester.circuit.CLK = 0
+    tester.circuit.S = 1
+    tester.circuit.I = 1
+    tester.advance_cycle()
+    tester.circuit.I = 0
+    tester.advance_cycle()
+    tester.compile_and_run("system-verilog",
+                           simulator="ncsim",
+                           magma_output="mlir-verilog",
+                           flags=["-sv"],
+                           skip_compile=True,
+                           disp_type="realtime",
+                           magma_opts={"sv": True,
+                                       "disable_initial_blocks": True},
+                           coverage=True)
+
+    out, _ = capsys.readouterr()
+    # covered
+    assert """\
+  Disabled Finish Failed   Assertion Name
+         0      1      0   Main_tb.dut.__cover1
+         0      0      0   Main_tb.dut.__cover2
+  Total Assertions = 2,  Failing Assertions = 0,  Unchecked Assertions = 1\
+""" in out, out
+
+
+@requires_ncsim
+def test_cover_when_true(capsys):
+    class Main(m.Circuit):
+        io = m.IO(
+            I=m.In(m.Bit), J=m.In(m.Bit), S=m.In(m.Bit), O=m.Out(m.Bit)
+        ) + m.ClockIO()
+        io.O @= m.Register(T=m.Bit)()(io.I)
+        with m.when(io.S):
+            f.cover(True, on=f.posedge(io.CLK))
+        with m.otherwise():
+            f.cover(True, on=f.posedge(io.CLK))
+    tester = f.SynchronousTester(Main, Main.CLK)
+    tester.circuit.S = 0
+    tester.advance_cycle()
+    tester.compile_and_run("system-verilog",
+                           simulator="ncsim",
+                           magma_output="mlir-verilog",
+                           flags=["-sv"],
+                           magma_opts={"sv": True,
+                                       "disable_initial_blocks": True},
+                           disp_type="realtime",
+                           coverage=True)
+
+    out, _ = capsys.readouterr()
+    assert """\
+  Disabled Finish Failed   Assertion Name
+         0      0      0   Main_tb.dut.__cover1
+         0      1      0   Main_tb.dut.__cover2
+  Total Assertions = 2,  Failing Assertions = 0,  Unchecked Assertions = 1\
+""" in out, out
+    tester.clear()
+    tester.circuit.CLK = 0
+    tester.circuit.S = 1
+    tester.advance_cycle()
+    tester.compile_and_run("system-verilog", simulator="ncsim",
+                           flags=["-sv"], skip_compile=True,
+                           magma_opts={"sv": True,
+                                       "disable_initial_blocks": True},
+                           disp_type="realtime", coverage=True)
+
+    out, _ = capsys.readouterr()
+    assert """\
+  Disabled Finish Failed   Assertion Name
+         0      1      0   Main_tb.dut.__cover1
+         0      0      0   Main_tb.dut.__cover2
+  Total Assertions = 2,  Failing Assertions = 0,  Unchecked Assertions = 1\
+""" in out, out