Update BNW axis-async-fifo-c4 test case so that we can both drive the DUT / infer transactions

runt/bi/runt.toml

@@ -2233,39 +2233,39 @@ expect_name = "s4_fixed.bi.expect"
 cmd = "cd ../.. && target/debug/bi --color never --protocol tests/fpga-debugging/axi-burst-s4/s4_fixed.prot --wave tests/fpga-debugging/axi-burst-s4/s4_fixed.vcd --instances TOP.test_l2_cache_wait_state.axi_bus:WriteSubordinate --sample-posedge TOP.test_l2_cache_wait_state.clk --show-waveform-time --time-unit ns 2>&1"
 
 [[tests]]
-name = "bi.tests_fpga_debugging_axi_lite_s1_s1_buggy.s1_buggy_bi"
+name = "bi.tests_fpga_debugging_axi_lite_s1_s1_buggy.s1_buggy_workload2_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"
+expect_name = "s1_buggy_workload2.bi.expect"
 cmd = "cd ../.. && target/debug/bi --color never --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>&1"
 
 [[tests]]
-name = "bi.tests_fpga_debugging_axi_lite_s1_s1_buggy_workload_1.s1_buggy_workload_1_bi"
+name = "bi.tests_fpga_debugging_axi_lite_s1_s1_buggy_workload_1.s1_buggy_workload1_bi"
 paths = [
   "../../tests/fpga-debugging/axi-lite-s1/s1_buggy_workload_1.prot",
 ]
 expect_dir = "../../tests/fpga-debugging/axi-lite-s1/expects"
-expect_name = "s1_buggy_workload_1.bi.expect"
+expect_name = "s1_buggy_workload1.bi.expect"
 cmd = "cd ../.. && target/debug/bi --color never --protocol tests/fpga-debugging/axi-lite-s1/s1_buggy_workload_1.prot --wave tests/fpga-debugging/axi-lite-s1/s1_buggy_workload1.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>&1"
 
 [[tests]]
-name = "bi.tests_fpga_debugging_axi_lite_s1_s1_fixed.s1_fixed_bi"
+name = "bi.tests_fpga_debugging_axi_lite_s1_s1_fixed.s1_fixed_workload2_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"
+expect_name = "s1_fixed_workload2.bi.expect"
 cmd = "cd ../.. && target/debug/bi --color never --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>&1"
 
 [[tests]]
-name = "bi.tests_fpga_debugging_axi_lite_s1_s1_fixed_workload_1.s1_fixed_workload_1_bi"
+name = "bi.tests_fpga_debugging_axi_lite_s1_s1_fixed_workload_1.s1_fixed_workload1_bi"
 paths = [
   "../../tests/fpga-debugging/axi-lite-s1/s1_fixed_workload_1.prot",
 ]
 expect_dir = "../../tests/fpga-debugging/axi-lite-s1/expects"
-expect_name = "s1_fixed_workload_1.bi.expect"
+expect_name = "s1_fixed_workload1.bi.expect"
 cmd = "cd ../.. && target/debug/bi --color never --protocol tests/fpga-debugging/axi-lite-s1/s1_fixed_workload_1.prot --wave tests/fpga-debugging/axi-lite-s1/s1_fixed_workload1.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>&1"
 
 [[tests]]
@@ -2305,22 +2305,22 @@ expect_name = "s3_fixed.bi.expect"
 cmd = "cd ../.. && target/debug/bi --color never --protocol tests/fpga-debugging/axis-adapter-s3/s3_fixed.prot --wave tests/fpga-debugging/axis-adapter-s3/s3_fixed.fst --instances TOP.test_axis_adapter_64_8.UUT:AXISManager --sample-posedge TOP.test_axis_adapter_64_8.UUT.clk --show-waveform-time --time-unit ns 2>&1"
 
 [[tests]]
-name = "bi.tests_fpga_debugging_axis_async_fifo_c4_c4_buggy.c4_buggy_bi"
+name = "bi.tests_fpga_debugging_axis_async_fifo_c4_c4.c4_buggy_bi"
 paths = [
-  "../../tests/fpga-debugging/axis-async-fifo-c4/c4_buggy.prot",
+  "../../tests/fpga-debugging/axis-async-fifo-c4/c4.prot",
 ]
 expect_dir = "../../tests/fpga-debugging/axis-async-fifo-c4/expects"
 expect_name = "c4_buggy.bi.expect"
-cmd = "cd ../.. && target/debug/bi --color never --protocol tests/fpga-debugging/axis-async-fifo-c4/c4_buggy.prot --wave tests/fpga-debugging/axis-async-fifo-c4/c4_buggy.fst --instances TOP.test_axis_async_fifo.UUT.axis_reg_inst:Sender TOP.test_axis_async_fifo.UUT.axis_reg_inst:Receiver --sample-posedge TOP.test_axis_async_fifo.UUT.axis_reg_inst.clk --show-waveform-time --time-unit ns 2>&1"
+cmd = "cd ../.. && target/debug/bi --color never --protocol tests/fpga-debugging/axis-async-fifo-c4/c4.prot --wave tests/fpga-debugging/axis-async-fifo-c4/c4_buggy.fst --instances TOP.test_axis_async_fifo.UUT.axis_reg_inst:AsyncFifo --sample-posedge TOP.test_axis_async_fifo.UUT.axis_reg_inst.clk --show-waveform-time --time-unit ns 2>&1"
 
 [[tests]]
-name = "bi.tests_fpga_debugging_axis_async_fifo_c4_c4_fixed.c4_fixed_bi"
+name = "bi.tests_fpga_debugging_axis_async_fifo_c4_c4.c4_fixed_bi"
 paths = [
-  "../../tests/fpga-debugging/axis-async-fifo-c4/c4_fixed.prot",
+  "../../tests/fpga-debugging/axis-async-fifo-c4/c4.prot",
 ]
 expect_dir = "../../tests/fpga-debugging/axis-async-fifo-c4/expects"
 expect_name = "c4_fixed.bi.expect"
-cmd = "cd ../.. && target/debug/bi --color never --protocol tests/fpga-debugging/axis-async-fifo-c4/c4_fixed.prot --wave tests/fpga-debugging/axis-async-fifo-c4/c4_fixed.fst --instances TOP.test_axis_async_fifo.UUT.axis_reg_inst:Sender TOP.test_axis_async_fifo.UUT.axis_reg_inst:Receiver --sample-posedge TOP.test_axis_async_fifo.UUT.axis_reg_inst.clk --show-waveform-time --time-unit ns 2>&1"
+cmd = "cd ../.. && target/debug/bi --color never --protocol tests/fpga-debugging/axis-async-fifo-c4/c4.prot --wave tests/fpga-debugging/axis-async-fifo-c4/c4_fixed.fst --instances TOP.test_axis_async_fifo.UUT.axis_reg_inst:AsyncFifo --sample-posedge TOP.test_axis_async_fifo.UUT.axis_reg_inst.clk --show-waveform-time --time-unit ns --max-traces 20 2>&1"
 
 [[tests]]
 name = "bi.tests_fpga_debugging_axis_fifo_d11_d11_buggy.d11_buggy_bi"

runt/fail/runt.toml

@@ -324,6 +324,24 @@ expect_dir = "../../tests/fifo/expects"
 expect_name = "push_pop_conflict.fail.expect"
 cmd = "cd ../.. && target/debug/graph-interp --transactions tests/fifo/push_pop_conflict.tx --transition-system --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.prot --module fifo_wrapper 2>/dev/null"
 
+[[tests]]
+name = "fail.tests_fpga_debugging_axis_async_fifo_c4_c4_buggy.c4_buggy_fail.graph"
+paths = [
+  "../../tests/fpga-debugging/axis-async-fifo-c4/c4_buggy.tx",
+]
+expect_dir = "../../tests/fpga-debugging/axis-async-fifo-c4/expects"
+expect_name = "c4_buggy.fail.expect"
+cmd = "cd ../.. && target/debug/graph-interp --transactions tests/fpga-debugging/axis-async-fifo-c4/c4_buggy.tx --respect-forks --determinize --brief-graph-errors --verilog tests/fpga-debugging/axis-async-fifo-c4/c4_dut.v tests/fpga-debugging/axis-async-fifo-c4/c4_buggy.v --protocol tests/fpga-debugging/axis-async-fifo-c4/c4.prot --module c4_dut 2>/dev/null"
+
+[[tests]]
+name = "fail.tests_fpga_debugging_axis_async_fifo_c4_c4_buggy.c4_buggy_fail.ts"
+paths = [
+  "../../tests/fpga-debugging/axis-async-fifo-c4/c4_buggy.tx",
+]
+expect_dir = "../../tests/fpga-debugging/axis-async-fifo-c4/expects"
+expect_name = "c4_buggy.fail.expect"
+cmd = "cd ../.. && target/debug/graph-interp --transactions tests/fpga-debugging/axis-async-fifo-c4/c4_buggy.tx --transition-system --verilog tests/fpga-debugging/axis-async-fifo-c4/c4_dut.v tests/fpga-debugging/axis-async-fifo-c4/c4_buggy.v --protocol tests/fpga-debugging/axis-async-fifo-c4/c4.prot --module c4_dut 2>/dev/null"
+
 [[tests]]
 name = "fail.tests_identities_identity_d1_explicit_fork.explicit_fork_fail.graph"
 paths = [

runt/graph_interp/runt.toml

@@ -531,6 +531,33 @@ expect_dir = "../../tests/fifo/expects"
 expect_name = "push_pop_identity_ok.graph_interp.expect"
 cmd = "cd ../.. && target/debug/graph-interp --transactions tests/fifo/push_pop_identity_ok.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.prot --module fifo_wrapper --respect-forks --determinize 2>/dev/null"
 
+[[tests]]
+name = "graph_interp.tests_fpga_debugging_axis_async_fifo_c4_c4_fixed.c4_fixed_graph_interp"
+paths = [
+  "../../tests/fpga-debugging/axis-async-fifo-c4/c4_fixed.tx",
+]
+expect_dir = "../../tests/fpga-debugging/axis-async-fifo-c4/expects"
+expect_name = "c4_fixed.graph_interp.expect"
+cmd = "cd ../.. && target/debug/graph-interp --transactions tests/fpga-debugging/axis-async-fifo-c4/c4_fixed.tx --verilog tests/fpga-debugging/axis-async-fifo-c4/c4_dut.v tests/fpga-debugging/axis-async-fifo-c4/c4_fixed.v --protocol tests/fpga-debugging/axis-async-fifo-c4/c4.prot --module c4_dut 2>/dev/null"
+
+[[tests]]
+name = "graph_interp.tests_fpga_debugging_axis_async_fifo_c4_c4_fixed.c4_fixed_graph_interp.contract_edges"
+paths = [
+  "../../tests/fpga-debugging/axis-async-fifo-c4/c4_fixed.tx",
+]
+expect_dir = "../../tests/fpga-debugging/axis-async-fifo-c4/expects"
+expect_name = "c4_fixed.graph_interp.expect"
+cmd = "cd ../.. && target/debug/graph-interp --transactions tests/fpga-debugging/axis-async-fifo-c4/c4_fixed.tx --verilog tests/fpga-debugging/axis-async-fifo-c4/c4_dut.v tests/fpga-debugging/axis-async-fifo-c4/c4_fixed.v --protocol tests/fpga-debugging/axis-async-fifo-c4/c4.prot --module c4_dut --contract-edges 2>/dev/null"
+
+[[tests]]
+name = "graph_interp.tests_fpga_debugging_axis_async_fifo_c4_c4_fixed.c4_fixed_graph_interp.respect_forks"
+paths = [
+  "../../tests/fpga-debugging/axis-async-fifo-c4/c4_fixed.tx",
+]
+expect_dir = "../../tests/fpga-debugging/axis-async-fifo-c4/expects"
+expect_name = "c4_fixed.graph_interp.expect"
+cmd = "cd ../.. && target/debug/graph-interp --transactions tests/fpga-debugging/axis-async-fifo-c4/c4_fixed.tx --verilog tests/fpga-debugging/axis-async-fifo-c4/c4_dut.v tests/fpga-debugging/axis-async-fifo-c4/c4_fixed.v --protocol tests/fpga-debugging/axis-async-fifo-c4/c4.prot --module c4_dut --respect-forks --determinize 2>/dev/null"
+
 [[tests]]
 name = "graph_interp.tests_identities_identity_d0_passthrough_combdep.passthrough_combdep_graph_interp"
 paths = [

runt/interp/runt.toml

@@ -441,6 +441,24 @@ expect_dir = "../../tests/fifo/expects"
 expect_name = "push_pop_identity_ok.interp.expect"
 cmd = "cd ../.. && target/debug/protocols-interp --color never --transactions tests/fifo/push_pop_identity_ok.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.prot --module fifo_wrapper 2>&1"
 
+[[tests]]
+name = "interp.tests_fpga_debugging_axis_async_fifo_c4_c4_buggy.c4_buggy_interp"
+paths = [
+  "../../tests/fpga-debugging/axis-async-fifo-c4/c4_buggy.tx",
+]
+expect_dir = "../../tests/fpga-debugging/axis-async-fifo-c4/expects"
+expect_name = "c4_buggy.interp.expect"
+cmd = "cd ../.. && target/debug/protocols-interp --color never --transactions tests/fpga-debugging/axis-async-fifo-c4/c4_buggy.tx --verilog tests/fpga-debugging/axis-async-fifo-c4/c4_dut.v tests/fpga-debugging/axis-async-fifo-c4/c4_buggy.v --protocol tests/fpga-debugging/axis-async-fifo-c4/c4.prot --module c4_dut 2>&1"
+
+[[tests]]
+name = "interp.tests_fpga_debugging_axis_async_fifo_c4_c4_fixed.c4_fixed_interp"
+paths = [
+  "../../tests/fpga-debugging/axis-async-fifo-c4/c4_fixed.tx",
+]
+expect_dir = "../../tests/fpga-debugging/axis-async-fifo-c4/expects"
+expect_name = "c4_fixed.interp.expect"
+cmd = "cd ../.. && target/debug/protocols-interp --color never --transactions tests/fpga-debugging/axis-async-fifo-c4/c4_fixed.tx --verilog tests/fpga-debugging/axis-async-fifo-c4/c4_dut.v tests/fpga-debugging/axis-async-fifo-c4/c4_fixed.v --protocol tests/fpga-debugging/axis-async-fifo-c4/c4.prot --module c4_dut 2>&1"
+
 [[tests]]
 name = "interp.tests_identities_dual_identity_d0_dual_identity_d0_combdep.dual_identity_d0_combdep_interp"
 paths = [

runt/waveform/runt.toml

@@ -513,6 +513,33 @@ expect_dir = "../../tests/fifo/expects"
 expect_name = "push_pop_identity_ok.waveform.expect"
 cmd = "cd ../.. && target/debug/graph-interp --transactions tests/fifo/push_pop_identity_ok.tx --transition-system --ascii-waveform --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.prot --module fifo_wrapper 2>/dev/null"
 
+[[tests]]
+name = "waveform.tests_fpga_debugging_axis_async_fifo_c4_c4_fixed.c4_fixed_waveform.ast"
+paths = [
+  "../../tests/fpga-debugging/axis-async-fifo-c4/c4_fixed.tx",
+]
+expect_dir = "../../tests/fpga-debugging/axis-async-fifo-c4/expects"
+expect_name = "c4_fixed.waveform.expect"
+cmd = "cd ../.. && target/debug/protocols-interp --color never --transactions tests/fpga-debugging/axis-async-fifo-c4/c4_fixed.tx --ascii-waveform --verilog tests/fpga-debugging/axis-async-fifo-c4/c4_dut.v tests/fpga-debugging/axis-async-fifo-c4/c4_fixed.v --protocol tests/fpga-debugging/axis-async-fifo-c4/c4.prot --module c4_dut 2>/dev/null"
+
+[[tests]]
+name = "waveform.tests_fpga_debugging_axis_async_fifo_c4_c4_fixed.c4_fixed_waveform.graph"
+paths = [
+  "../../tests/fpga-debugging/axis-async-fifo-c4/c4_fixed.tx",
+]
+expect_dir = "../../tests/fpga-debugging/axis-async-fifo-c4/expects"
+expect_name = "c4_fixed.waveform.expect"
+cmd = "cd ../.. && target/debug/graph-interp --transactions tests/fpga-debugging/axis-async-fifo-c4/c4_fixed.tx --respect-forks --determinize --ascii-waveform --verilog tests/fpga-debugging/axis-async-fifo-c4/c4_dut.v tests/fpga-debugging/axis-async-fifo-c4/c4_fixed.v --protocol tests/fpga-debugging/axis-async-fifo-c4/c4.prot --module c4_dut 2>/dev/null"
+
+[[tests]]
+name = "waveform.tests_fpga_debugging_axis_async_fifo_c4_c4_fixed.c4_fixed_waveform.ts"
+paths = [
+  "../../tests/fpga-debugging/axis-async-fifo-c4/c4_fixed.tx",
+]
+expect_dir = "../../tests/fpga-debugging/axis-async-fifo-c4/expects"
+expect_name = "c4_fixed.waveform.expect"
+cmd = "cd ../.. && target/debug/graph-interp --transactions tests/fpga-debugging/axis-async-fifo-c4/c4_fixed.tx --transition-system --ascii-waveform --verilog tests/fpga-debugging/axis-async-fifo-c4/c4_dut.v tests/fpga-debugging/axis-async-fifo-c4/c4_fixed.v --protocol tests/fpga-debugging/axis-async-fifo-c4/c4.prot --module c4_dut 2>/dev/null"
+
 [[tests]]
 name = "waveform.tests_identities_identity_d0_passthrough_combdep.passthrough_combdep_waveform.ast"
 paths = [

scripts/generate_runt_configs.py

@@ -74,10 +74,12 @@ def replace_non_alphanumerics(value: object) -> str:
 
 
 def case_stem(case: dict) -> str:
-    # antmicro cases share one .prot but differ by wave, so name them by
-    # the wave; otherwise use the test file's stem (dropping a .bi suffix).
+    # Antmicro & Brave New World test cases for the BI share the same `.prot`
+    # file but have multiple waveforms, so we use the waveform files'
+    # names to identify a particular test, otherwise we use the `.prot` file's stem
+    # to identify a test
     wave = case.get("wave")
-    if wave and "antmicro" in wave:
+    if wave and ("antmicro" in wave or "fpga-debugging" in wave):
         return Path(wave).stem
     stem = Path(case["paths"][0]).stem
     return stem.removesuffix(".bi")

scripts/test_catalog.py

@@ -305,6 +305,24 @@
         "top": "fifo_wrapper",
         "expect": "pass",
     },
+    "tests/fpga-debugging/axis-async-fifo-c4/c4_buggy.tx": {
+        "protocol": "tests/fpga-debugging/axis-async-fifo-c4/c4.prot",
+        "verilog": (
+            "tests/fpga-debugging/axis-async-fifo-c4/c4_dut.v",
+            "tests/fpga-debugging/axis-async-fifo-c4/c4_buggy.v",
+        ),
+        "top": "c4_dut",
+        "expect": "assertion_mismatch",
+    },
+    "tests/fpga-debugging/axis-async-fifo-c4/c4_fixed.tx": {
+        "protocol": "tests/fpga-debugging/axis-async-fifo-c4/c4.prot",
+        "verilog": (
+            "tests/fpga-debugging/axis-async-fifo-c4/c4_dut.v",
+            "tests/fpga-debugging/axis-async-fifo-c4/c4_fixed.v",
+        ),
+        "top": "c4_dut",
+        "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",),
@@ -701,12 +719,9 @@
         ),
     },
     "tests.fpga-debugging.axis-async-fifo-c4.c4_buggy": {
-        "protocol": "tests/fpga-debugging/axis-async-fifo-c4/c4_buggy.prot",
+        "protocol": "tests/fpga-debugging/axis-async-fifo-c4/c4.prot",
         "wave": "tests/fpga-debugging/axis-async-fifo-c4/c4_buggy.fst",
-        "instances": (
-            "TOP.test_axis_async_fifo.UUT.axis_reg_inst:Sender",
-            "TOP.test_axis_async_fifo.UUT.axis_reg_inst:Receiver",
-        ),
+        "instances": ("TOP.test_axis_async_fifo.UUT.axis_reg_inst:AsyncFifo",),
         "expect": None,
         "extra_args": (
             "--sample-posedge",
@@ -717,19 +732,18 @@
         ),
     },
     "tests.fpga-debugging.axis-async-fifo-c4.c4_fixed": {
-        "protocol": "tests/fpga-debugging/axis-async-fifo-c4/c4_fixed.prot",
+        "protocol": "tests/fpga-debugging/axis-async-fifo-c4/c4.prot",
         "wave": "tests/fpga-debugging/axis-async-fifo-c4/c4_fixed.fst",
-        "instances": (
-            "TOP.test_axis_async_fifo.UUT.axis_reg_inst:Sender",
-            "TOP.test_axis_async_fifo.UUT.axis_reg_inst:Receiver",
-        ),
+        "instances": ("TOP.test_axis_async_fifo.UUT.axis_reg_inst:AsyncFifo",),
         "expect": "pass",
         "extra_args": (
             "--sample-posedge",
             "TOP.test_axis_async_fifo.UUT.axis_reg_inst.clk",
             "--show-waveform-time",
             "--time-unit",
             "ns",
+            "--max-traces",
+            "20",
         ),
     },
     "tests.fpga-debugging.axis-fifo-d11.d11_buggy": {