(WIP) Use same protocol to both drive DUT + infer transactions for BNW axi-lite-s1 bug

.github/workflows/test.yml

@@ -36,6 +36,8 @@ jobs:
       run: runt runt/graph_interp
     - name: Run Runt tests for monitor
       run: runt runt/monitor
+    - name: Run Runt tests for bi
+      run: runt runt/bi
 
   test-freshness:
     name: Check Generated Runt Configs are Fresh

.gitignore

@@ -36,3 +36,4 @@ scripts/_catalog_gen.py
 !tests/fpga-debugging/axis-async-fifo-c4/*.png
 
 /*.fst
+scripts/__pycache__/

justfile

@@ -1,8 +1,9 @@
 # Runs the Runt snapshot suites that together cover every test
 runt:
-  cargo build --offline --package protocols-interp --package protocols-monitor --package graph-interp
+  cargo build --offline --package protocols-interp --package protocols-monitor --package graph-interp --package bi
   runt --max-futures 1 runt/interp
   runt --max-futures 1 runt/monitor
+  runt --max-futures 1 runt/bi
   runt --max-futures 1 runt/graph_interp
   runt --max-futures 1 runt/waveform
 

runt/bi/runt.toml

@@ -0,0 +1,19 @@
+ver = "0.4.1"
+
+[[tests]]
+name = "bi.tests_fpga_debugging_axi_lite_s1_s1_buggy.s1_buggy_bi"
+paths = [
+  "../../tests/fpga-debugging/axi-lite-s1/s1_buggy.prot",
+]
+expect_dir = "../../tests/fpga-debugging/axi-lite-s1/expects"
+expect_name = "s1_buggy.bi.expect"
+cmd = "cd ../.. && target/debug/bi --protocol tests/fpga-debugging/axi-lite-s1/s1_buggy.prot --wave tests/fpga-debugging/axi-lite-s1/s1_buggy_interp.fst --instances dut:WriteSubordinate --show-steps --include-in-progress 2>/dev/null"
+
+[[tests]]
+name = "bi.tests_fpga_debugging_axi_lite_s1_s1_fixed.s1_fixed_bi"
+paths = [
+  "../../tests/fpga-debugging/axi-lite-s1/s1_fixed.prot",
+]
+expect_dir = "../../tests/fpga-debugging/axi-lite-s1/expects"
+expect_name = "s1_fixed.bi.expect"
+cmd = "cd ../.. && target/debug/bi --protocol tests/fpga-debugging/axi-lite-s1/s1_fixed.prot --wave tests/fpga-debugging/axi-lite-s1/s1_fixed_interp.fst --instances dut:WriteSubordinate --show-steps 2>/dev/null"

runt/interp/runt.toml

@@ -495,6 +495,24 @@ expect_dir = "../../tests/fifo/expects"
 expect_name = "push_pop_loop_not_empty.interp.expect"
 cmd = "cd ../.. && target/debug/protocols-interp --color never --transactions tests/fifo/push_pop_loop_not_empty.tx --verilog tests/fifo/bsg_mem_1rw_sync.v tests/fifo/bsg_mem_1rw_sync_synth.v tests/fifo/bsg_circular_ptr.v tests/fifo/bsg_fifo_1rw_large.v tests/fifo/fifo_wrapper.v --protocol tests/fifo/fifo_bounded_loop.prot --module fifo_wrapper 2>&1"
 
+[[tests]]
+name = "interp.tests_fpga_debugging_axi_lite_s1_s1_buggy.s1_buggy_interp"
+paths = [
+  "../../tests/fpga-debugging/axi-lite-s1/s1_buggy.tx",
+]
+expect_dir = "../../tests/fpga-debugging/axi-lite-s1/expects"
+expect_name = "s1_buggy.interp.expect"
+cmd = "cd ../.. && target/debug/protocols-interp --color never --transactions tests/fpga-debugging/axi-lite-s1/s1_buggy.tx --verilog tests/fpga-debugging/axi-lite-s1/s1_buggy.v --protocol tests/fpga-debugging/axi-lite-s1/s1_buggy.prot --module xlnxdemo --max-steps 300 2>&1"
+
+[[tests]]
+name = "interp.tests_fpga_debugging_axi_lite_s1_s1_fixed.s1_fixed_interp"
+paths = [
+  "../../tests/fpga-debugging/axi-lite-s1/s1_fixed.tx",
+]
+expect_dir = "../../tests/fpga-debugging/axi-lite-s1/expects"
+expect_name = "s1_fixed.interp.expect"
+cmd = "cd ../.. && target/debug/protocols-interp --color never --transactions tests/fpga-debugging/axi-lite-s1/s1_fixed.tx --verilog tests/fpga-debugging/axi-lite-s1/s1_fixed.v --protocol tests/fpga-debugging/axi-lite-s1/s1_fixed.prot --module xlnxdemo --max-steps 300 2>&1"
+
 [[tests]]
 name = "interp.tests_identities_dual_identity_d0_dual_identity_d0_combdep.dual_identity_d0_combdep_interp"
 paths = [

runt/monitor/runt.toml

@@ -1240,7 +1240,7 @@ paths = [
 ]
 expect_dir = "../../tests/fpga-debugging/axi-lite-s1/expects"
 expect_name = "s1_buggy.monitor.expect"
-cmd = "cd ../.. && target/debug/protocols-monitor --protocol tests/fpga-debugging/axi-lite-s1/s1_buggy.prot --wave tests/fpga-debugging/axi-lite-s1/s1_buggy_workload2.vcd --instances TOP.testbench.UUT:WriteSubordinate TOP.testbench.UUT:ReadSubordinate --sample-posedge TOP.testbench.UUT.S_AXI_ACLK --show-waveform-time --time-unit ns --include-idle 2>/dev/null"
+cmd = "cd ../.. && target/debug/protocols-monitor --protocol tests/fpga-debugging/axi-lite-s1/s1_buggy.prot --wave tests/fpga-debugging/axi-lite-s1/s1_buggy_workload2.vcd --instances TOP.testbench.UUT:WriteSubordinate --sample-posedge TOP.testbench.UUT.S_AXI_ACLK --show-waveform-time --time-unit ns --include-idle 2>/dev/null"
 
 [[tests]]
 name = "monitor.tests_fpga_debugging_axi_lite_s1_s1_buggy_workload_1.s1_buggy_workload_1_monitor"
@@ -1258,7 +1258,7 @@ paths = [
 ]
 expect_dir = "../../tests/fpga-debugging/axi-lite-s1/expects"
 expect_name = "s1_fixed.monitor.expect"
-cmd = "cd ../.. && target/debug/protocols-monitor --protocol tests/fpga-debugging/axi-lite-s1/s1_fixed.prot --wave tests/fpga-debugging/axi-lite-s1/s1_fixed_workload2.vcd --instances TOP.testbench.UUT:WriteSubordinate TOP.testbench.UUT:ReadSubordinate --sample-posedge TOP.testbench.UUT.S_AXI_ACLK --show-waveform-time --time-unit ns --include-idle 2>/dev/null"
+cmd = "cd ../.. && target/debug/protocols-monitor --protocol tests/fpga-debugging/axi-lite-s1/s1_fixed.prot --wave tests/fpga-debugging/axi-lite-s1/s1_fixed_workload2.vcd --instances TOP.testbench.UUT:WriteSubordinate --sample-posedge TOP.testbench.UUT.S_AXI_ACLK --show-waveform-time --time-unit ns --include-idle 2>/dev/null"
 
 [[tests]]
 name = "monitor.tests_fpga_debugging_axi_lite_s1_s1_fixed_workload_1.s1_fixed_workload_1_monitor"

scripts/generate_runt_configs.py

@@ -62,6 +62,25 @@ def load_monitor_cases() -> list[dict]:
     return out
 
 
+def load_bi_cases() -> list[dict]:
+    """Same as load_monitor_cases but for the bi cases"""
+    out = []
+    for case_id, c in test_catalog.BI_CASES.items():
+        out.append(
+            {
+                "id": case_id,
+                "path": c["protocol"],
+                "wave": c.get("wave"),
+                "instances": c.get("instances", ()),
+                "max_steps": c.get("max_steps"),
+                "timeout_secs": c.get("timeout_secs"),
+                "extra_args": c.get("extra_args", ()),
+                "expected": c["expect"],
+            }
+        )
+    return out
+
+
 # helper function to escape globs in places
 def runt_glob_literal(path: str) -> str:
     return path.replace("[", "[[]").replace("*", "[*]").replace("?", "[?]")
@@ -195,6 +214,19 @@ def monitor_runt_command(case: dict) -> list[tuple[str, str]]:
     return [("", repo_root_command(cmd))]
 
 
+# Same as `monitor_runt_command` above but for BI test cases
+def bi_runt_command(case: dict) -> list[tuple[str, str]]:
+    cmd = [*binary_prefix("bi"), "--protocol", case["path"]]
+    if case["wave"]:
+        cmd += ["--wave", case["wave"]]
+    if case["instances"]:
+        cmd += ["--instances", *case["instances"]]
+    cmd += case["extra_args"]
+    if case["timeout_secs"] is not None:
+        cmd = timeout_cmd(case["timeout_secs"], cmd)
+    return [("", repo_root_command(cmd))]
+
+
 def waveform_runt_command(case: dict) -> list[tuple[str, str]]:
     ast_cmd = [
         *binary_prefix("protocols-interp"),
@@ -226,6 +258,7 @@ def waveform_runt_command(case: dict) -> list[tuple[str, str]]:
     "interp": interp_runt_command,
     "graph_interp": graph_interp_runt_command,
     "monitor": monitor_runt_command,
+    "bi": bi_runt_command,
     "waveform": waveform_runt_command,
 }
 
@@ -330,11 +363,13 @@ def write_runt_toml(output_dir: Path, suites) -> None:
 def generate_runt_configs() -> None:
     tx = load_tx_cases()
     mon = load_monitor_cases()
+    bi = load_bi_cases()
     # Each suite maps a name to (runner, cases). interp + monitor + graph_interp
     # together cover every test.
     suite_specs = {
         "interp": ("interp", tx),
         "monitor": ("monitor", mon),
+        "bi": ("bi", bi),
         "graph_interp": ("graph_interp", graph_interp_cases(tx)),
         "waveform": ("waveform", waveform_cases(tx)),
     }

scripts/test_catalog.py

@@ -1,7 +1,7 @@
 # Checked-in test catalog. Hand-maintained source of truth.
 # Consumed by scripts/generate_runt_configs.py and scripts/benchmark_monitor.py.
 #
-# TX_CASES are keyed by their .tx path. MONITOR_CASES are keyed by a unique id
+# TX_CASES are keyed by their .tx path. MONITOR_CASES & BI_CASES are both keyed by a unique id
 
 TX_CASES = {
     "examples/picorv32/unsigned_mul.tx": {
@@ -349,6 +349,20 @@
         "top": "fifo_wrapper",
         "expect": "pass",
     },
+    "tests/fpga-debugging/axi-lite-s1/s1_buggy.tx": {
+        "protocol": "tests/fpga-debugging/axi-lite-s1/s1_buggy.prot",
+        "verilog": ("tests/fpga-debugging/axi-lite-s1/s1_buggy.v",),
+        "top": "xlnxdemo",
+        "max_steps": 300,
+        "expect": "assignment_conflict",
+    },
+    "tests/fpga-debugging/axi-lite-s1/s1_fixed.tx": {
+        "protocol": "tests/fpga-debugging/axi-lite-s1/s1_fixed.prot",
+        "verilog": ("tests/fpga-debugging/axi-lite-s1/s1_fixed.v",),
+        "top": "xlnxdemo",
+        "max_steps": 300,
+        "expect": "pass",
+    },
     "tests/identities/dual_identity_d0/dual_identity_d0_combdep.tx": {
         "protocol": "tests/identities/dual_identity_d0/dual_identity_d0.prot",
         "verilog": ("tests/identities/dual_identity_d0/dual_identity_d0.v",),
@@ -660,10 +674,7 @@
     "tests.fpga-debugging.axi-lite-s1.s1_buggy": {
         "protocol": "tests/fpga-debugging/axi-lite-s1/s1_buggy.prot",
         "wave": "tests/fpga-debugging/axi-lite-s1/s1_buggy_workload2.vcd",
-        "instances": (
-            "TOP.testbench.UUT:WriteSubordinate",
-            "TOP.testbench.UUT:ReadSubordinate",
-        ),
+        "instances": ("TOP.testbench.UUT:WriteSubordinate",),
         "expect": None,
         "extra_args": (
             "--sample-posedge",
@@ -694,11 +705,11 @@
     "tests.fpga-debugging.axi-lite-s1.s1_fixed": {
         "protocol": "tests/fpga-debugging/axi-lite-s1/s1_fixed.prot",
         "wave": "tests/fpga-debugging/axi-lite-s1/s1_fixed_workload2.vcd",
-        "instances": (
-            "TOP.testbench.UUT:WriteSubordinate",
-            "TOP.testbench.UUT:ReadSubordinate",
-        ),
-        "expect": "pass",
+        "instances": ("TOP.testbench.UUT:WriteSubordinate",),
+        # The monitor doesn't work for this protocol due to a known bug
+        # (inability to handle multiple assignments to the same port within the same cycle).
+        # See https://github.com/cucapra/protocols/issues/214
+        "expect": None,
         "extra_args": (
             "--sample-posedge",
             "TOP.testbench.UUT.S_AXI_ACLK",
@@ -1099,3 +1110,24 @@ def _antmicro_case(stem):
         for stem in ANTMICRO_TRACE_STEMS
     }
 )
+
+# The filepath supplied to the `wave` field are .fst files produced by the interpreter.
+BI_CASES = {
+    "tests.fpga-debugging.axi-lite-s1.s1_buggy.bi": {
+        "protocol": "tests/fpga-debugging/axi-lite-s1/s1_buggy.prot",
+        "wave": "tests/fpga-debugging/axi-lite-s1/s1_buggy_interp.fst",
+        "instances": ("dut:WriteSubordinate",),
+        # `--include-in-progress` makes `bi` report the two writes that
+        # started but whose responses never completed, surfacing the
+        # lost-write-response bug on the monitoring side.
+        "expect": None,
+        "extra_args": ("--show-steps", "--include-in-progress"),
+    },
+    "tests.fpga-debugging.axi-lite-s1.s1_fixed.bi": {
+        "protocol": "tests/fpga-debugging/axi-lite-s1/s1_fixed.prot",
+        "wave": "tests/fpga-debugging/axi-lite-s1/s1_fixed_interp.fst",
+        "instances": ("dut:WriteSubordinate",),
+        "expect": None,
+        "extra_args": ("--show-steps",),
+    },
+}

tests/fpga-debugging/axi-lite-s1/expects/s1_buggy.bi.expect

@@ -0,0 +1,13 @@
+// trace 0
+trace {
+    reset(); [0]
+    write(8, 7, X, 0); [7 .. ]
+    write(4, 42, X, 4); [1 .. ]
+}
+
+// trace 1
+trace {
+    reset(); [0]
+    write(8, 7, X, 0); [7 .. ]
+    write(4, 42, X, 3); [2 .. ]
+}

tests/fpga-debugging/axi-lite-s1/expects/s1_buggy.interp.expect

@@ -0,0 +1,15 @@
+error: Thread 1 (`write`) attempted conflicting assignment to 'S_AXI_BREADY': current=1, new=0
+   ┌─ tests/fpga-debugging/axi-lite-s1/s1_buggy.prot:83:5
+   │
+83 │     DUT.S_AXI_BREADY := 1'b0;
+   │     ^^^^^^^^^^^^^^^^^^^^^^^^^ Thread 1 (`write`) attempted conflicting assignment to 'S_AXI_BREADY': current=1, new=0
+
+error: Thread 2 (`write`) attempted conflicting assignment to 'S_AXI_BREADY': current=0, new=1
+   ┌─ tests/fpga-debugging/axi-lite-s1/s1_buggy.prot:95:5
+   │
+95 │     DUT.S_AXI_BREADY := 1'b1;
+   │     ^^^^^^^^^^^^^^^^^^^^^^^^^ Thread 2 (`write`) attempted conflicting assignment to 'S_AXI_BREADY': current=0, new=1
+
+Trace 0 execution failed.
+---CODE---
+101

tests/fpga-debugging/axi-lite-s1/expects/s1_fixed.bi.expect

@@ -0,0 +1,43 @@
+// trace 0
+trace {
+    reset(); [0]
+    write(4, 42, 0, 4); [1 .. 12]
+    write(8, 7, 0, 0); [7 .. 14]
+}
+
+// trace 1
+trace {
+    reset(); [0]
+    write(4, 42, 0, 4); [1 .. 12]
+    write(8, 7, 0, 0); [7 .. 14]
+}
+
+// trace 2
+trace {
+    reset(); [0]
+    write(4, 42, 0, 4); [1 .. 12]
+    write(8, 7, 0, 0); [7 .. 14]
+}
+
+// trace 3
+trace {
+    reset(); [0]
+    write(4, 42, 0, 4); [1 .. 12]
+    write(8, 7, 0, 0); [7 .. 14]
+}
+
+// trace 4
+trace {
+    reset(); [0]
+    write(4, 42, 0, 4); [1 .. 12]
+    write(8, 7, 0, 0); [7 .. 14]
+}
+
+// trace 5
+trace {
+    reset(); [0]
+    write(4, 42, 0, 4); [1 .. 12]
+    write(8, 7, 0, 0); [7 .. 14]
+}
+---CODE---
+1

tests/fpga-debugging/axi-lite-s1/expects/s1_fixed.interp.expect

@@ -0,0 +1 @@
+Trace 0 executed successfully!

tests/fpga-debugging/axi-lite-s1/expects/s1_fixed.monitor.expect

@@ -1,8 +1,2 @@
-// trace 0
-trace {
-    WriteSubordinate::idle();  // [time: 0ns -> 25ns]
-    ReadSubordinate::idle();  // [time: 0ns -> 25ns]
-    WriteSubordinate::write(64, 2147483648, 0, 0);  // [time: 25ns -> 100ns]
-    ReadSubordinate::read_v2(68, 0, 1);  // [time: 50ns -> 125ns]
-    ReadSubordinate::idle();  // [time: 125ns -> 150ns]
-}
+---CODE---
+1