From 1910ed78240e7ed3a51fca1f9e9fb9e597dd0fc4 Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Mon, 24 Aug 2026 18:25:17 -0400 Subject: [PATCH 01/29] Delete old versions of s3 protocol --- .../axis-adapter-s3/s3_buggy.prot | 113 ------------------ .../axis-adapter-s3/s3_fixed.prot | 113 ------------------ 2 files changed, 226 deletions(-) delete mode 100644 tests/fpga-debugging/axis-adapter-s3/s3_buggy.prot delete mode 100644 tests/fpga-debugging/axis-adapter-s3/s3_fixed.prot diff --git a/tests/fpga-debugging/axis-adapter-s3/s3_buggy.prot b/tests/fpga-debugging/axis-adapter-s3/s3_buggy.prot deleted file mode 100644 index 023e0f32..00000000 --- a/tests/fpga-debugging/axis-adapter-s3/s3_buggy.prot +++ /dev/null @@ -1,113 +0,0 @@ -// Source (manager) that outputs a sequence of 8 words -struct AXISManager { - // Control signals - in rst: u1, // Active-low reset - - // AXI-Stream manager outputs (from DUT perspective) - out output_axis_tvalid: u1, // manager has valid data - out output_axis_tdata: u8, // Data payload - out output_axis_tlast: u1, // Last word in packet - - // AXI-Stream sub-ordinate input - in output_axis_tready: u1, // Downstream ready to accept -} - -// RESET: Assert reset (active-low) and wait for manager to be ready -// The manager waits C_M_START_COUNT cycles in INIT_COUNTER before sending -prot reset() { - DUT.rst := 1'b1; // Assert reset (active-high) - DUT.output_axis_tready := 1'b0; - step(); -} - -// RECV: Receive one data word from the AXI-Stream manager -// Data transfer occurs when output_axis_tvalid and output_axis_tready are both 1 -// Only matches when data is immediately available (output_axis_tvalid = 1) -// -// Output Arguments: -// data - Expected payload from manager -prot recv( - data: u8, -) { - DUT.rst := 1'b0; // Keep out of reset - DUT.output_axis_tready := 1'b1; // Signal ready to receive - - // Only matches when data is available - // (use wait_for_data for cycles when tready=1 but tvalid=0) - assert_eq(DUT.output_axis_tvalid, 1'b1); - - // Verify output data - assert_eq(DUT.output_axis_tdata, data); - - // Assert that this is *not* the last data word - assert_eq(DUT.output_axis_tlast, 1'b0); - - // One cycle for the transfer to complete - step(); -} - -// RECV_LAST: Receive the last data word (with output_axis_tlast asserted) -// This verifies both the data and that output_axis_tlast is properly set -// Only matches when data is immediately available (output_axis_tvalid = 1) -// -// Output Arguments: -// data - Expected payload from manager (should be the last word) -prot recv_last( - data: u8, -) { - DUT.rst := 1'b0; // Keep out of reset - DUT.output_axis_tready := 1'b1; // Signal ready to receive - - // Only matches when data is available - assert_eq(DUT.output_axis_tvalid, 1'b1); - - // Verify output data and output_axis_tlast - assert_eq(DUT.output_axis_tdata, data); - assert_eq(DUT.output_axis_tlast, 1'b1); - - // One cycle for the transfer to complete - step(); -} - -// STALL: Assert backpressure (output_axis_tready=0) while manager has valid data -// AXI-Stream requires output args (tdata, tlast) to remain stable during stall -// Only matches when the waveform contains output_axis_tvalid=1 (i.e. there is some valid data and it's available to stall) -prot stall(data: u8, last: u1) { - DUT.rst := 1'b0; // Keep out of reset - DUT.output_axis_tready := 1'b0; // Apply backpressure - - // Stall only applies when manager has valid data - // If output_axis_tvalid=0, this fails and we instead have an `idle` transaction - assert_eq(DUT.output_axis_tvalid, 1'b1); - - // Capture output values before the stall cycle - assert_eq(DUT.output_axis_tdata, data); - assert_eq(DUT.output_axis_tlast, last); - - step(); - - // Verify outputs remained stable during the stall - assert_eq(DUT.output_axis_tdata, data); - assert_eq(DUT.output_axis_tlast, last); - - step(); -} - -// WAIT_FOR_DATA: Receiver is ready but no data is available -// Used when tready=1 but tvalid=0 (i.e. receiver is polling for data) -prot wait_for_data() { - DUT.rst := 1'b0; // Keep out of reset - DUT.output_axis_tready := 1'b1; - - // Only matches when no data is available - assert_eq(DUT.output_axis_tvalid, 1'b0); - step(); -} - -// IDLE: No transaction - output_axis_tready is deasserted -#[idle] -prot idle() { - DUT.rst := 1'b0; // Keep out of reset - DUT.output_axis_tready := 1'b0; - step(); -} diff --git a/tests/fpga-debugging/axis-adapter-s3/s3_fixed.prot b/tests/fpga-debugging/axis-adapter-s3/s3_fixed.prot deleted file mode 100644 index 023e0f32..00000000 --- a/tests/fpga-debugging/axis-adapter-s3/s3_fixed.prot +++ /dev/null @@ -1,113 +0,0 @@ -// Source (manager) that outputs a sequence of 8 words -struct AXISManager { - // Control signals - in rst: u1, // Active-low reset - - // AXI-Stream manager outputs (from DUT perspective) - out output_axis_tvalid: u1, // manager has valid data - out output_axis_tdata: u8, // Data payload - out output_axis_tlast: u1, // Last word in packet - - // AXI-Stream sub-ordinate input - in output_axis_tready: u1, // Downstream ready to accept -} - -// RESET: Assert reset (active-low) and wait for manager to be ready -// The manager waits C_M_START_COUNT cycles in INIT_COUNTER before sending -prot reset() { - DUT.rst := 1'b1; // Assert reset (active-high) - DUT.output_axis_tready := 1'b0; - step(); -} - -// RECV: Receive one data word from the AXI-Stream manager -// Data transfer occurs when output_axis_tvalid and output_axis_tready are both 1 -// Only matches when data is immediately available (output_axis_tvalid = 1) -// -// Output Arguments: -// data - Expected payload from manager -prot recv( - data: u8, -) { - DUT.rst := 1'b0; // Keep out of reset - DUT.output_axis_tready := 1'b1; // Signal ready to receive - - // Only matches when data is available - // (use wait_for_data for cycles when tready=1 but tvalid=0) - assert_eq(DUT.output_axis_tvalid, 1'b1); - - // Verify output data - assert_eq(DUT.output_axis_tdata, data); - - // Assert that this is *not* the last data word - assert_eq(DUT.output_axis_tlast, 1'b0); - - // One cycle for the transfer to complete - step(); -} - -// RECV_LAST: Receive the last data word (with output_axis_tlast asserted) -// This verifies both the data and that output_axis_tlast is properly set -// Only matches when data is immediately available (output_axis_tvalid = 1) -// -// Output Arguments: -// data - Expected payload from manager (should be the last word) -prot recv_last( - data: u8, -) { - DUT.rst := 1'b0; // Keep out of reset - DUT.output_axis_tready := 1'b1; // Signal ready to receive - - // Only matches when data is available - assert_eq(DUT.output_axis_tvalid, 1'b1); - - // Verify output data and output_axis_tlast - assert_eq(DUT.output_axis_tdata, data); - assert_eq(DUT.output_axis_tlast, 1'b1); - - // One cycle for the transfer to complete - step(); -} - -// STALL: Assert backpressure (output_axis_tready=0) while manager has valid data -// AXI-Stream requires output args (tdata, tlast) to remain stable during stall -// Only matches when the waveform contains output_axis_tvalid=1 (i.e. there is some valid data and it's available to stall) -prot stall(data: u8, last: u1) { - DUT.rst := 1'b0; // Keep out of reset - DUT.output_axis_tready := 1'b0; // Apply backpressure - - // Stall only applies when manager has valid data - // If output_axis_tvalid=0, this fails and we instead have an `idle` transaction - assert_eq(DUT.output_axis_tvalid, 1'b1); - - // Capture output values before the stall cycle - assert_eq(DUT.output_axis_tdata, data); - assert_eq(DUT.output_axis_tlast, last); - - step(); - - // Verify outputs remained stable during the stall - assert_eq(DUT.output_axis_tdata, data); - assert_eq(DUT.output_axis_tlast, last); - - step(); -} - -// WAIT_FOR_DATA: Receiver is ready but no data is available -// Used when tready=1 but tvalid=0 (i.e. receiver is polling for data) -prot wait_for_data() { - DUT.rst := 1'b0; // Keep out of reset - DUT.output_axis_tready := 1'b1; - - // Only matches when no data is available - assert_eq(DUT.output_axis_tvalid, 1'b0); - step(); -} - -// IDLE: No transaction - output_axis_tready is deasserted -#[idle] -prot idle() { - DUT.rst := 1'b0; // Keep out of reset - DUT.output_axis_tready := 1'b0; - step(); -} From dbeeb1b2da3020ff2f5ee0a299b306f7074942f4 Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Mon, 24 Aug 2026 18:25:40 -0400 Subject: [PATCH 02/29] Update catalog of expect tests for Runt --- runt/bi/runt.toml | 12 ++++++------ scripts/test_catalog.py | 8 ++++---- 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/runt/bi/runt.toml b/runt/bi/runt.toml index b1be5db9..86c71516 100644 --- a/runt/bi/runt.toml +++ b/runt/bi/runt.toml @@ -2377,22 +2377,22 @@ expect_name = "s2_fixed.bi.expect" cmd = "cd ../.. && target/debug/bi --color never --protocol tests/fpga-debugging/axi-stream-s2/s2.prot --wave tests/fpga-debugging/axi-stream-s2/s2_fixed.fst --instances TOP.testbench.UUT:AXISManager --sample-posedge TOP.testbench.UUT.M_AXIS_ACLK --show-waveform-time --time-unit ns 2>&1" [[tests]] -name = "bi.tests_fpga_debugging_axis_adapter_s3_s3_buggy.s3_buggy_bi" +name = "bi.tests_fpga_debugging_axis_adapter_s3_s3.s3_buggy_bi" paths = [ - "../../tests/fpga-debugging/axis-adapter-s3/s3_buggy.prot", + "../../tests/fpga-debugging/axis-adapter-s3/s3.prot", ] expect_dir = "../../tests/fpga-debugging/axis-adapter-s3/expects" expect_name = "s3_buggy.bi.expect" -cmd = "cd ../.. && target/debug/bi --color never --protocol tests/fpga-debugging/axis-adapter-s3/s3_buggy.prot --wave tests/fpga-debugging/axis-adapter-s3/s3_buggy.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" +cmd = "cd ../.. && target/debug/bi --color never --protocol tests/fpga-debugging/axis-adapter-s3/s3.prot --wave tests/fpga-debugging/axis-adapter-s3/s3_buggy.fst --instances TOP.test_axis_adapter_64_8.UUT:AXIS --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_adapter_s3_s3_fixed.s3_fixed_bi" +name = "bi.tests_fpga_debugging_axis_adapter_s3_s3.s3_fixed_bi" paths = [ - "../../tests/fpga-debugging/axis-adapter-s3/s3_fixed.prot", + "../../tests/fpga-debugging/axis-adapter-s3/s3.prot", ] expect_dir = "../../tests/fpga-debugging/axis-adapter-s3/expects" 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" +cmd = "cd ../.. && target/debug/bi --color never --protocol tests/fpga-debugging/axis-adapter-s3/s3.prot --wave tests/fpga-debugging/axis-adapter-s3/s3_fixed.fst --instances TOP.test_axis_adapter_64_8.UUT:AXIS --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.c4_buggy_bi" diff --git a/scripts/test_catalog.py b/scripts/test_catalog.py index 3b7def3c..162605da 100644 --- a/scripts/test_catalog.py +++ b/scripts/test_catalog.py @@ -699,9 +699,9 @@ ), }, "tests.fpga-debugging.axis-adapter-s3.s3_buggy": { - "protocol": "tests/fpga-debugging/axis-adapter-s3/s3_buggy.prot", + "protocol": "tests/fpga-debugging/axis-adapter-s3/s3.prot", "wave": "tests/fpga-debugging/axis-adapter-s3/s3_buggy.fst", - "instances": ("TOP.test_axis_adapter_64_8.UUT:AXISManager",), + "instances": ("TOP.test_axis_adapter_64_8.UUT:AXIS",), "expect": "pass", "extra_args": ( "--sample-posedge", @@ -712,9 +712,9 @@ ), }, "tests.fpga-debugging.axis-adapter-s3.s3_fixed": { - "protocol": "tests/fpga-debugging/axis-adapter-s3/s3_fixed.prot", + "protocol": "tests/fpga-debugging/axis-adapter-s3/s3.prot", "wave": "tests/fpga-debugging/axis-adapter-s3/s3_fixed.fst", - "instances": ("TOP.test_axis_adapter_64_8.UUT:AXISManager",), + "instances": ("TOP.test_axis_adapter_64_8.UUT:AXIS",), "expect": "pass", "extra_args": ( "--sample-posedge", From f0558318dd5eeabfa3da9c696e46cb4aef90577f Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Mon, 24 Aug 2026 18:32:59 -0400 Subject: [PATCH 03/29] New version of s3 protocol --- tests/fpga-debugging/axis-adapter-s3/s3.prot | 113 +++++++++++++++++++ 1 file changed, 113 insertions(+) create mode 100644 tests/fpga-debugging/axis-adapter-s3/s3.prot diff --git a/tests/fpga-debugging/axis-adapter-s3/s3.prot b/tests/fpga-debugging/axis-adapter-s3/s3.prot new file mode 100644 index 00000000..ec8fc7f3 --- /dev/null +++ b/tests/fpga-debugging/axis-adapter-s3/s3.prot @@ -0,0 +1,113 @@ +// AXI-Stream width adapter which converts a 64-bit input into 8-bit outputs over multiple cycles +struct AXIS { + // Reset is active-high + in rst: u1, + + // Signals related to the DUT accepting input data from the environment + + // 64-bit data that the DUT accepts as input from the environment + in input_axis_tdata: u64, + + // bitmask indicating which bytes of `tdata` are meaningful + in input_axis_tkeep: u8, + + // 1 if this is the last word in a packet + in input_axis_tlast: u1, + + // Indicates if `input_tdata` contains valid data + in input_axis_tvalid: u1, + + // Signal indicating whether the DUT + // is ready to accept data from the environment as input + out input_axis_tready: u1, + + //---------------------------------------------------------------- + // Signals related to the DUT emitting data as output + + // 8-bit data that the DUT emits as output + out output_axis_tdata: u8, + + // Output data is 8 bits, so `tkeep` is now just 1 bit wide + // `tkeep` is 1 if `output_tdata` contains meaningful data + out output_axis_tkeep: u1, + + // 1 if this is the last word in a packet + out output_axis_tlast: u1, + + // Indicates if `output_data` contains valid data + out output_axis_tvalid: u1, + + // Signal indicating whether the environment is ready to + // accept the data emitted by the DUT as output + in output_axis_tready: u1, +} + +prot reset() { + DUT.rst := 1'b1; + + // Valid pin (for both directions) must be low when + // reset is asserted (AXI-Stream spec section 2.7.2) + DUT.input_axis_tvalid := 1'b0; + assert_eq(DUT.output_axis_tvalid, 1'b0); + + step(); +} + +// When idle, the DUT neither accepts data from the environment, +// nor does it emit data as output +#[idle] +prot idle() { + DUT.rst := 1'b0; + DUT.input_axis_tvalid := 1'b0; + + assert_eq(DUT.output_axis_tvalid, 1'b0); + step(); +} + + +// DUT accepts a 64-bit data payload from the environment +// The `keep` argument is a bitmask indicating which bytes of `data` contain +// meaningful data +prot accept_word(data: u64, keep: u8, last: u1) { + DUT.rst := 1'b0; + DUT.input_axis_tdata := data; + DUT.input_axis_tkeep := keep; + DUT.input_axis_tlast := last; + DUT.input_axis_tvalid := 1'b1; + + // Wait until the DUT signals that it has taken the word + while (!(DUT.input_axis_tready == 1'b1)) { + step(); + } + + step(); +} + +// DUT emits an 8-bit data payload (not the last byte of the packet) +prot emit_byte(data: u8) { + DUT.rst := 1'b0; + + assert_eq(DUT.output_axis_tvalid, 1'b1); + assert_eq(DUT.output_axis_tdata, data); + + // Set `tkeep` to 1 to indicate that the output data is meaningful + assert_eq(DUT.output_axis_tkeep, 1'b1); + + // Set `tlast` to 0 to indicate this isn't the last byte of the packet + assert_eq(DUT.output_axis_tlast, 1'b0); + + step(); +} + +// DUT emits the last byte of the packet +prot emit_last_byte(data: u8) { + DUT.rst := 1'b0; + + assert_eq(DUT.output_axis_tvalid, 1'b1); + assert_eq(DUT.output_axis_tdata, data); + assert_eq(DUT.output_axis_tkeep, 1'b1); + assert_eq(DUT.output_axis_tlast, 1'b1); + + step(); +} + From 06438c72f4001f3378a357931d7dee629b8ec67b Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Mon, 24 Aug 2026 18:33:13 -0400 Subject: [PATCH 04/29] Update Runt output --- .../expects/s3_buggy.bi.expect | 91 +++++++++++++++++-- .../expects/s3_fixed.bi.expect | 14 ++- 2 files changed, 88 insertions(+), 17 deletions(-) diff --git a/tests/fpga-debugging/axis-adapter-s3/expects/s3_buggy.bi.expect b/tests/fpga-debugging/axis-adapter-s3/expects/s3_buggy.bi.expect index 204d6b80..8ec894e5 100644 --- a/tests/fpga-debugging/axis-adapter-s3/expects/s3_buggy.bi.expect +++ b/tests/fpga-debugging/axis-adapter-s3/expects/s3_buggy.bi.expect @@ -1,13 +1,86 @@ // trace 0 trace { reset(); // [time: 0ns -> 25ns] - wait_for_data(); // [time: 25ns -> 50ns] - wait_for_data(); // [time: 50ns -> 75ns] - wait_for_data(); // [time: 75ns -> 100ns] - recv(205); // [time: 100ns -> 125ns] - recv(171); // [time: 125ns -> 150ns] - recv(205); // [time: 150ns -> 175ns] - recv(171); // [time: 175ns -> 200ns] - recv(205); // [time: 200ns -> 225ns] - recv_last(171); // [time: 225ns -> 225ns] + accept_word(12379739850550389709, 31, 1); // [time: 75ns -> 100ns] + emit_byte(205); // [time: 100ns -> 125ns] + emit_byte(171); // [time: 125ns -> 150ns] + emit_byte(205); // [time: 150ns -> 175ns] + emit_byte(171); // [time: 175ns -> 200ns] + emit_byte(205); // [time: 200ns -> 225ns] } +error: [emit_last_byte@9] executing step 0 of the transaction: 0 != 1 + ┌─ tests/fpga-debugging/axis-adapter-s3/s3.prot:108:5 + │ +108 │ assert_eq(DUT.output_axis_tkeep, 1'b1); + │ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ [emit_last_byte@9] executing step 0 of the transaction: 0 != 1 + + +// trace 1 +trace { + reset(); // [time: 0ns -> 25ns] + accept_word(12379739850550389709, 31, 1); // [time: 75ns -> 100ns] + emit_byte(205); // [time: 100ns -> 125ns] + emit_byte(171); // [time: 125ns -> 150ns] + emit_byte(205); // [time: 150ns -> 175ns] + emit_byte(171); // [time: 175ns -> 200ns] + emit_byte(205); // [time: 200ns -> 225ns] +} +error: [emit_byte@9] executing step 0 of the transaction: 0 != 1 + ┌─ tests/fpga-debugging/axis-adapter-s3/s3.prot:94:5 + │ +94 │ assert_eq(DUT.output_axis_tkeep, 1'b1); + │ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ [emit_byte@9] executing step 0 of the transaction: 0 != 1 + + +// trace 2 +trace { + reset(); // [time: 0ns -> 25ns] + accept_word(12379739850550389709, 31, 1); // [time: 75ns -> 100ns] + emit_byte(205); // [time: 100ns -> 125ns] + emit_byte(171); // [time: 125ns -> 150ns] + emit_byte(205); // [time: 150ns -> 175ns] + emit_byte(171); // [time: 175ns -> 200ns] + emit_byte(205); // [time: 200ns -> 225ns] +} +error: [accept_word@9] executing step 0 of the transaction: 0 != 1 + ┌─ tests/fpga-debugging/axis-adapter-s3/s3.prot:76:5 + │ +76 │ DUT.input_axis_tvalid := 1'b1; + │ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ [accept_word@9] executing step 0 of the transaction: 0 != 1 + + +// trace 3 +trace { + reset(); // [time: 0ns -> 25ns] + accept_word(12379739850550389709, 31, 1); // [time: 75ns -> 100ns] + emit_byte(205); // [time: 100ns -> 125ns] + emit_byte(171); // [time: 125ns -> 150ns] + emit_byte(205); // [time: 150ns -> 175ns] + emit_byte(171); // [time: 175ns -> 200ns] + emit_byte(205); // [time: 200ns -> 225ns] +} +error: [idle@9] executing step 0 of the transaction: 1 != 0 + ┌─ tests/fpga-debugging/axis-adapter-s3/s3.prot:63:5 + │ +63 │ assert_eq(DUT.output_axis_tvalid, 1'b0); + │ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ [idle@9] executing step 0 of the transaction: 1 != 0 + + +// trace 4 +trace { + reset(); // [time: 0ns -> 25ns] + accept_word(12379739850550389709, 31, 1); // [time: 75ns -> 100ns] + emit_byte(205); // [time: 100ns -> 125ns] + emit_byte(171); // [time: 125ns -> 150ns] + emit_byte(205); // [time: 150ns -> 175ns] + emit_byte(171); // [time: 175ns -> 200ns] + emit_byte(205); // [time: 200ns -> 225ns] +} +error: [reset@9] executing step 0 of the transaction: 1 != 0 + ┌─ tests/fpga-debugging/axis-adapter-s3/s3.prot:51:5 + │ +51 │ assert_eq(DUT.output_axis_tvalid, 1'b0); + │ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ [reset@9] executing step 0 of the transaction: 1 != 0 + +---CODE--- +1 diff --git a/tests/fpga-debugging/axis-adapter-s3/expects/s3_fixed.bi.expect b/tests/fpga-debugging/axis-adapter-s3/expects/s3_fixed.bi.expect index 5cbf6070..2c38ca6b 100644 --- a/tests/fpga-debugging/axis-adapter-s3/expects/s3_fixed.bi.expect +++ b/tests/fpga-debugging/axis-adapter-s3/expects/s3_fixed.bi.expect @@ -1,12 +1,10 @@ // trace 0 trace { reset(); // [time: 0ns -> 25ns] - wait_for_data(); // [time: 25ns -> 50ns] - wait_for_data(); // [time: 50ns -> 75ns] - wait_for_data(); // [time: 75ns -> 100ns] - recv(205); // [time: 100ns -> 125ns] - recv(171); // [time: 125ns -> 150ns] - recv(205); // [time: 150ns -> 175ns] - recv(171); // [time: 175ns -> 200ns] - recv_last(205); // [time: 200ns -> 200ns] + accept_word(12379739850550389709, 31, 1); // [time: 75ns -> 100ns] + emit_byte(205); // [time: 100ns -> 125ns] + emit_byte(171); // [time: 125ns -> 150ns] + emit_byte(205); // [time: 150ns -> 175ns] + emit_byte(171); // [time: 175ns -> 200ns] + emit_last_byte(205); // [time: 200ns -> 200ns] } From 9f2981018a671669e160ccb1f8a9d45dd58c7793 Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Mon, 24 Aug 2026 18:49:39 -0400 Subject: [PATCH 05/29] Add comment --- .../fpga-debugging/axis-adapter-s3/expects/s3_buggy.bi.expect | 4 ++-- tests/fpga-debugging/axis-adapter-s3/s3.prot | 4 +++- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/tests/fpga-debugging/axis-adapter-s3/expects/s3_buggy.bi.expect b/tests/fpga-debugging/axis-adapter-s3/expects/s3_buggy.bi.expect index 8ec894e5..eac18daf 100644 --- a/tests/fpga-debugging/axis-adapter-s3/expects/s3_buggy.bi.expect +++ b/tests/fpga-debugging/axis-adapter-s3/expects/s3_buggy.bi.expect @@ -9,9 +9,9 @@ trace { emit_byte(205); // [time: 200ns -> 225ns] } error: [emit_last_byte@9] executing step 0 of the transaction: 0 != 1 - ┌─ tests/fpga-debugging/axis-adapter-s3/s3.prot:108:5 + ┌─ tests/fpga-debugging/axis-adapter-s3/s3.prot:110:5 │ -108 │ assert_eq(DUT.output_axis_tkeep, 1'b1); +110 │ assert_eq(DUT.output_axis_tkeep, 1'b1); │ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ [emit_last_byte@9] executing step 0 of the transaction: 0 != 1 diff --git a/tests/fpga-debugging/axis-adapter-s3/s3.prot b/tests/fpga-debugging/axis-adapter-s3/s3.prot index ec8fc7f3..548fdc8a 100644 --- a/tests/fpga-debugging/axis-adapter-s3/s3.prot +++ b/tests/fpga-debugging/axis-adapter-s3/s3.prot @@ -99,7 +99,9 @@ prot emit_byte(data: u8) { step(); } -// DUT emits the last byte of the packet +// DUT emits the last byte of the packet. +// Note that this protocol is the same as `emit_byte`, +// except we assert that `tlast = 1` prot emit_last_byte(data: u8) { DUT.rst := 1'b0; From e5adee92c34602d6958e659e78a545ccd28e6f87 Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Tue, 25 Aug 2026 15:57:01 -0400 Subject: [PATCH 06/29] Attempt at rewriting --- runt/bi/runt.toml | 4 +- scripts/test_catalog.py | 5 + .../expects/s3_buggy.bi.expect | 85 ++----- .../expects/s3_fixed.bi.expect | 9 +- tests/fpga-debugging/axis-adapter-s3/s3.prot | 180 ++++++++++++--- .../axis-adapter-s3/s3_new.prot | 210 ++++++++++++++++++ 6 files changed, 377 insertions(+), 116 deletions(-) create mode 100644 tests/fpga-debugging/axis-adapter-s3/s3_new.prot diff --git a/runt/bi/runt.toml b/runt/bi/runt.toml index 86c71516..7a042c65 100644 --- a/runt/bi/runt.toml +++ b/runt/bi/runt.toml @@ -2383,7 +2383,7 @@ paths = [ ] expect_dir = "../../tests/fpga-debugging/axis-adapter-s3/expects" expect_name = "s3_buggy.bi.expect" -cmd = "cd ../.. && target/debug/bi --color never --protocol tests/fpga-debugging/axis-adapter-s3/s3.prot --wave tests/fpga-debugging/axis-adapter-s3/s3_buggy.fst --instances TOP.test_axis_adapter_64_8.UUT:AXIS --sample-posedge TOP.test_axis_adapter_64_8.UUT.clk --show-waveform-time --time-unit ns 2>&1" +cmd = "cd ../.. && target/debug/bi --color never --protocol tests/fpga-debugging/axis-adapter-s3/s3.prot --wave tests/fpga-debugging/axis-adapter-s3/s3_buggy.fst --instances TOP.test_axis_adapter_64_8.UUT:AXIS --sample-posedge TOP.test_axis_adapter_64_8.UUT.clk --show-waveform-time --include-idle --time-unit ns --display-hex 2>&1" [[tests]] name = "bi.tests_fpga_debugging_axis_adapter_s3_s3.s3_fixed_bi" @@ -2392,7 +2392,7 @@ paths = [ ] expect_dir = "../../tests/fpga-debugging/axis-adapter-s3/expects" expect_name = "s3_fixed.bi.expect" -cmd = "cd ../.. && target/debug/bi --color never --protocol tests/fpga-debugging/axis-adapter-s3/s3.prot --wave tests/fpga-debugging/axis-adapter-s3/s3_fixed.fst --instances TOP.test_axis_adapter_64_8.UUT:AXIS --sample-posedge TOP.test_axis_adapter_64_8.UUT.clk --show-waveform-time --time-unit ns 2>&1" +cmd = "cd ../.. && target/debug/bi --color never --protocol tests/fpga-debugging/axis-adapter-s3/s3.prot --wave tests/fpga-debugging/axis-adapter-s3/s3_fixed.fst --instances TOP.test_axis_adapter_64_8.UUT:AXIS --sample-posedge TOP.test_axis_adapter_64_8.UUT.clk --show-waveform-time --include-idle --time-unit ns --include-in-progress --display-hex 2>&1" [[tests]] name = "bi.tests_fpga_debugging_axis_async_fifo_c4_c4.c4_buggy_bi" diff --git a/scripts/test_catalog.py b/scripts/test_catalog.py index 162605da..cb2b00dc 100644 --- a/scripts/test_catalog.py +++ b/scripts/test_catalog.py @@ -707,8 +707,10 @@ "--sample-posedge", "TOP.test_axis_adapter_64_8.UUT.clk", "--show-waveform-time", + "--include-idle", "--time-unit", "ns", + "--display-hex" ), }, "tests.fpga-debugging.axis-adapter-s3.s3_fixed": { @@ -720,8 +722,11 @@ "--sample-posedge", "TOP.test_axis_adapter_64_8.UUT.clk", "--show-waveform-time", + "--include-idle", "--time-unit", "ns", + "--include-in-progress", + "--display-hex" ), }, "tests.fpga-debugging.axis-async-fifo-c4.c4_buggy": { diff --git a/tests/fpga-debugging/axis-adapter-s3/expects/s3_buggy.bi.expect b/tests/fpga-debugging/axis-adapter-s3/expects/s3_buggy.bi.expect index eac18daf..ebf4e835 100644 --- a/tests/fpga-debugging/axis-adapter-s3/expects/s3_buggy.bi.expect +++ b/tests/fpga-debugging/axis-adapter-s3/expects/s3_buggy.bi.expect @@ -1,86 +1,27 @@ // trace 0 trace { reset(); // [time: 0ns -> 25ns] - accept_word(12379739850550389709, 31, 1); // [time: 75ns -> 100ns] - emit_byte(205); // [time: 100ns -> 125ns] - emit_byte(171); // [time: 125ns -> 150ns] - emit_byte(205); // [time: 150ns -> 175ns] - emit_byte(171); // [time: 175ns -> 200ns] - emit_byte(205); // [time: 200ns -> 225ns] + idle(); // [time: 25ns -> 50ns] + idle(); // [time: 50ns -> 75ns] } -error: [emit_last_byte@9] executing step 0 of the transaction: 0 != 1 - ┌─ tests/fpga-debugging/axis-adapter-s3/s3.prot:110:5 +error: [split_word@3] executing step 5 of the transaction: 0 != 1 + ┌─ tests/fpga-debugging/axis-adapter-s3/s3.prot:169:33 │ -110 │ assert_eq(DUT.output_axis_tkeep, 1'b1); - │ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ [emit_last_byte@9] executing step 0 of the transaction: 0 != 1 +169 │ assert_eq(keep[5], 1'b1); + │ ^^^^^^^^^^^^^^^^^^^^^^^^^ [split_word@3] executing step 5 of the transaction: 0 != 1 // trace 1 trace { reset(); // [time: 0ns -> 25ns] - accept_word(12379739850550389709, 31, 1); // [time: 75ns -> 100ns] - emit_byte(205); // [time: 100ns -> 125ns] - emit_byte(171); // [time: 125ns -> 150ns] - emit_byte(205); // [time: 150ns -> 175ns] - emit_byte(171); // [time: 175ns -> 200ns] - emit_byte(205); // [time: 200ns -> 225ns] + idle(); // [time: 25ns -> 50ns] + idle(); // [time: 50ns -> 75ns] } -error: [emit_byte@9] executing step 0 of the transaction: 0 != 1 - ┌─ tests/fpga-debugging/axis-adapter-s3/s3.prot:94:5 - │ -94 │ assert_eq(DUT.output_axis_tkeep, 1'b1); - │ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ [emit_byte@9] executing step 0 of the transaction: 0 != 1 - - -// trace 2 -trace { - reset(); // [time: 0ns -> 25ns] - accept_word(12379739850550389709, 31, 1); // [time: 75ns -> 100ns] - emit_byte(205); // [time: 100ns -> 125ns] - emit_byte(171); // [time: 125ns -> 150ns] - emit_byte(205); // [time: 150ns -> 175ns] - emit_byte(171); // [time: 175ns -> 200ns] - emit_byte(205); // [time: 200ns -> 225ns] -} -error: [accept_word@9] executing step 0 of the transaction: 0 != 1 - ┌─ tests/fpga-debugging/axis-adapter-s3/s3.prot:76:5 - │ -76 │ DUT.input_axis_tvalid := 1'b1; - │ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ [accept_word@9] executing step 0 of the transaction: 0 != 1 - - -// trace 3 -trace { - reset(); // [time: 0ns -> 25ns] - accept_word(12379739850550389709, 31, 1); // [time: 75ns -> 100ns] - emit_byte(205); // [time: 100ns -> 125ns] - emit_byte(171); // [time: 125ns -> 150ns] - emit_byte(205); // [time: 150ns -> 175ns] - emit_byte(171); // [time: 175ns -> 200ns] - emit_byte(205); // [time: 200ns -> 225ns] -} -error: [idle@9] executing step 0 of the transaction: 1 != 0 - ┌─ tests/fpga-debugging/axis-adapter-s3/s3.prot:63:5 - │ -63 │ assert_eq(DUT.output_axis_tvalid, 1'b0); - │ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ [idle@9] executing step 0 of the transaction: 1 != 0 - - -// trace 4 -trace { - reset(); // [time: 0ns -> 25ns] - accept_word(12379739850550389709, 31, 1); // [time: 75ns -> 100ns] - emit_byte(205); // [time: 100ns -> 125ns] - emit_byte(171); // [time: 125ns -> 150ns] - emit_byte(205); // [time: 150ns -> 175ns] - emit_byte(171); // [time: 175ns -> 200ns] - emit_byte(205); // [time: 200ns -> 225ns] -} -error: [reset@9] executing step 0 of the transaction: 1 != 0 - ┌─ tests/fpga-debugging/axis-adapter-s3/s3.prot:51:5 - │ -51 │ assert_eq(DUT.output_axis_tvalid, 1'b0); - │ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ [reset@9] executing step 0 of the transaction: 1 != 0 +error: [split_word@3L] executing step 5 of the transaction: 0 != 1 + ┌─ tests/fpga-debugging/axis-adapter-s3/s3.prot:163:33 + │ +163 │ assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); + │ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ [split_word@3L] executing step 5 of the transaction: 0 != 1 ---CODE--- 1 diff --git a/tests/fpga-debugging/axis-adapter-s3/expects/s3_fixed.bi.expect b/tests/fpga-debugging/axis-adapter-s3/expects/s3_fixed.bi.expect index 2c38ca6b..94fd93a2 100644 --- a/tests/fpga-debugging/axis-adapter-s3/expects/s3_fixed.bi.expect +++ b/tests/fpga-debugging/axis-adapter-s3/expects/s3_fixed.bi.expect @@ -1,10 +1,7 @@ // trace 0 trace { reset(); // [time: 0ns -> 25ns] - accept_word(12379739850550389709, 31, 1); // [time: 75ns -> 100ns] - emit_byte(205); // [time: 100ns -> 125ns] - emit_byte(171); // [time: 125ns -> 150ns] - emit_byte(205); // [time: 150ns -> 175ns] - emit_byte(171); // [time: 175ns -> 200ns] - emit_last_byte(205); // [time: 200ns -> 200ns] + idle(); // [time: 25ns -> 50ns] + idle(); // [time: 50ns -> 75ns] + split_word(0xabcdabcdabcdabcd, 0x1f, 0x1, 0x[cd, ab, cd, ab, cd]); // [time: 75ns -> ] } diff --git a/tests/fpga-debugging/axis-adapter-s3/s3.prot b/tests/fpga-debugging/axis-adapter-s3/s3.prot index 548fdc8a..80ebd5e7 100644 --- a/tests/fpga-debugging/axis-adapter-s3/s3.prot +++ b/tests/fpga-debugging/axis-adapter-s3/s3.prot @@ -1,4 +1,22 @@ // AXI-Stream width adapter which converts a 64-bit input into 8-bit outputs over multiple cycles + +// Notes: +// - The DUT has 3 termination conditions +// - 1. All the bytes corresponding to the rightmost contiguous sequence of 1s in `tkeep` are emitted, +// e.g. tkeep = 11111111 (all bytes of `tdata` are meaningful) +// or tkeep = 00011111 (the 5 least significant bytes of `tdata` are meaningful) +// - 2. When emitting the i-th byte, the DUT sees that tkeep[i] = 0, in which case it treats the i-th byte as the last one and stops emitting any further bytes +// - 3. For the fixed DUT only, it truncates the output after `i` bytes if it detects that `input_tkeep[i + 1] = 0` +// - The DUT cannot accept a new 64-bit input when it is still emitting the bytes of the existing data +// - The DUT examines `tkeep` from right to left, i.e. the 0th byte emitted +// corresponds to `tdata[7:0]` and `tkeep[0]` (the LSB of `tkeep`) +// - The fixed waveform has `tkeep = 0001 1111`, so only 5 bytes are emitted and the +// waveform ends after the 5 bytes are emitted +// - The `output_bytes` parameter to the `send_word` protocol below contains +// the bytes in the order they're emitted, and since the DUT examines `tdata` right to left, +// this means if `tdata = 0xABCD`, the output bytes are `[0xCD, 0xAB]` +// (i.e. the bytes corresponding to less significant bits are emitted first) + struct AXIS { // Reset is active-high in rst: u1, @@ -64,52 +82,142 @@ prot idle() { step(); } - -// DUT accepts a 64-bit data payload from the environment -// The `keep` argument is a bitmask indicating which bytes of `data` contain -// meaningful data -prot accept_word(data: u64, keep: u8, last: u1) { +prot split_word(data: u64, keep: u8, is_final_word_in_packet: u1, output_bytes: [u8]+) { DUT.rst := 1'b0; DUT.input_axis_tdata := data; DUT.input_axis_tkeep := keep; - DUT.input_axis_tlast := last; + DUT.input_axis_tlast := is_final_word_in_packet; DUT.input_axis_tvalid := 1'b1; // Wait until the DUT signals that it has taken the word while (!(DUT.input_axis_tready == 1'b1)) { step(); } - - step(); -} - -// DUT emits an 8-bit data payload (not the last byte of the packet) -prot emit_byte(data: u8) { - DUT.rst := 1'b0; - - assert_eq(DUT.output_axis_tvalid, 1'b1); - assert_eq(DUT.output_axis_tdata, data); - - // Set `tkeep` to 1 to indicate that the output data is meaningful - assert_eq(DUT.output_axis_tkeep, 1'b1); - - // Set `tlast` to 0 to indicate this isn't the last byte of the packet - assert_eq(DUT.output_axis_tlast, 1'b0); - + // One cycle for DUT to accept input data from environment step(); -} -// DUT emits the last byte of the packet. -// Note that this protocol is the same as `emit_byte`, -// except we assert that `tlast = 1` -prot emit_last_byte(data: u8) { - DUT.rst := 1'b0; - - assert_eq(DUT.output_axis_tvalid, 1'b1); - assert_eq(DUT.output_axis_tdata, data); - assert_eq(DUT.output_axis_tkeep, 1'b1); - assert_eq(DUT.output_axis_tlast, 1'b1); + // DUT has accepted input data, so we set the input pins to DOntCare + DUT.input_axis_tdata := X; + DUT.input_axis_tkeep := X; + DUT.input_axis_tlast := X; + + // Since input pins are DontCare, we also set `input_tvalid` to DontCare + DUT.input_axis_tvalid := X; + + // DUT is ready to emit output data + DUT.output_axis_tready := 1'b1; + + // TODO: double check this + + for byte in output_bytes { + while (!(DUT.output_axis_tvalid == 1'b1)) { + step(); + } + + assert_eq(DUT.output_axis_tdata, byte); + + if iter_count::() == 3'd0 { + // For the `i`-th output byte, the output `tkeep` bit is `keep[i]` + assert_eq(DUT.output_axis_tkeep, keep[0]); + if is_last() { + assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); + // Current byte is the last one, so the next byte is not kept + assert_eq(keep[1], 1'b0); + } else { + assert_eq(DUT.output_axis_tlast, 1'b0); + + // Current byte is not the last one, so the next byte is kept + assert_eq(keep[1], 1'b1); + } + } else { + if iter_count::() == 3'd1 { + assert_eq(DUT.output_axis_tkeep, keep[1]); + if is_last() { + assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); + // The current byte is the last one, so the next byte is not kept + assert_eq(keep[2], 1'b0); + } else { + assert_eq(DUT.output_axis_tlast, 1'b0); + // The current byte is not the last one, so the next byte is kept + assert_eq(keep[2], 1'b1); + } + } else { + if iter_count::() == 3'd2 { + assert_eq(DUT.output_axis_tkeep, keep[2]); + if is_last() { + assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); + // The current byte is the last one, so the next byte is not kept + assert_eq(keep[3], 1'b0); + } else { + assert_eq(DUT.output_axis_tlast, 1'b0); + // The current byte is not the last one, so the next byte is kept + assert_eq(keep[3], 1'b1); + } + } else { + if iter_count::() == 3'd3 { + assert_eq(DUT.output_axis_tkeep, keep[3]); + if is_last() { + assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); + // The current byte is the last one, so the next byte is not kept + assert_eq(keep[4], 1'b0); + } else { + assert_eq(DUT.output_axis_tlast, 1'b0); + // The current byte is not the last one, so the next byte is kept + assert_eq(keep[4], 1'b1); + } + } else { + if iter_count::() == 3'd4 { + assert_eq(DUT.output_axis_tkeep, keep[4]); + if is_last() { + assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); + // The current byte is the last one, so the next byte is not kept + assert_eq(keep[5], 1'b0); + } else { + assert_eq(DUT.output_axis_tlast, 1'b0); + // The current byte is not the last one, so the next byte is kept + assert_eq(keep[5], 1'b1); + } + } else { + if iter_count::() == 3'd5 { + assert_eq(DUT.output_axis_tkeep, keep[5]); + if is_last() { + assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); + // The current byte is the last one, so the next byte is not kept + assert_eq(keep[6], 1'b0); + } else { + assert_eq(DUT.output_axis_tlast, 1'b0); + // The current byte is not the last one, so the next byte is kept + assert_eq(keep[6], 1'b1); + } + } else { + if iter_count::() == 3'd6 { + assert_eq(DUT.output_axis_tkeep, keep[6]); + if is_last() { + assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); + // The current byte is the last one, so the next byte is not kept + assert_eq(keep[7], 1'b0); + } else { + assert_eq(DUT.output_axis_tlast, 1'b0); + // The current byte is not the last one, so the next byte is kept + assert_eq(keep[7], 1'b1); + } + } else { + // Last iteration (can't have more than 8 bytes in a 64-bit output) + assert_eq(DUT.output_axis_tkeep, keep[7]); + + if is_last() { + assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); + } else { + assert_eq(DUT.output_axis_tlast, 1'b0); + } + } + } + } + } + } + } + } - step(); + step(); + } } - diff --git a/tests/fpga-debugging/axis-adapter-s3/s3_new.prot b/tests/fpga-debugging/axis-adapter-s3/s3_new.prot new file mode 100644 index 00000000..56fe5400 --- /dev/null +++ b/tests/fpga-debugging/axis-adapter-s3/s3_new.prot @@ -0,0 +1,210 @@ +// AXI-Stream width adapter which converts a 64-bit input into 8-bit outputs over multiple cycles + +// Notes: +// - the fixed DUT truncates the output after `i` bytes +// if it detects that `input_tkeep[i + 1] = 0`. +// - The DUT cannot accept a new 64-bit input when it is still emitting the bytes of the existing data +// - There is no reordering in the DUT + + +struct AXIS { + // Reset is active-high + in rst: u1, + + // Signals related to the DUT accepting input data from the environment + + // 64-bit data that the DUT accepts as input from the environment + in input_axis_tdata: u64, + + // bitmask indicating which bytes of `tdata` are meaningful + in input_axis_tkeep: u8, + + // 1 if this is the last word in a packet + in input_axis_tlast: u1, + + // Indicates if `input_tdata` contains valid data + in input_axis_tvalid: u1, + + // Signal indicating whether the DUT + // is ready to accept data from the environment as input + out input_axis_tready: u1, + + //---------------------------------------------------------------- + // Signals related to the DUT emitting data as output + + // 8-bit data that the DUT emits as output + out output_axis_tdata: u8, + + // Output data is 8 bits, so `tkeep` is now just 1 bit wide + // `tkeep` is 1 if `output_tdata` contains meaningful data + out output_axis_tkeep: u1, + + // 1 if this is the last word in a packet + out output_axis_tlast: u1, + + // Indicates if `output_data` contains valid data + out output_axis_tvalid: u1, + + // Signal indicating whether the environment is ready to + // accept the data emitted by the DUT as output + in output_axis_tready: u1, +} + +prot reset() { + DUT.rst := 1'b1; + + // Valid pin (for both directions) must be low when + // reset is asserted (AXI-Stream spec section 2.7.2) + DUT.input_axis_tvalid := 1'b0; + assert_eq(DUT.output_axis_tvalid, 1'b0); + + step(); +} + +// When idle, the DUT neither accepts data from the environment, +// nor does it emit data as output +#[idle] +prot idle() { + DUT.rst := 1'b0; + DUT.input_axis_tvalid := 1'b0; + + assert_eq(DUT.output_axis_tvalid, 1'b0); + step(); +} + +prot split_word(data: u64, keep: u8, is_final_word_in_packet: u1, output_bytes: [u8]+) { + DUT.rst := 1'b0; + DUT.input_axis_tdata := data; + DUT.input_axis_tkeep := keep; + DUT.input_axis_tlast := is_final_word_in_packet; + DUT.input_axis_tvalid := 1'b1; + + // Wait until the DUT signals that it has taken the word + while (!(DUT.input_axis_tready == 1'b1)) { + step(); + } + // One cycle for DUT to accept input data from environment + step(); + + // DUT has accepted input data, so we set the input pins to DOntCare + DUT.input_axis_tdata := X; + DUT.input_axis_tkeep := X; + DUT.input_axis_tlast := X; + + // DUT is ready to emit output data + DUT.output_axis_tready := 1'b1; + + // TODO: double check this + + for byte in output_bytes { + while (!(DUT.output_axis_tvalid == 1'b1)) { + step(); + } + + assert_eq(DUT.output_axis_tdata, byte); + + if iter_count::() == 3'd0 { + // For the `i`-th output byte, the output `tkeep` bit is `keep[i]` + assert_eq(DUT.output_axis_tkeep, keep[0]); + if is_last() { + assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); + // Current byte is the last one, so the next byte is not kept + assert_eq(keep[1], 1'b0); + } else { + assert_eq(DUT.output_axis_tlast, 1'b0); + + // Current byte is not the last one, so the next byte is kept + assert_eq(keep[1], 1'b1); + } + } else { + if iter_count::() == 3'd1 { + assert_eq(DUT.output_axis_tkeep, keep[1]); + if is_last() { + assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); + // The current byte is the last one, so the next byte is not kept + assert_eq(keep[2], 1'b0); + } else { + assert_eq(DUT.output_axis_tlast, 1'b0); + // The current byte is not the last one, so the next byte is kept + assert_eq(keep[2], 1'b1); + } + } else { + if iter_count::() == 3'd2 { + assert_eq(DUT.output_axis_tkeep, keep[2]); + if is_last() { + assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); + // The current byte is the last one, so the next byte is not kept + assert_eq(keep[3], 1'b0); + } else { + assert_eq(DUT.output_axis_tlast, 1'b0); + // The current byte is not the last one, so the next byte is kept + assert_eq(keep[3], 1'b1); + } + } else { + if iter_count::() == 3'd3 { + assert_eq(DUT.output_axis_tkeep, keep[3]); + if is_last() { + assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); + // The current byte is the last one, so the next byte is not kept + assert_eq(keep[4], 1'b0); + } else { + assert_eq(DUT.output_axis_tlast, 1'b0); + // The current byte is not the last one, so the next byte is kept + assert_eq(keep[4], 1'b1); + } + } else { + if iter_count::() == 3'd4 { + assert_eq(DUT.output_axis_tkeep, keep[4]); + if is_last() { + assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); + // The current byte is the last one, so the next byte is not kept + assert_eq(keep[5], 1'b0); + } else { + assert_eq(DUT.output_axis_tlast, 1'b0); + // The current byte is not the last one, so the next byte is kept + assert_eq(keep[5], 1'b1); + } + } else { + if iter_count::() == 3'd5 { + assert_eq(DUT.output_axis_tkeep, keep[5]); + if is_last() { + assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); + // The current byte is the last one, so the next byte is not kept + assert_eq(keep[6], 1'b0); + } else { + assert_eq(DUT.output_axis_tlast, 1'b0); + // The current byte is not the last one, so the next byte is kept + assert_eq(keep[6], 1'b1); + } + } else { + if iter_count::() == 3'd6 { + assert_eq(DUT.output_axis_tkeep, keep[6]); + if is_last() { + assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); + // The current byte is the last one, so the next byte is not kept + assert_eq(keep[7], 1'b0); + } else { + assert_eq(DUT.output_axis_tlast, 1'b0); + // The current byte is not the last one, so the next byte is kept + assert_eq(keep[7], 1'b1); + } + } else { + // Last iteration (can't have more than 8 bytes in a 64-bit output) + assert_eq(DUT.output_axis_tkeep, keep[7]); + + if is_last() { + assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); + } else { + assert_eq(DUT.output_axis_tlast, 1'b0); + } + } + } + } + } + } + } + } + + step(); + } +} From 1d17b654cd6244bb4bb612abd5fe7d91fc84f308 Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Tue, 25 Aug 2026 15:57:35 -0400 Subject: [PATCH 07/29] python formatting --- scripts/test_catalog.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/test_catalog.py b/scripts/test_catalog.py index cb2b00dc..3facbdce 100644 --- a/scripts/test_catalog.py +++ b/scripts/test_catalog.py @@ -710,7 +710,7 @@ "--include-idle", "--time-unit", "ns", - "--display-hex" + "--display-hex", ), }, "tests.fpga-debugging.axis-adapter-s3.s3_fixed": { @@ -726,7 +726,7 @@ "--time-unit", "ns", "--include-in-progress", - "--display-hex" + "--display-hex", ), }, "tests.fpga-debugging.axis-async-fifo-c4.c4_buggy": { From 2e3e1443119f07896183591e13db5bc2ea6343e2 Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Tue, 25 Aug 2026 15:58:27 -0400 Subject: [PATCH 08/29] rm duplicate .prot file --- .../axis-adapter-s3/s3_new.prot | 210 ------------------ 1 file changed, 210 deletions(-) delete mode 100644 tests/fpga-debugging/axis-adapter-s3/s3_new.prot diff --git a/tests/fpga-debugging/axis-adapter-s3/s3_new.prot b/tests/fpga-debugging/axis-adapter-s3/s3_new.prot deleted file mode 100644 index 56fe5400..00000000 --- a/tests/fpga-debugging/axis-adapter-s3/s3_new.prot +++ /dev/null @@ -1,210 +0,0 @@ -// AXI-Stream width adapter which converts a 64-bit input into 8-bit outputs over multiple cycles - -// Notes: -// - the fixed DUT truncates the output after `i` bytes -// if it detects that `input_tkeep[i + 1] = 0`. -// - The DUT cannot accept a new 64-bit input when it is still emitting the bytes of the existing data -// - There is no reordering in the DUT - - -struct AXIS { - // Reset is active-high - in rst: u1, - - // Signals related to the DUT accepting input data from the environment - - // 64-bit data that the DUT accepts as input from the environment - in input_axis_tdata: u64, - - // bitmask indicating which bytes of `tdata` are meaningful - in input_axis_tkeep: u8, - - // 1 if this is the last word in a packet - in input_axis_tlast: u1, - - // Indicates if `input_tdata` contains valid data - in input_axis_tvalid: u1, - - // Signal indicating whether the DUT - // is ready to accept data from the environment as input - out input_axis_tready: u1, - - //---------------------------------------------------------------- - // Signals related to the DUT emitting data as output - - // 8-bit data that the DUT emits as output - out output_axis_tdata: u8, - - // Output data is 8 bits, so `tkeep` is now just 1 bit wide - // `tkeep` is 1 if `output_tdata` contains meaningful data - out output_axis_tkeep: u1, - - // 1 if this is the last word in a packet - out output_axis_tlast: u1, - - // Indicates if `output_data` contains valid data - out output_axis_tvalid: u1, - - // Signal indicating whether the environment is ready to - // accept the data emitted by the DUT as output - in output_axis_tready: u1, -} - -prot reset() { - DUT.rst := 1'b1; - - // Valid pin (for both directions) must be low when - // reset is asserted (AXI-Stream spec section 2.7.2) - DUT.input_axis_tvalid := 1'b0; - assert_eq(DUT.output_axis_tvalid, 1'b0); - - step(); -} - -// When idle, the DUT neither accepts data from the environment, -// nor does it emit data as output -#[idle] -prot idle() { - DUT.rst := 1'b0; - DUT.input_axis_tvalid := 1'b0; - - assert_eq(DUT.output_axis_tvalid, 1'b0); - step(); -} - -prot split_word(data: u64, keep: u8, is_final_word_in_packet: u1, output_bytes: [u8]+) { - DUT.rst := 1'b0; - DUT.input_axis_tdata := data; - DUT.input_axis_tkeep := keep; - DUT.input_axis_tlast := is_final_word_in_packet; - DUT.input_axis_tvalid := 1'b1; - - // Wait until the DUT signals that it has taken the word - while (!(DUT.input_axis_tready == 1'b1)) { - step(); - } - // One cycle for DUT to accept input data from environment - step(); - - // DUT has accepted input data, so we set the input pins to DOntCare - DUT.input_axis_tdata := X; - DUT.input_axis_tkeep := X; - DUT.input_axis_tlast := X; - - // DUT is ready to emit output data - DUT.output_axis_tready := 1'b1; - - // TODO: double check this - - for byte in output_bytes { - while (!(DUT.output_axis_tvalid == 1'b1)) { - step(); - } - - assert_eq(DUT.output_axis_tdata, byte); - - if iter_count::() == 3'd0 { - // For the `i`-th output byte, the output `tkeep` bit is `keep[i]` - assert_eq(DUT.output_axis_tkeep, keep[0]); - if is_last() { - assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); - // Current byte is the last one, so the next byte is not kept - assert_eq(keep[1], 1'b0); - } else { - assert_eq(DUT.output_axis_tlast, 1'b0); - - // Current byte is not the last one, so the next byte is kept - assert_eq(keep[1], 1'b1); - } - } else { - if iter_count::() == 3'd1 { - assert_eq(DUT.output_axis_tkeep, keep[1]); - if is_last() { - assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); - // The current byte is the last one, so the next byte is not kept - assert_eq(keep[2], 1'b0); - } else { - assert_eq(DUT.output_axis_tlast, 1'b0); - // The current byte is not the last one, so the next byte is kept - assert_eq(keep[2], 1'b1); - } - } else { - if iter_count::() == 3'd2 { - assert_eq(DUT.output_axis_tkeep, keep[2]); - if is_last() { - assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); - // The current byte is the last one, so the next byte is not kept - assert_eq(keep[3], 1'b0); - } else { - assert_eq(DUT.output_axis_tlast, 1'b0); - // The current byte is not the last one, so the next byte is kept - assert_eq(keep[3], 1'b1); - } - } else { - if iter_count::() == 3'd3 { - assert_eq(DUT.output_axis_tkeep, keep[3]); - if is_last() { - assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); - // The current byte is the last one, so the next byte is not kept - assert_eq(keep[4], 1'b0); - } else { - assert_eq(DUT.output_axis_tlast, 1'b0); - // The current byte is not the last one, so the next byte is kept - assert_eq(keep[4], 1'b1); - } - } else { - if iter_count::() == 3'd4 { - assert_eq(DUT.output_axis_tkeep, keep[4]); - if is_last() { - assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); - // The current byte is the last one, so the next byte is not kept - assert_eq(keep[5], 1'b0); - } else { - assert_eq(DUT.output_axis_tlast, 1'b0); - // The current byte is not the last one, so the next byte is kept - assert_eq(keep[5], 1'b1); - } - } else { - if iter_count::() == 3'd5 { - assert_eq(DUT.output_axis_tkeep, keep[5]); - if is_last() { - assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); - // The current byte is the last one, so the next byte is not kept - assert_eq(keep[6], 1'b0); - } else { - assert_eq(DUT.output_axis_tlast, 1'b0); - // The current byte is not the last one, so the next byte is kept - assert_eq(keep[6], 1'b1); - } - } else { - if iter_count::() == 3'd6 { - assert_eq(DUT.output_axis_tkeep, keep[6]); - if is_last() { - assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); - // The current byte is the last one, so the next byte is not kept - assert_eq(keep[7], 1'b0); - } else { - assert_eq(DUT.output_axis_tlast, 1'b0); - // The current byte is not the last one, so the next byte is kept - assert_eq(keep[7], 1'b1); - } - } else { - // Last iteration (can't have more than 8 bytes in a 64-bit output) - assert_eq(DUT.output_axis_tkeep, keep[7]); - - if is_last() { - assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); - } else { - assert_eq(DUT.output_axis_tlast, 1'b0); - } - } - } - } - } - } - } - } - - step(); - } -} From 3943045cab17b6356ef3578f4c241176018ad447 Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Tue, 25 Aug 2026 16:10:33 -0400 Subject: [PATCH 09/29] Update expect file --- .../axis-adapter-s3/expects/s3_buggy.bi.expect | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/tests/fpga-debugging/axis-adapter-s3/expects/s3_buggy.bi.expect b/tests/fpga-debugging/axis-adapter-s3/expects/s3_buggy.bi.expect index ebf4e835..7d17cff4 100644 --- a/tests/fpga-debugging/axis-adapter-s3/expects/s3_buggy.bi.expect +++ b/tests/fpga-debugging/axis-adapter-s3/expects/s3_buggy.bi.expect @@ -5,9 +5,9 @@ trace { idle(); // [time: 50ns -> 75ns] } error: [split_word@3] executing step 5 of the transaction: 0 != 1 - ┌─ tests/fpga-debugging/axis-adapter-s3/s3.prot:169:33 + ┌─ tests/fpga-debugging/axis-adapter-s3/s3.prot:178:33 │ -169 │ assert_eq(keep[5], 1'b1); +178 │ assert_eq(keep[5], 1'b1); │ ^^^^^^^^^^^^^^^^^^^^^^^^^ [split_word@3] executing step 5 of the transaction: 0 != 1 @@ -18,9 +18,9 @@ trace { idle(); // [time: 50ns -> 75ns] } error: [split_word@3L] executing step 5 of the transaction: 0 != 1 - ┌─ tests/fpga-debugging/axis-adapter-s3/s3.prot:163:33 + ┌─ tests/fpga-debugging/axis-adapter-s3/s3.prot:172:33 │ -163 │ assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); +172 │ assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); │ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ [split_word@3L] executing step 5 of the transaction: 0 != 1 ---CODE--- From f6c10b475e0e84be33af2513792f92fb3a47391a Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Tue, 25 Aug 2026 16:14:35 -0400 Subject: [PATCH 10/29] Add clarifying comments --- tests/fpga-debugging/axis-adapter-s3/s3.prot | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/tests/fpga-debugging/axis-adapter-s3/s3.prot b/tests/fpga-debugging/axis-adapter-s3/s3.prot index 80ebd5e7..04f6a77a 100644 --- a/tests/fpga-debugging/axis-adapter-s3/s3.prot +++ b/tests/fpga-debugging/axis-adapter-s3/s3.prot @@ -82,6 +82,9 @@ prot idle() { step(); } +// - `is_final_word_in_packet` is an parameter that represents `tlast` +// (this variable name was chosen to be more informative and to avoid confusion with our DSL's `is_last()` construct) +// - `output_bytes` is the sequence of bytes that the DUT produces as output prot split_word(data: u64, keep: u8, is_final_word_in_packet: u1, output_bytes: [u8]+) { DUT.rst := 1'b0; DUT.input_axis_tdata := data; @@ -96,7 +99,7 @@ prot split_word(data: u64, keep: u8, is_final_word_in_packet: u1, out // One cycle for DUT to accept input data from environment step(); - // DUT has accepted input data, so we set the input pins to DOntCare + // DUT has accepted input data, so we set the input pins to DontCare DUT.input_axis_tdata := X; DUT.input_axis_tkeep := X; DUT.input_axis_tlast := X; @@ -107,8 +110,6 @@ prot split_word(data: u64, keep: u8, is_final_word_in_packet: u1, out // DUT is ready to emit output data DUT.output_axis_tready := 1'b1; - // TODO: double check this - for byte in output_bytes { while (!(DUT.output_axis_tvalid == 1'b1)) { step(); From aa77ac5b489c08ef7473e331b1124b86f5544768 Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Tue, 25 Aug 2026 16:17:20 -0400 Subject: [PATCH 11/29] more comments --- tests/fpga-debugging/axis-adapter-s3/s3.prot | 24 ++++++++++---------- 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/tests/fpga-debugging/axis-adapter-s3/s3.prot b/tests/fpga-debugging/axis-adapter-s3/s3.prot index 04f6a77a..ae40d6c7 100644 --- a/tests/fpga-debugging/axis-adapter-s3/s3.prot +++ b/tests/fpga-debugging/axis-adapter-s3/s3.prot @@ -135,11 +135,11 @@ prot split_word(data: u64, keep: u8, is_final_word_in_packet: u1, out assert_eq(DUT.output_axis_tkeep, keep[1]); if is_last() { assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); - // The current byte is the last one, so the next byte is not kept + // The current byte is the final byte emitted by the DUT, so the next byte's corresponding `tkeep` bit must be 0 assert_eq(keep[2], 1'b0); } else { assert_eq(DUT.output_axis_tlast, 1'b0); - // The current byte is not the last one, so the next byte is kept + // The current byte is *not* the final byte emitted by the DUT, so the next byte's corresponding `tkeep` bit must be 1 assert_eq(keep[2], 1'b1); } } else { @@ -147,11 +147,11 @@ prot split_word(data: u64, keep: u8, is_final_word_in_packet: u1, out assert_eq(DUT.output_axis_tkeep, keep[2]); if is_last() { assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); - // The current byte is the last one, so the next byte is not kept + // The current byte is the final byte emitted by the DUT, so the next byte's corresponding `tkeep` bit must be 0 assert_eq(keep[3], 1'b0); } else { assert_eq(DUT.output_axis_tlast, 1'b0); - // The current byte is not the last one, so the next byte is kept + // The current byte is *not* the final byte emitted by the DUT, so the next byte's corresponding `tkeep` bit must be 1 assert_eq(keep[3], 1'b1); } } else { @@ -159,11 +159,11 @@ prot split_word(data: u64, keep: u8, is_final_word_in_packet: u1, out assert_eq(DUT.output_axis_tkeep, keep[3]); if is_last() { assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); - // The current byte is the last one, so the next byte is not kept + // The current byte is the final byte emitted by the DUT, so the next byte's corresponding `tkeep` bit must be 0 assert_eq(keep[4], 1'b0); } else { assert_eq(DUT.output_axis_tlast, 1'b0); - // The current byte is not the last one, so the next byte is kept + // The current byte is *not* the final byte emitted by the DUT, so the next byte's corresponding `tkeep` bit must be 1 assert_eq(keep[4], 1'b1); } } else { @@ -171,11 +171,11 @@ prot split_word(data: u64, keep: u8, is_final_word_in_packet: u1, out assert_eq(DUT.output_axis_tkeep, keep[4]); if is_last() { assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); - // The current byte is the last one, so the next byte is not kept + // The current byte is the final byte emitted by the DUT, so the next byte's corresponding `tkeep` bit must be 0 assert_eq(keep[5], 1'b0); } else { assert_eq(DUT.output_axis_tlast, 1'b0); - // The current byte is not the last one, so the next byte is kept + // The current byte is *not* the final byte emitted by the DUT, so the next byte's corresponding `tkeep` bit must be 1 assert_eq(keep[5], 1'b1); } } else { @@ -183,11 +183,11 @@ prot split_word(data: u64, keep: u8, is_final_word_in_packet: u1, out assert_eq(DUT.output_axis_tkeep, keep[5]); if is_last() { assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); - // The current byte is the last one, so the next byte is not kept + // The current byte is the final byte emitted by the DUT, so the next byte's corresponding `tkeep` bit must be 0 assert_eq(keep[6], 1'b0); } else { assert_eq(DUT.output_axis_tlast, 1'b0); - // The current byte is not the last one, so the next byte is kept + // The current byte is *not* the final byte emitted by the DUT, so the next byte's corresponding `tkeep` bit must be 1 assert_eq(keep[6], 1'b1); } } else { @@ -195,11 +195,11 @@ prot split_word(data: u64, keep: u8, is_final_word_in_packet: u1, out assert_eq(DUT.output_axis_tkeep, keep[6]); if is_last() { assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); - // The current byte is the last one, so the next byte is not kept + // The current byte is the final byte emitted by the DUT, so the next byte's corresponding `tkeep` bit must be 0 assert_eq(keep[7], 1'b0); } else { assert_eq(DUT.output_axis_tlast, 1'b0); - // The current byte is not the last one, so the next byte is kept + // The current byte is *not* the final byte emitted by the DUT, so the next byte's corresponding `tkeep` bit must be 1 assert_eq(keep[7], 1'b1); } } else { From d7a962320ab0b19ec3cd751e8a68b409f6a769c3 Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Tue, 25 Aug 2026 16:17:47 -0400 Subject: [PATCH 12/29] Update expect test output --- .../axis-adapter-s3/expects/s3_buggy.bi.expect | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/tests/fpga-debugging/axis-adapter-s3/expects/s3_buggy.bi.expect b/tests/fpga-debugging/axis-adapter-s3/expects/s3_buggy.bi.expect index 7d17cff4..11b62615 100644 --- a/tests/fpga-debugging/axis-adapter-s3/expects/s3_buggy.bi.expect +++ b/tests/fpga-debugging/axis-adapter-s3/expects/s3_buggy.bi.expect @@ -5,9 +5,9 @@ trace { idle(); // [time: 50ns -> 75ns] } error: [split_word@3] executing step 5 of the transaction: 0 != 1 - ┌─ tests/fpga-debugging/axis-adapter-s3/s3.prot:178:33 + ┌─ tests/fpga-debugging/axis-adapter-s3/s3.prot:179:33 │ -178 │ assert_eq(keep[5], 1'b1); +179 │ assert_eq(keep[5], 1'b1); │ ^^^^^^^^^^^^^^^^^^^^^^^^^ [split_word@3] executing step 5 of the transaction: 0 != 1 @@ -18,9 +18,9 @@ trace { idle(); // [time: 50ns -> 75ns] } error: [split_word@3L] executing step 5 of the transaction: 0 != 1 - ┌─ tests/fpga-debugging/axis-adapter-s3/s3.prot:172:33 + ┌─ tests/fpga-debugging/axis-adapter-s3/s3.prot:173:33 │ -172 │ assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); +173 │ assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); │ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ [split_word@3L] executing step 5 of the transaction: 0 != 1 ---CODE--- From 4c5935a28544e48ef2f86bbb348c10751f67632e Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Tue, 25 Aug 2026 16:22:19 -0400 Subject: [PATCH 13/29] More comments --- .../axis-adapter-s3/expects/s3_buggy.bi.expect | 8 ++++---- tests/fpga-debugging/axis-adapter-s3/s3.prot | 11 +++++++++-- 2 files changed, 13 insertions(+), 6 deletions(-) diff --git a/tests/fpga-debugging/axis-adapter-s3/expects/s3_buggy.bi.expect b/tests/fpga-debugging/axis-adapter-s3/expects/s3_buggy.bi.expect index 11b62615..5178d4cf 100644 --- a/tests/fpga-debugging/axis-adapter-s3/expects/s3_buggy.bi.expect +++ b/tests/fpga-debugging/axis-adapter-s3/expects/s3_buggy.bi.expect @@ -5,9 +5,9 @@ trace { idle(); // [time: 50ns -> 75ns] } error: [split_word@3] executing step 5 of the transaction: 0 != 1 - ┌─ tests/fpga-debugging/axis-adapter-s3/s3.prot:179:33 + ┌─ tests/fpga-debugging/axis-adapter-s3/s3.prot:180:33 │ -179 │ assert_eq(keep[5], 1'b1); +180 │ assert_eq(keep[5], 1'b1); │ ^^^^^^^^^^^^^^^^^^^^^^^^^ [split_word@3] executing step 5 of the transaction: 0 != 1 @@ -18,9 +18,9 @@ trace { idle(); // [time: 50ns -> 75ns] } error: [split_word@3L] executing step 5 of the transaction: 0 != 1 - ┌─ tests/fpga-debugging/axis-adapter-s3/s3.prot:173:33 + ┌─ tests/fpga-debugging/axis-adapter-s3/s3.prot:174:33 │ -173 │ assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); +174 │ assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); │ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ [split_word@3L] executing step 5 of the transaction: 0 != 1 ---CODE--- diff --git a/tests/fpga-debugging/axis-adapter-s3/s3.prot b/tests/fpga-debugging/axis-adapter-s3/s3.prot index ae40d6c7..b74ffc85 100644 --- a/tests/fpga-debugging/axis-adapter-s3/s3.prot +++ b/tests/fpga-debugging/axis-adapter-s3/s3.prot @@ -1,7 +1,8 @@ -// AXI-Stream width adapter which converts a 64-bit input into 8-bit outputs over multiple cycles +// This file describes an AXI-Stream width adapter which +// converts a 64-bit input into 8-bit output chunks over multiple cycles // Notes: -// - The DUT has 3 termination conditions +// - The DUT has 3 termination conditions: // - 1. All the bytes corresponding to the rightmost contiguous sequence of 1s in `tkeep` are emitted, // e.g. tkeep = 11111111 (all bytes of `tdata` are meaningful) // or tkeep = 00011111 (the 5 least significant bytes of `tdata` are meaningful) @@ -206,6 +207,9 @@ prot split_word(data: u64, keep: u8, is_final_word_in_packet: u1, out // Last iteration (can't have more than 8 bytes in a 64-bit output) assert_eq(DUT.output_axis_tkeep, keep[7]); + // Since this is the last iteration of the for-each loop, + // there is no "next" bit of `tkeep` to inspect, so + // we only need to check `tlast` for the remainder of this case if is_last() { assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); } else { @@ -219,6 +223,9 @@ prot split_word(data: u64, keep: u8, is_final_word_in_packet: u1, out } } + // We need this step for well-formedness, since + // each loop iteration must take at least one-step + // (the DUT also emits at most one byte in one clock cycle) step(); } } From 69548904b98e083f847f039b66e2b3cea70ef2d8 Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Tue, 25 Aug 2026 18:13:26 -0400 Subject: [PATCH 14/29] Rewrite split_word by removing output_bytes parameter --- runt/bi/runt.toml | 2 +- scripts/test_catalog.py | 1 - .../expects/s3_buggy.bi.expect | 19 +- .../expects/s3_fixed.bi.expect | 2 +- tests/fpga-debugging/axis-adapter-s3/s3.prot | 295 +++++++++++------- 5 files changed, 190 insertions(+), 129 deletions(-) diff --git a/runt/bi/runt.toml b/runt/bi/runt.toml index 7a042c65..d86248eb 100644 --- a/runt/bi/runt.toml +++ b/runt/bi/runt.toml @@ -2392,7 +2392,7 @@ paths = [ ] expect_dir = "../../tests/fpga-debugging/axis-adapter-s3/expects" expect_name = "s3_fixed.bi.expect" -cmd = "cd ../.. && target/debug/bi --color never --protocol tests/fpga-debugging/axis-adapter-s3/s3.prot --wave tests/fpga-debugging/axis-adapter-s3/s3_fixed.fst --instances TOP.test_axis_adapter_64_8.UUT:AXIS --sample-posedge TOP.test_axis_adapter_64_8.UUT.clk --show-waveform-time --include-idle --time-unit ns --include-in-progress --display-hex 2>&1" +cmd = "cd ../.. && target/debug/bi --color never --protocol tests/fpga-debugging/axis-adapter-s3/s3.prot --wave tests/fpga-debugging/axis-adapter-s3/s3_fixed.fst --instances TOP.test_axis_adapter_64_8.UUT:AXIS --sample-posedge TOP.test_axis_adapter_64_8.UUT.clk --show-waveform-time --include-idle --time-unit ns --display-hex 2>&1" [[tests]] name = "bi.tests_fpga_debugging_axis_async_fifo_c4_c4.c4_buggy_bi" diff --git a/scripts/test_catalog.py b/scripts/test_catalog.py index 3facbdce..a939344b 100644 --- a/scripts/test_catalog.py +++ b/scripts/test_catalog.py @@ -725,7 +725,6 @@ "--include-idle", "--time-unit", "ns", - "--include-in-progress", "--display-hex", ), }, diff --git a/tests/fpga-debugging/axis-adapter-s3/expects/s3_buggy.bi.expect b/tests/fpga-debugging/axis-adapter-s3/expects/s3_buggy.bi.expect index 5178d4cf..e39f189a 100644 --- a/tests/fpga-debugging/axis-adapter-s3/expects/s3_buggy.bi.expect +++ b/tests/fpga-debugging/axis-adapter-s3/expects/s3_buggy.bi.expect @@ -5,23 +5,10 @@ trace { idle(); // [time: 50ns -> 75ns] } error: [split_word@3] executing step 5 of the transaction: 0 != 1 - ┌─ tests/fpga-debugging/axis-adapter-s3/s3.prot:180:33 + ┌─ tests/fpga-debugging/axis-adapter-s3/s3.prot:198:25 │ -180 │ assert_eq(keep[5], 1'b1); - │ ^^^^^^^^^^^^^^^^^^^^^^^^^ [split_word@3] executing step 5 of the transaction: 0 != 1 - - -// trace 1 -trace { - reset(); // [time: 0ns -> 25ns] - idle(); // [time: 25ns -> 50ns] - idle(); // [time: 50ns -> 75ns] -} -error: [split_word@3L] executing step 5 of the transaction: 0 != 1 - ┌─ tests/fpga-debugging/axis-adapter-s3/s3.prot:174:33 - │ -174 │ assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); - │ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ [split_word@3L] executing step 5 of the transaction: 0 != 1 +198 │ assert_eq(keep[5], 1'b1); + │ ^^^^^^^^^^^^^^^^^^^^^^^^^ [split_word@3] executing step 5 of the transaction: 0 != 1 ---CODE--- 1 diff --git a/tests/fpga-debugging/axis-adapter-s3/expects/s3_fixed.bi.expect b/tests/fpga-debugging/axis-adapter-s3/expects/s3_fixed.bi.expect index 94fd93a2..3edc3603 100644 --- a/tests/fpga-debugging/axis-adapter-s3/expects/s3_fixed.bi.expect +++ b/tests/fpga-debugging/axis-adapter-s3/expects/s3_fixed.bi.expect @@ -3,5 +3,5 @@ trace { reset(); // [time: 0ns -> 25ns] idle(); // [time: 25ns -> 50ns] idle(); // [time: 50ns -> 75ns] - split_word(0xabcdabcdabcdabcd, 0x1f, 0x1, 0x[cd, ab, cd, ab, cd]); // [time: 75ns -> ] + split_word(0xabcdabcdabcdabcd, 0x1f, 0x1); // [time: 75ns -> 200ns] } diff --git a/tests/fpga-debugging/axis-adapter-s3/s3.prot b/tests/fpga-debugging/axis-adapter-s3/s3.prot index b74ffc85..bdee8733 100644 --- a/tests/fpga-debugging/axis-adapter-s3/s3.prot +++ b/tests/fpga-debugging/axis-adapter-s3/s3.prot @@ -3,11 +3,17 @@ // Notes: // - The DUT has 3 termination conditions: -// - 1. All the bytes corresponding to the rightmost contiguous sequence of 1s in `tkeep` are emitted, -// e.g. tkeep = 11111111 (all bytes of `tdata` are meaningful) -// or tkeep = 00011111 (the 5 least significant bytes of `tdata` are meaningful) -// - 2. When emitting the i-th byte, the DUT sees that tkeep[i] = 0, in which case it treats the i-th byte as the last one and stops emitting any further bytes -// - 3. For the fixed DUT only, it truncates the output after `i` bytes if it detects that `input_tkeep[i + 1] = 0` +// - 1. All 8 bytes have been emitted (in the fixed DUT, this only happens when `tkeep = 11111111`, i.e. all bytes of `tdata` are meaningful) +// - 2. When emitting the i-th byte, the DUT sees that `tkeep[i] = 0`, in which case it treats the i-th byte as the last one and stops emitting any further bytes +// - 3. For the fixed DUT only, if `tkeep[i] = 1` but `tkeep[i+1] = 0`, then the DUT treats the `i`-th byte as the last one +// and stops emitting any further bytes (the fixed DUT gains this "lookahead" logic) +// - The `tlast` parameter indicates if the data word corresponds to the final word of a packet +// (Note: there can be multiple words in a packet. Moreover, the last byte of a non-final word in a packet +// still gets `tlast = 0`, since it is not the last word of a packet.) +// - AXI-Stream spec says that for "downsizing" operations in which data with larger bit-widths +// are converted to smaller bitwidths (section 2.3.3), which this DUT is doing, +// if the input data word happens to be the last word of a packet (i.e. `tlast = 1` for the input), +// in the output sequence of bytes, `tlast` can only be asserted for the last byte emitted // - The DUT cannot accept a new 64-bit input when it is still emitting the bytes of the existing data // - The DUT examines `tkeep` from right to left, i.e. the 0th byte emitted // corresponds to `tdata[7:0]` and `tkeep[0]` (the LSB of `tkeep`) @@ -83,17 +89,18 @@ prot idle() { step(); } -// - `is_final_word_in_packet` is an parameter that represents `tlast` +// - `is_final_word_in_packet` is a parameter that represents `tlast` // (this variable name was chosen to be more informative and to avoid confusion with our DSL's `is_last()` construct) -// - `output_bytes` is the sequence of bytes that the DUT produces as output -prot split_word(data: u64, keep: u8, is_final_word_in_packet: u1, output_bytes: [u8]+) { +prot split_word(data: u64, keep: u8, is_final_word_in_packet: u1) { DUT.rst := 1'b0; DUT.input_axis_tdata := data; DUT.input_axis_tkeep := keep; DUT.input_axis_tlast := is_final_word_in_packet; + + // There is valid data (namely the input word), so set `valid = 1` DUT.input_axis_tvalid := 1'b1; - // Wait until the DUT signals that it has taken the word + // Wait until the DUT signals it is ready to accept to the input word while (!(DUT.input_axis_tready == 1'b1)) { step(); } @@ -105,127 +112,195 @@ prot split_word(data: u64, keep: u8, is_final_word_in_packet: u1, out DUT.input_axis_tkeep := X; DUT.input_axis_tlast := X; - // Since input pins are DontCare, we also set `input_tvalid` to DontCare - DUT.input_axis_tvalid := X; + // Since input pins are DontCare, there is no longer valid data, so set `valid = 0` + DUT.input_axis_tvalid := 1'b0; - // DUT is ready to emit output data + // Environment is now ready to accept the output data emitted by the DUT DUT.output_axis_tready := 1'b1; - for byte in output_bytes { + // Wait until the DUT indicates that the next byte is valid for emitting + while (!(DUT.output_axis_tvalid == 1'b1)) { + step(); + } + + // 0th (rightmost) bit of `keep` is the current value of `tkeep` + assert_eq(DUT.output_axis_tkeep, keep[0]); + + // Rightmost 8 bits of `data` are now on the `output_tdata` pin + assert_eq(DUT.output_axis_tdata, data[7:0]); + + // If the 0th byte was not the final byte in an entire packet + // (note: it could still be the last byte in the data word, but + // AXI-S) + if (DUT.output_axis_tlast == 1'b0) { + // Then the 1st byte (the next byte) must be kept, + // i.e. its `tkeep` bit must be 1 + assert_eq(keep[1], 1'b1); + // One clock cycle to emit the 0th byte + step(); + + // Wait until the DUT indicates that the next byte is valid for emitting while (!(DUT.output_axis_tvalid == 1'b1)) { step(); - } + } + // DUT provides the next byte of data and its `tkeep` bit on the output pins + assert_eq(DUT.output_axis_tdata, data[15:8]); + assert_eq(DUT.output_axis_tkeep, keep[1]); - assert_eq(DUT.output_axis_tdata, byte); + // If the 1st byte is not the final byte in the entire packet + if (DUT.output_axis_tlast == 1'b0) { + // then the 2nd byte must be kept, i.e. its `tkeep` bit must be 1 + assert_eq(keep[2], 1'b1); + // One clock cycle to emit the 1st byte + step(); - if iter_count::() == 3'd0 { - // For the `i`-th output byte, the output `tkeep` bit is `keep[i]` - assert_eq(DUT.output_axis_tkeep, keep[0]); - if is_last() { - assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); - // Current byte is the last one, so the next byte is not kept - assert_eq(keep[1], 1'b0); - } else { - assert_eq(DUT.output_axis_tlast, 1'b0); - - // Current byte is not the last one, so the next byte is kept - assert_eq(keep[1], 1'b1); + // Wait until the DUT indicates that the next byte is valid for emitting + while (!(DUT.output_axis_tvalid == 1'b1)) { + step(); } - } else { - if iter_count::() == 3'd1 { - assert_eq(DUT.output_axis_tkeep, keep[1]); - if is_last() { - assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); - // The current byte is the final byte emitted by the DUT, so the next byte's corresponding `tkeep` bit must be 0 - assert_eq(keep[2], 1'b0); - } else { - assert_eq(DUT.output_axis_tlast, 1'b0); - // The current byte is *not* the final byte emitted by the DUT, so the next byte's corresponding `tkeep` bit must be 1 - assert_eq(keep[2], 1'b1); + // DUT provides the next byte of data and its `tkeep` bit on the output pins + assert_eq(DUT.output_axis_tdata, data[23:16]); + assert_eq(DUT.output_axis_tkeep, keep[2]); + + // If the 2nd byte isn't the final byte in a packet + if (DUT.output_axis_tlast == 1'b0) { + // Then the 3rd byte must be kept, i.e. its `tkeep` bit is 1 + assert_eq(keep[3], 1'b1); + // One clock cycle to emit the 2nd byte + step(); + + // Wait until the DUT indicates that the next byte is valid for emitting + while (!(DUT.output_axis_tvalid == 1'b1)) { + step(); } - } else { - if iter_count::() == 3'd2 { - assert_eq(DUT.output_axis_tkeep, keep[2]); - if is_last() { - assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); - // The current byte is the final byte emitted by the DUT, so the next byte's corresponding `tkeep` bit must be 0 - assert_eq(keep[3], 1'b0); - } else { - assert_eq(DUT.output_axis_tlast, 1'b0); - // The current byte is *not* the final byte emitted by the DUT, so the next byte's corresponding `tkeep` bit must be 1 - assert_eq(keep[3], 1'b1); + // DUT provides the next byte of data and its `tkeep` bit on the output pins + assert_eq(DUT.output_axis_tdata, data[31:24]); + assert_eq(DUT.output_axis_tkeep, keep[3]); + + // If the 3rd byte isn't the final byte in a packet + if (DUT.output_axis_tlast == 1'b0) { + // Then the 4th byte must be kept + assert_eq(keep[4], 1'b1); + // One clock cycle to emit the 3rd byte + step(); + + // Wait until the DUT indicates that the next byte is valid for emitting + while (!(DUT.output_axis_tvalid == 1'b1)) { + step(); } - } else { - if iter_count::() == 3'd3 { - assert_eq(DUT.output_axis_tkeep, keep[3]); - if is_last() { - assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); - // The current byte is the final byte emitted by the DUT, so the next byte's corresponding `tkeep` bit must be 0 - assert_eq(keep[4], 1'b0); - } else { - assert_eq(DUT.output_axis_tlast, 1'b0); - // The current byte is *not* the final byte emitted by the DUT, so the next byte's corresponding `tkeep` bit must be 1 - assert_eq(keep[4], 1'b1); + // DUT provides the next byte of data and its `tkeep` bit on the output pins + assert_eq(DUT.output_axis_tdata, data[39:32]); + assert_eq(DUT.output_axis_tkeep, keep[4]); + + // If the 4th byte wasn't the last byte of a packet + if (DUT.output_axis_tlast == 1'b0) { + // The 5th byte must be kept + assert_eq(keep[5], 1'b1); + // One clock cycle to emit the 4th byte + step(); + + // Wait until DUT has valid data to emit + while (!(DUT.output_axis_tvalid == 1'b1)) { + step(); } - } else { - if iter_count::() == 3'd4 { - assert_eq(DUT.output_axis_tkeep, keep[4]); - if is_last() { - assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); - // The current byte is the final byte emitted by the DUT, so the next byte's corresponding `tkeep` bit must be 0 - assert_eq(keep[5], 1'b0); - } else { - assert_eq(DUT.output_axis_tlast, 1'b0); - // The current byte is *not* the final byte emitted by the DUT, so the next byte's corresponding `tkeep` bit must be 1 - assert_eq(keep[5], 1'b1); + // DUT provides the next byte of data and its `tkeep` on its output pins + assert_eq(DUT.output_axis_tdata, data[47:40]); + assert_eq(DUT.output_axis_tkeep, keep[5]); + + // If the 5th byte wasn't the last byte of a packet + if (DUT.output_axis_tlast == 1'b0) { + // The 6th byte must be kept + assert_eq(keep[6], 1'b1); + // One clock cycle to emit the 5th byte + step(); + + // Wait until DUT has valid data to emit + while (!(DUT.output_axis_tvalid == 1'b1)) { + step(); } - } else { - if iter_count::() == 3'd5 { - assert_eq(DUT.output_axis_tkeep, keep[5]); - if is_last() { - assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); - // The current byte is the final byte emitted by the DUT, so the next byte's corresponding `tkeep` bit must be 0 - assert_eq(keep[6], 1'b0); - } else { - assert_eq(DUT.output_axis_tlast, 1'b0); - // The current byte is *not* the final byte emitted by the DUT, so the next byte's corresponding `tkeep` bit must be 1 - assert_eq(keep[6], 1'b1); + // DUT provides the next byte of data and its `tkeep` on its output pins + assert_eq(DUT.output_axis_tdata, data[55:48]); + assert_eq(DUT.output_axis_tkeep, keep[6]); + + // If the 6th byte wasn't the last byte of a packet + if (DUT.output_axis_tlast == 1'b0) { + // The 7th byte must be kept + assert_eq(keep[7], 1'b1); + // One clock cycle to emit the 6th byte + step(); + + // Wait until DUT has valid data to emit + while (!(DUT.output_axis_tvalid == 1'b1)) { + step(); } + // DUT provides the final byte of data and its `tkeep` on its output pins + assert_eq(DUT.output_axis_tdata, data[63:56]); + assert_eq(DUT.output_axis_tkeep, keep[7]); + + // The 7th byte is the last byte for a 64-bit word, + // so we don't need to inspect the `tkeep` bit for the "next" byte + // We only need to check whether this byte is the end of the + // of the entire packet, which is determined by the `is_final_word_in_packet` parameter + assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); + + // One clock cycle to emit the 7th byte + step(); } else { - if iter_count::() == 3'd6 { - assert_eq(DUT.output_axis_tkeep, keep[6]); - if is_last() { - assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); - // The current byte is the final byte emitted by the DUT, so the next byte's corresponding `tkeep` bit must be 0 - assert_eq(keep[7], 1'b0); - } else { - assert_eq(DUT.output_axis_tlast, 1'b0); - // The current byte is *not* the final byte emitted by the DUT, so the next byte's corresponding `tkeep` bit must be 1 - assert_eq(keep[7], 1'b1); - } - } else { - // Last iteration (can't have more than 8 bytes in a 64-bit output) - assert_eq(DUT.output_axis_tkeep, keep[7]); - - // Since this is the last iteration of the for-each loop, - // there is no "next" bit of `tkeep` to inspect, so - // we only need to check `tlast` for the remainder of this case - if is_last() { - assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); - } else { - assert_eq(DUT.output_axis_tlast, 1'b0); - } + // 6th byte was the last byte of a packet + // If the 6th byte is also kept, then the 7th byte must not be kept + if (DUT.output_axis_tkeep == 1'b1) { + assert_eq(keep[7], 1'b0); } + step(); } + } else { + // 5th byte was the last byte of a packet + // If the 5th byte is also kept, then the 6th byte must not be kept + if (DUT.output_axis_tkeep == 1'b1) { + assert_eq(keep[6], 1'b0); + } + step(); + } + } else { + // 4th byte was the last byte in a packet + // If the 4th byte is also kept, then the 5th byte must not be kept + if (DUT.output_axis_tkeep == 1'b1) { + assert_eq(keep[5], 1'b0); } + step(); } + } else { + // 3rd byte was the last byte in an entire packet + // If the 3rd byte is kept as well, then the 4th byte must not be kept (its `tkeep` bit must be 0) + if (DUT.output_axis_tkeep == 1'b1) { + assert_eq(keep[4], 1'b0); + } + step(); + } + + } else { + // 2nd byte was the last byte in an entire packet + // If the 2nd byte is kept as well, then the 3rd-byte's `tkeep` must be 0 (i.e. 3rd byte is not kept) + if (DUT.output_axis_tkeep == 1'b1) { + assert_eq(keep[3], 1'b0); } + step(); } + } else { + // 1st byte was the last byte in an entire packet + // If the 1st byte is kept as well, then the 2nd-byte's `tkeep` bit must be 0 (i.e. 2nd byte is not kept) + if (DUT.output_axis_tkeep == 1'b1) { + assert_eq(keep[2], 1'b0); + } + step(); + } + } else { + // 0th byte was the last byte of the last word of a packet, i.e. `output_axis_tlast == 1` + // If the 0th byte is kept as well (i.e. `tkeep = 1`), + // then we know the next byte's corresponding `tkeep` must be 0 (i.e. is not kept) + if (DUT.output_axis_tkeep == 1'b1) { + assert_eq(keep[1], 1'b0); } - - // We need this step for well-formedness, since - // each loop iteration must take at least one-step - // (the DUT also emits at most one byte in one clock cycle) step(); } -} +} \ No newline at end of file From 2155328cde67798f0ec185e426717bc385417d6e Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Tue, 25 Aug 2026 18:29:12 -0400 Subject: [PATCH 15/29] Get interpreter to drive fixed version of DUT --- runt/graph_interp/runt.toml | 27 +++++++++++++++++++ runt/interp/runt.toml | 10 +++++++ runt/waveform/runt.toml | 27 +++++++++++++++++++ scripts/generate_runt_configs.py | 2 ++ scripts/test_catalog.py | 6 +++++ .../expects/s3_fixed.graph_interp.expect | 1 + .../expects/s3_fixed.interp.expect | 1 + .../expects/s3_fixed.waveform.expect | 12 +++++++++ .../axis-adapter-s3/s3_fixed.tx | 6 +++++ 9 files changed, 92 insertions(+) create mode 100644 tests/fpga-debugging/axis-adapter-s3/expects/s3_fixed.graph_interp.expect create mode 100644 tests/fpga-debugging/axis-adapter-s3/expects/s3_fixed.interp.expect create mode 100644 tests/fpga-debugging/axis-adapter-s3/expects/s3_fixed.waveform.expect create mode 100644 tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx diff --git a/runt/graph_interp/runt.toml b/runt/graph_interp/runt.toml index 373c5075..f273a862 100644 --- a/runt/graph_interp/runt.toml +++ b/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_adapter_s3_s3_fixed.s3_fixed_graph_interp" +paths = [ + "../../tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx", +] +expect_dir = "../../tests/fpga-debugging/axis-adapter-s3/expects" +expect_name = "s3_fixed.graph_interp.expect" +cmd = "cd ../.. && target/debug/graph-interp --transactions tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx --verilog tests/fpga-debugging/axis-adapter-s3/s3_fixed.v --protocol tests/fpga-debugging/axis-adapter-s3/s3.prot --module axis_adapter 2>/dev/null" + +[[tests]] +name = "graph_interp.tests_fpga_debugging_axis_adapter_s3_s3_fixed.s3_fixed_graph_interp.contract_edges" +paths = [ + "../../tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx", +] +expect_dir = "../../tests/fpga-debugging/axis-adapter-s3/expects" +expect_name = "s3_fixed.graph_interp.expect" +cmd = "cd ../.. && target/debug/graph-interp --transactions tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx --verilog tests/fpga-debugging/axis-adapter-s3/s3_fixed.v --protocol tests/fpga-debugging/axis-adapter-s3/s3.prot --module axis_adapter --contract-edges 2>/dev/null" + +[[tests]] +name = "graph_interp.tests_fpga_debugging_axis_adapter_s3_s3_fixed.s3_fixed_graph_interp.respect_forks" +paths = [ + "../../tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx", +] +expect_dir = "../../tests/fpga-debugging/axis-adapter-s3/expects" +expect_name = "s3_fixed.graph_interp.expect" +cmd = "cd ../.. && target/debug/graph-interp --transactions tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx --verilog tests/fpga-debugging/axis-adapter-s3/s3_fixed.v --protocol tests/fpga-debugging/axis-adapter-s3/s3.prot --module axis_adapter --respect-forks --determinize 2>/dev/null" + [[tests]] name = "graph_interp.tests_fpga_debugging_axis_async_fifo_c4_c4_fixed.c4_fixed_graph_interp" paths = [ diff --git a/runt/interp/runt.toml b/runt/interp/runt.toml index 428844fb..5c51a57f 100644 --- a/runt/interp/runt.toml +++ b/runt/interp/runt.toml @@ -450,6 +450,16 @@ expect_dir = "../../tests/fpga-debugging/axi-stream-s2/expects" expect_name = "s2_fixed.interp.expect" cmd = "cd ../.. && target/debug/protocols-interp --color never --transactions tests/fpga-debugging/axi-stream-s2/s2_fixed.tx --verilog tests/fpga-debugging/axi-stream-s2/s2_fixed.v --protocol tests/fpga-debugging/axi-stream-s2/s2.prot --module xlnxstream_2018_3 2>&1" + +[[tests]] +name = "interp.tests_fpga_debugging_axis_adapter_s3_s3_fixed.s3_fixed_interp" +paths = [ + "../../tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx", +] +expect_dir = "../../tests/fpga-debugging/axis-adapter-s3/expects" +expect_name = "s3_fixed.interp.expect" +cmd = "cd ../.. && target/debug/protocols-interp --color never --transactions tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx --verilog tests/fpga-debugging/axis-adapter-s3/s3_fixed.v --protocol tests/fpga-debugging/axis-adapter-s3/s3.prot --module axis_adapter 2>&1" + [[tests]] name = "interp.tests_fpga_debugging_axis_async_fifo_c4_c4_buggy.c4_buggy_interp" paths = [ diff --git a/runt/waveform/runt.toml b/runt/waveform/runt.toml index 579c1232..7d5da4f4 100644 --- a/runt/waveform/runt.toml +++ b/runt/waveform/runt.toml @@ -675,6 +675,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 --bound 6 --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_adapter_s3_s3_fixed.s3_fixed_waveform.ast" +paths = [ + "../../tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx", +] +expect_dir = "../../tests/fpga-debugging/axis-adapter-s3/expects" +expect_name = "s3_fixed.waveform.expect" +cmd = "cd ../.. && target/debug/protocols-interp --color never --transactions tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx --ascii-waveform --verilog tests/fpga-debugging/axis-adapter-s3/s3_fixed.v --protocol tests/fpga-debugging/axis-adapter-s3/s3.prot --module axis_adapter 2>/dev/null" + +[[tests]] +name = "waveform.tests_fpga_debugging_axis_adapter_s3_s3_fixed.s3_fixed_waveform.graph" +paths = [ + "../../tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx", +] +expect_dir = "../../tests/fpga-debugging/axis-adapter-s3/expects" +expect_name = "s3_fixed.waveform.expect" +cmd = "cd ../.. && target/debug/graph-interp --transactions tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx --respect-forks --determinize --ascii-waveform --verilog tests/fpga-debugging/axis-adapter-s3/s3_fixed.v --protocol tests/fpga-debugging/axis-adapter-s3/s3.prot --module axis_adapter 2>/dev/null" + +[[tests]] +name = "waveform.tests_fpga_debugging_axis_adapter_s3_s3_fixed.s3_fixed_waveform.ts" +paths = [ + "../../tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx", +] +expect_dir = "../../tests/fpga-debugging/axis-adapter-s3/expects" +expect_name = "s3_fixed.waveform.expect" +cmd = "cd ../.. && target/debug/graph-interp --transactions tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx --transition-system --ascii-waveform --verilog tests/fpga-debugging/axis-adapter-s3/s3_fixed.v --protocol tests/fpga-debugging/axis-adapter-s3/s3.prot --module axis_adapter 2>/dev/null" + [[tests]] name = "waveform.tests_fpga_debugging_axis_async_fifo_c4_c4_fixed.c4_fixed_waveform.ast" paths = [ diff --git a/scripts/generate_runt_configs.py b/scripts/generate_runt_configs.py index 56e296a0..b3616023 100644 --- a/scripts/generate_runt_configs.py +++ b/scripts/generate_runt_configs.py @@ -252,9 +252,11 @@ def waveform_runt_command(case: dict) -> list[tuple[str, str]]: # (and still 1 min in release mode) to be worth running every time. # maybe in the future we can flag a slow/fast runt config # c4_fixed.tx is simply too long (stack overflows in execution) for now but is fixable + # Note: ignoring `s3_fixed.tx` for graph-interpreter for now as it is a Brave New World test case if ( case["paths"][0] != "examples/picorv32/unsigned_mul.tx" and case["paths"][0] != "tests/fpga-debugging/axis-async-fifo-c4/c4_fixed.tx" + and case["paths"][0] != "tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx" ): variants.append(("bmc", repo_root_command(bounded_cmd, stderr="discard"))) diff --git a/scripts/test_catalog.py b/scripts/test_catalog.py index a939344b..da099188 100644 --- a/scripts/test_catalog.py +++ b/scripts/test_catalog.py @@ -305,6 +305,12 @@ "top": "fifo_wrapper", "expect": "pass", }, + "tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx": { + "protocol": "tests/fpga-debugging/axis-adapter-s3/s3.prot", + "verilog": ("tests/fpga-debugging/axis-adapter-s3/s3_fixed.v",), + "top": "axis_adapter", + "expect": "pass", + }, "tests/fpga-debugging/axi-stream-s2/s2_fixed.tx": { "protocol": "tests/fpga-debugging/axi-stream-s2/s2.prot", "verilog": ("tests/fpga-debugging/axi-stream-s2/s2_fixed.v",), diff --git a/tests/fpga-debugging/axis-adapter-s3/expects/s3_fixed.graph_interp.expect b/tests/fpga-debugging/axis-adapter-s3/expects/s3_fixed.graph_interp.expect new file mode 100644 index 00000000..f5f6cb49 --- /dev/null +++ b/tests/fpga-debugging/axis-adapter-s3/expects/s3_fixed.graph_interp.expect @@ -0,0 +1 @@ +Trace 0 executed successfully! diff --git a/tests/fpga-debugging/axis-adapter-s3/expects/s3_fixed.interp.expect b/tests/fpga-debugging/axis-adapter-s3/expects/s3_fixed.interp.expect new file mode 100644 index 00000000..f5f6cb49 --- /dev/null +++ b/tests/fpga-debugging/axis-adapter-s3/expects/s3_fixed.interp.expect @@ -0,0 +1 @@ +Trace 0 executed successfully! diff --git a/tests/fpga-debugging/axis-adapter-s3/expects/s3_fixed.waveform.expect b/tests/fpga-debugging/axis-adapter-s3/expects/s3_fixed.waveform.expect new file mode 100644 index 00000000..ad5e863a --- /dev/null +++ b/tests/fpga-debugging/axis-adapter-s3/expects/s3_fixed.waveform.expect @@ -0,0 +1,12 @@ +Trace 0 executed successfully! +output_axis_tready x x x 1 1 1 1 1 +input_axis_tlast x 1 1 x x x x x +input_axis_tvalid 0 1 1 0 0 0 0 0 +input_axis_tkeep[7:0] x 31 31 x x x x x +input_axis_tdata[63:0] x 12379739850550389709 12379739850550389709 x x x x x +rst 1 0 0 0 0 0 0 0 +output_axis_tlast 0 0 0 0 0 0 0 1 +output_axis_tvalid 0 0 0 1 1 1 1 1 +output_axis_tkeep 0 0 0 1 1 1 1 1 +output_axis_tdata[7:0] 0 0 0 205 171 205 171 205 +input_axis_tready 0 0 1 0 0 0 0 1 diff --git a/tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx b/tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx new file mode 100644 index 00000000..9bb3da82 --- /dev/null +++ b/tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx @@ -0,0 +1,6 @@ +trace { + reset(); + idle(); + // Same transaction with the same input data, as in `s3_fixed.fst` (waveform from Brave New World artifact) + split_word(0xabcdabcdabcdabcd, 0x1f, 0b1); +} From b96aafd6440a11dc917a8280435dd53d05fafc7c Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Tue, 25 Aug 2026 18:33:55 -0400 Subject: [PATCH 16/29] Update Runt --- .../axis-adapter-s3/expects/s3_fixed.waveform.expect | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/tests/fpga-debugging/axis-adapter-s3/expects/s3_fixed.waveform.expect b/tests/fpga-debugging/axis-adapter-s3/expects/s3_fixed.waveform.expect index ad5e863a..fcba3353 100644 --- a/tests/fpga-debugging/axis-adapter-s3/expects/s3_fixed.waveform.expect +++ b/tests/fpga-debugging/axis-adapter-s3/expects/s3_fixed.waveform.expect @@ -1,9 +1,9 @@ Trace 0 executed successfully! output_axis_tready x x x 1 1 1 1 1 -input_axis_tlast x 1 1 x x x x x -input_axis_tvalid 0 1 1 0 0 0 0 0 -input_axis_tkeep[7:0] x 31 31 x x x x x -input_axis_tdata[63:0] x 12379739850550389709 12379739850550389709 x x x x x +input_axis_tlast x x 1 x x x x x +input_axis_tvalid 0 0 1 0 0 0 0 0 +input_axis_tkeep[7:0] x x 31 x x x x x +input_axis_tdata[63:0] x x 12379739850550389709 x x x x x rst 1 0 0 0 0 0 0 0 output_axis_tlast 0 0 0 0 0 0 0 1 output_axis_tvalid 0 0 0 1 1 1 1 1 From 7fa00e80039c311bd03a75e5552c3b0e34c82fc6 Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Tue, 25 Aug 2026 19:11:52 -0400 Subject: [PATCH 17/29] Rewrite protcool by branching on current value of tkeep for each output byte --- .../expects/s3_buggy.bi.expect | 6 +- tests/fpga-debugging/axis-adapter-s3/s3.prot | 319 ++++++++++-------- 2 files changed, 182 insertions(+), 143 deletions(-) diff --git a/tests/fpga-debugging/axis-adapter-s3/expects/s3_buggy.bi.expect b/tests/fpga-debugging/axis-adapter-s3/expects/s3_buggy.bi.expect index e39f189a..6cf58529 100644 --- a/tests/fpga-debugging/axis-adapter-s3/expects/s3_buggy.bi.expect +++ b/tests/fpga-debugging/axis-adapter-s3/expects/s3_buggy.bi.expect @@ -5,10 +5,10 @@ trace { idle(); // [time: 50ns -> 75ns] } error: [split_word@3] executing step 5 of the transaction: 0 != 1 - ┌─ tests/fpga-debugging/axis-adapter-s3/s3.prot:198:25 + ┌─ tests/fpga-debugging/axis-adapter-s3/s3.prot:237:45 │ -198 │ assert_eq(keep[5], 1'b1); - │ ^^^^^^^^^^^^^^^^^^^^^^^^^ [split_word@3] executing step 5 of the transaction: 0 != 1 +237 │ assert_eq(keep[5], 1'b1); + │ ^^^^^^^^^^^^^^^^^^^^^^^^^ [split_word@3] executing step 5 of the transaction: 0 != 1 ---CODE--- 1 diff --git a/tests/fpga-debugging/axis-adapter-s3/s3.prot b/tests/fpga-debugging/axis-adapter-s3/s3.prot index bdee8733..04742380 100644 --- a/tests/fpga-debugging/axis-adapter-s3/s3.prot +++ b/tests/fpga-debugging/axis-adapter-s3/s3.prot @@ -118,189 +118,228 @@ prot split_word(data: u64, keep: u8, is_final_word_in_packet: u1) { // Environment is now ready to accept the output data emitted by the DUT DUT.output_axis_tready := 1'b1; - // Wait until the DUT indicates that the next byte is valid for emitting + // Wait until the DUT indicates that there is valid data to emit while (!(DUT.output_axis_tvalid == 1'b1)) { step(); } - + // Both ready & valid are now 1 in the output direction, + // so the DUT can begin to emit the 0th byte + // 0th (rightmost) bit of `keep` is the current value of `tkeep` assert_eq(DUT.output_axis_tkeep, keep[0]); // Rightmost 8 bits of `data` are now on the `output_tdata` pin assert_eq(DUT.output_axis_tdata, data[7:0]); - // If the 0th byte was not the final byte in an entire packet - // (note: it could still be the last byte in the data word, but - // AXI-S) - if (DUT.output_axis_tlast == 1'b0) { - // Then the 1st byte (the next byte) must be kept, - // i.e. its `tkeep` bit must be 1 - assert_eq(keep[1], 1'b1); - // One clock cycle to emit the 0th byte - step(); + // Check if the 0th byte is meaningful + if (DUT.output_axis_tkeep == 1'b1) { + // Check if it is the end of a packet + if (DUT.output_axis_tlast == 1'b1) { + // 0th byte is meaningful & also the end of a packet, so the 1st byte shouldn't be kept + assert_eq(keep[1], 1'b0); + // One clock cycle to emit the 0th byte + step(); + } else { + // 0th byte is meaningful but not the end of a packet, so the 1st byte should also be kept + assert_eq(keep[1], 1'b1); - // Wait until the DUT indicates that the next byte is valid for emitting - while (!(DUT.output_axis_tvalid == 1'b1)) { - step(); - } - // DUT provides the next byte of data and its `tkeep` bit on the output pins - assert_eq(DUT.output_axis_tdata, data[15:8]); - assert_eq(DUT.output_axis_tkeep, keep[1]); - - // If the 1st byte is not the final byte in the entire packet - if (DUT.output_axis_tlast == 1'b0) { - // then the 2nd byte must be kept, i.e. its `tkeep` bit must be 1 - assert_eq(keep[2], 1'b1); - // One clock cycle to emit the 1st byte + // One clock cycle to emit the 0th byte step(); // Wait until the DUT indicates that the next byte is valid for emitting while (!(DUT.output_axis_tvalid == 1'b1)) { step(); } - // DUT provides the next byte of data and its `tkeep` bit on the output pins - assert_eq(DUT.output_axis_tdata, data[23:16]); - assert_eq(DUT.output_axis_tkeep, keep[2]); - - // If the 2nd byte isn't the final byte in a packet - if (DUT.output_axis_tlast == 1'b0) { - // Then the 3rd byte must be kept, i.e. its `tkeep` bit is 1 - assert_eq(keep[3], 1'b1); - // One clock cycle to emit the 2nd byte - step(); - // Wait until the DUT indicates that the next byte is valid for emitting - while (!(DUT.output_axis_tvalid == 1'b1)) { + // DUT provides the next byte of data and its `tkeep` on its output pins + assert_eq(DUT.output_axis_tkeep, keep[1]); + assert_eq(DUT.output_axis_tdata, data[15:8]); + + // Check if the 1st byte is meaningful + if (DUT.output_axis_tkeep == 1'b1) { + // Check if it's the end of a packet + if (DUT.output_axis_tlast == 1'b1) { + // 1st byte is meaningful & also the end of a packet, so the 2nd byte shouldn't be kept + assert_eq(keep[2], 1'b0); + // One clock cycle to emit the 1st byte step(); - } - // DUT provides the next byte of data and its `tkeep` bit on the output pins - assert_eq(DUT.output_axis_tdata, data[31:24]); - assert_eq(DUT.output_axis_tkeep, keep[3]); - - // If the 3rd byte isn't the final byte in a packet - if (DUT.output_axis_tlast == 1'b0) { - // Then the 4th byte must be kept - assert_eq(keep[4], 1'b1); - // One clock cycle to emit the 3rd byte + } else { + // 1st byte is meaningful but not the end of a packet, so the 2nd byte should also be kept + assert_eq(keep[2], 1'b1); + + // One clock cycle to emit the 1st byte step(); - // Wait until the DUT indicates that the next byte is valid for emitting + // Wait till DUT has valid data to emit while (!(DUT.output_axis_tvalid == 1'b1)) { step(); } - // DUT provides the next byte of data and its `tkeep` bit on the output pins - assert_eq(DUT.output_axis_tdata, data[39:32]); - assert_eq(DUT.output_axis_tkeep, keep[4]); - - // If the 4th byte wasn't the last byte of a packet - if (DUT.output_axis_tlast == 1'b0) { - // The 5th byte must be kept - assert_eq(keep[5], 1'b1); - // One clock cycle to emit the 4th byte - step(); + + // DUT provides the next byte of data and its `tkeep` on its output pins + assert_eq(DUT.output_axis_tkeep, keep[2]); + assert_eq(DUT.output_axis_tdata, data[23:16]); - // Wait until DUT has valid data to emit - while (!(DUT.output_axis_tvalid == 1'b1)) { - step(); - } - // DUT provides the next byte of data and its `tkeep` on its output pins - assert_eq(DUT.output_axis_tdata, data[47:40]); - assert_eq(DUT.output_axis_tkeep, keep[5]); - - // If the 5th byte wasn't the last byte of a packet - if (DUT.output_axis_tlast == 1'b0) { - // The 6th byte must be kept - assert_eq(keep[6], 1'b1); - // One clock cycle to emit the 5th byte + // Check if the 2nd byte is meaningful + if (DUT.output_axis_tkeep == 1'b1) { + // Check if the 2nd byte is the end of a packet + if (DUT.output_axis_tlast == 1'b1) { + // 2nd byte is meaningful & also the end of a packet, so the 3rd byte shouldn't be kept + assert_eq(keep[3], 1'b0); + // One clock cycle to emit the 2nd byte step(); + } else { + // 2nd byte is meaningful but not the end of a packet, so the 3rd byte should also be kept + assert_eq(keep[3], 1'b1); - // Wait until DUT has valid data to emit + // One clock cycle to emit the 2nd byte + step(); + // Wait till DUT has valid data to emit while (!(DUT.output_axis_tvalid == 1'b1)) { step(); } - // DUT provides the next byte of data and its `tkeep` on its output pins - assert_eq(DUT.output_axis_tdata, data[55:48]); - assert_eq(DUT.output_axis_tkeep, keep[6]); - - // If the 6th byte wasn't the last byte of a packet - if (DUT.output_axis_tlast == 1'b0) { - // The 7th byte must be kept - assert_eq(keep[7], 1'b1); - // One clock cycle to emit the 6th byte - step(); + // DUT provides the final byte of data and its `tkeep` on its output pins + assert_eq(DUT.output_axis_tkeep, keep[3]); + assert_eq(DUT.output_axis_tdata, data[31:24]); - // Wait until DUT has valid data to emit - while (!(DUT.output_axis_tvalid == 1'b1)) { + // Check if the 3rd byte is meaningful + if (DUT.output_axis_tkeep == 1'b1) { + // Check if the 3rd byte is the end of a packet + if (DUT.output_axis_tlast == 1'b1) { + // 3rd byte is meaningful & also the end of the packet, so the 4th byte shouldn't be kept + assert_eq(keep[4], 1'b0); + // One clock cycle to emit the 3rd byte step(); - } - // DUT provides the final byte of data and its `tkeep` on its output pins - assert_eq(DUT.output_axis_tdata, data[63:56]); - assert_eq(DUT.output_axis_tkeep, keep[7]); - - // The 7th byte is the last byte for a 64-bit word, - // so we don't need to inspect the `tkeep` bit for the "next" byte - // We only need to check whether this byte is the end of the - // of the entire packet, which is determined by the `is_final_word_in_packet` parameter - assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); + } else { + // 3rd byte is meaningful but not the end of a packet, so the 4th byte should also be kept + assert_eq(keep[4], 1'b1); - // One clock cycle to emit the 7th byte - step(); - } else { - // 6th byte was the last byte of a packet - // If the 6th byte is also kept, then the 7th byte must not be kept - if (DUT.output_axis_tkeep == 1'b1) { - assert_eq(keep[7], 1'b0); + // One clock cycle to emit the 3rd byte + step(); + + // Wait till DUT has valid data to emit + while (!(DUT.output_axis_tvalid == 1'b1)) { + step(); + } + // DUT provides the final byte of data and its `tkeep` on its output pins + assert_eq(DUT.output_axis_tkeep, keep[4]); + assert_eq(DUT.output_axis_tdata, data[39:32]); + + // Check if the 4th byte is meaningful + if (DUT.output_axis_tkeep == 1'b1) { + // Check if the 4th byte is the end of a packet + if (DUT.output_axis_tlast == 1'b1) { + // 4th byte is meaningful and also the end of a packet, so the 5th byte shouldn't be kept + assert_eq(keep[5], 1'b0); + // One clock cycle to emit the 4th byte + step(); + } else { + // 4th byte is meaningful but not the end of a packet, so the 5th byte should also be kept + assert_eq(keep[5], 1'b1); + + // One clock cycle to emit the 5th byte + step(); + + // Wait until DUT has valid data to emit + while (!(DUT.output_axis_tvalid == 1'b1)) { + step(); + } + // DUT provides the final byte of data and its `tkeep` on its output pins + assert_eq(DUT.output_axis_tkeep, keep[5]); + assert_eq(DUT.output_axis_tdata, data[47:40]); + + // Check if the 5th byte is meaningful + if (DUT.output_axis_tkeep == 1'b1) { + // Check if the 5th byte is the end of a packet + if (DUT.output_axis_tlast == 1'b1) { + // 5th byte is meaningful and also the end of a packet, so the 6th byte shouldn't be kept + assert_eq(keep[6], 1'b0); + // One clock cycle to emit the 5th byte + step(); + } else { + // 5th byte is meaningful but not the end of a packet, so the 6th byte should also be kept + assert_eq(keep[6], 1'b1); + + // One clock cycle to emit the 5th byte + step(); + + // Wait until DUT has valid data to emit + while (!(DUT.output_axis_tvalid == 1'b1)) { + step(); + } + // DUT provides the final byte of data and its `tkeep` on its output pins + assert_eq(DUT.output_axis_tkeep, keep[6]); + assert_eq(DUT.output_axis_tdata, data[55:48]); + + // Check if the 6th byte is meaningful + if (DUT.output_axis_tkeep == 1'b1) { + if (DUT.output_axis_tlast == 1'b1) { + // 6th byte is meaningful and also the end of a packet, so the 7th byte shouldn't be kept + assert_eq(keep[7], 1'b0); + // One clock cycle to emit the 6th byte + step(); + } else { + // 6th byte is meaningful but not the end of a packet, so the 7th byte should also be kept + assert_eq(keep[7], 1'b1); + + // One clock cycle to emit the 6th byte + step(); + + // Wait until DUT has valid data to emit + while (!(DUT.output_axis_tvalid == 1'b1)) { + step(); + } + // DUT provides the final byte of data and its `tkeep` on its output pins + assert_eq(DUT.output_axis_tkeep, keep[7]); + assert_eq(DUT.output_axis_tdata, data[63:56]); + + // The 7th byte is the last byte for a 64-bit word, + // so we don't need to inspect the `tkeep` bit for the "next" byte + // We only need to check whether this byte is the end of the + // of the entire packet, which is determined by the `is_final_word_in_packet` parameter + assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); + + // One clock cycle to emit the 7th and final byte + step(); + } + } else { + // 6th byte isn't meaningful (tkeep = 0), so the DUT stops emitting bytes from this point onwards + assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); + step(); + } + } + } else { + // 5th byte isn't meaningful (tkeep = 0), so the DUT stops emitting bytes from this point onwards + assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); + step(); + } + } + } else { + // 4th byte isn't meaningful (tkeep = 0), so the DUT stops emitting bytes from this point onwards + assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); + step(); + } } - step(); - } - } else { - // 5th byte was the last byte of a packet - // If the 5th byte is also kept, then the 6th byte must not be kept - if (DUT.output_axis_tkeep == 1'b1) { - assert_eq(keep[6], 1'b0); + } else { + // 3rd byte isn't meaningful, so the DUT stops emitting bytes from this point onwards + assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); + step(); } - step(); } } else { - // 4th byte was the last byte in a packet - // If the 4th byte is also kept, then the 5th byte must not be kept - if (DUT.output_axis_tkeep == 1'b1) { - assert_eq(keep[5], 1'b0); - } + // 2nd byte isn't meaningful (tkeep = 0), so the DUT stops emitting bytes from this point onwards + assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); step(); } - } else { - // 3rd byte was the last byte in an entire packet - // If the 3rd byte is kept as well, then the 4th byte must not be kept (its `tkeep` bit must be 0) - if (DUT.output_axis_tkeep == 1'b1) { - assert_eq(keep[4], 1'b0); - } - step(); } - } else { - // 2nd byte was the last byte in an entire packet - // If the 2nd byte is kept as well, then the 3rd-byte's `tkeep` must be 0 (i.e. 3rd byte is not kept) - if (DUT.output_axis_tkeep == 1'b1) { - assert_eq(keep[3], 1'b0); - } + // 1st byte isn't meaningful (tkeep = 0) the DUT stops emitting bytes from this point onwards + assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); step(); - } - } else { - // 1st byte was the last byte in an entire packet - // If the 1st byte is kept as well, then the 2nd-byte's `tkeep` bit must be 0 (i.e. 2nd byte is not kept) - if (DUT.output_axis_tkeep == 1'b1) { - assert_eq(keep[2], 1'b0); - } - step(); + } } } else { - // 0th byte was the last byte of the last word of a packet, i.e. `output_axis_tlast == 1` - // If the 0th byte is kept as well (i.e. `tkeep = 1`), - // then we know the next byte's corresponding `tkeep` must be 0 (i.e. is not kept) - if (DUT.output_axis_tkeep == 1'b1) { - assert_eq(keep[1], 1'b0); - } + // 0th byte isn't meaningful (tkeep = 0), so the DUT stops emitting bytes from this point onwards + assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); step(); } } \ No newline at end of file From 459420095ffa8095d97c1e47a1bd50ac03154c78 Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Tue, 25 Aug 2026 21:43:14 -0400 Subject: [PATCH 18/29] Add alternate version of protocol that branches on the parameter keep --- .../axis-adapter-s3/s3_new.prot | 303 ++++++++++++++++++ 1 file changed, 303 insertions(+) create mode 100644 tests/fpga-debugging/axis-adapter-s3/s3_new.prot diff --git a/tests/fpga-debugging/axis-adapter-s3/s3_new.prot b/tests/fpga-debugging/axis-adapter-s3/s3_new.prot new file mode 100644 index 00000000..eb43a95b --- /dev/null +++ b/tests/fpga-debugging/axis-adapter-s3/s3_new.prot @@ -0,0 +1,303 @@ +// This file describes an AXI-Stream width adapter which +// converts a 64-bit input into 8-bit output chunks over multiple cycles + +// Notes: +// - The DUT has 3 termination conditions: +// - 1. All 8 bytes have been emitted (in the fixed DUT, this only happens when `tkeep = 11111111`, i.e. all bytes of `tdata` are meaningful) +// - 2. When emitting the i-th byte, the DUT sees that `tkeep[i] = 0`, in which case it treats the i-th byte as the last one and stops emitting any further bytes +// - 3. For the fixed DUT only, if `tkeep[i] = 1` but `tkeep[i+1] = 0`, then the DUT treats the `i`-th byte as the last one +// and stops emitting any further bytes (the fixed DUT gains this "lookahead" logic) +// - The `tlast` parameter indicates if the data word corresponds to the final word of a packet +// (Note: there can be multiple words in a packet. Moreover, the last byte of a non-final word in a packet +// still gets `tlast = 0`, since it is not the last word of a packet.) +// - AXI-Stream spec says that for "downsizing" operations in which data with larger bit-widths +// are converted to smaller bitwidths (section 2.3.3), which this DUT is doing, +// if the input data word happens to be the last word of a packet (i.e. `tlast = 1` for the input), +// in the output sequence of bytes, `tlast` can only be asserted for the last byte emitted +// - The DUT cannot accept a new 64-bit input when it is still emitting the bytes of the existing data +// - The DUT examines `tkeep` from right to left, i.e. the 0th byte emitted +// corresponds to `tdata[7:0]` and `tkeep[0]` (the LSB of `tkeep`) +// - The fixed waveform has `tkeep = 0001 1111`, so only 5 bytes are emitted and the +// waveform ends after the 5 bytes are emitted +// - The `output_bytes` parameter to the `send_word` protocol below contains +// the bytes in the order they're emitted, and since the DUT examines `tdata` right to left, +// this means if `tdata = 0xABCD`, the output bytes are `[0xCD, 0xAB]` +// (i.e. the bytes corresponding to less significant bits are emitted first) + +struct AXIS { + // Reset is active-high + in rst: u1, + + // Signals related to the DUT accepting input data from the environment + + // 64-bit data that the DUT accepts as input from the environment + in input_axis_tdata: u64, + + // bitmask indicating which bytes of `tdata` are meaningful + in input_axis_tkeep: u8, + + // 1 if this is the last word in a packet + in input_axis_tlast: u1, + + // Indicates if `input_tdata` contains valid data + in input_axis_tvalid: u1, + + // Signal indicating whether the DUT + // is ready to accept data from the environment as input + out input_axis_tready: u1, + + //---------------------------------------------------------------- + // Signals related to the DUT emitting data as output + + // 8-bit data that the DUT emits as output + out output_axis_tdata: u8, + + // Output data is 8 bits, so `tkeep` is now just 1 bit wide + // `tkeep` is 1 if `output_tdata` contains meaningful data + out output_axis_tkeep: u1, + + // 1 if this is the last word in a packet + out output_axis_tlast: u1, + + // Indicates if `output_data` contains valid data + out output_axis_tvalid: u1, + + // Signal indicating whether the environment is ready to + // accept the data emitted by the DUT as output + in output_axis_tready: u1, +} + +prot reset() { + DUT.rst := 1'b1; + + // Valid pin (for both directions) must be low when + // reset is asserted (AXI-Stream spec section 2.7.2) + DUT.input_axis_tvalid := 1'b0; + assert_eq(DUT.output_axis_tvalid, 1'b0); + + step(); +} + +// When idle, the DUT neither accepts data from the environment, +// nor does it emit data as output +#[idle] +prot idle() { + DUT.rst := 1'b0; + DUT.input_axis_tvalid := 1'b0; + + assert_eq(DUT.output_axis_tvalid, 1'b0); + step(); +} + +// Note: the `split_word` protocol below is a variant of the one in `s3.prot`, +// except it branches on `keep[i]`, where `keep` is a parameter to the protocol +// (Branching on parameters is currently not permitted in our DSL) + +// - `is_final_word_in_packet` is a parameter that represents `tlast` +// (this variable name was chosen to be more informative and to avoid confusion with our DSL's `is_last()` construct) +prot split_word(data: u64, keep: u8, is_final_word_in_packet: u1) { + DUT.rst := 1'b0; + DUT.input_axis_tdata := data; + DUT.input_axis_tkeep := keep; + DUT.input_axis_tlast := is_final_word_in_packet; + + // There is valid data (namely the input word), so set `valid = 1` + DUT.input_axis_tvalid := 1'b1; + + // Wait until the DUT signals it is ready to accept to the input word + while (!(DUT.input_axis_tready == 1'b1)) { + step(); + } + // One cycle for DUT to accept input data from environment + step(); + + // DUT has accepted input data, so we set the input pins to DontCare + DUT.input_axis_tdata := X; + DUT.input_axis_tkeep := X; + DUT.input_axis_tlast := X; + + // Since input pins are DontCare, there is no longer valid data, so set `valid = 0` + DUT.input_axis_tvalid := 1'b0; + + // Environment is now ready to accept the output data emitted by the DUT + DUT.output_axis_tready := 1'b1; + + // Wait until the DUT indicates that there is valid data to emit + while (!(DUT.output_axis_tvalid == 1'b1)) { + step(); + } + // Both ready & valid are now 1 in the output direction, + // so the DUT can begin to emit the 0th byte + + // Rightmost 8 bits of `data` are now on the `output_tdata` pin + assert_eq(DUT.output_axis_tdata, data[7:0]); + + // Check if 0th byte is meaningful + if (keep[0] == 1'b1) { + // keep[0] = 1, so the output tkeep must also be 1 + assert_eq(DUT.output_axis_tkeep, 1'b1); + + // Lookahead and check if 1st byte is also meaningful + if (keep[1] == 1'b1) { + // 1st byte is meaningful, so the 0th byte can't be the end of the packet, + // so output tlast must be 0 for the 0th byte + assert_eq(DUT.output_axis_tlast, 1'b0); + + // One clock cycle to emit the 0th byte + step(); + + // Wait till DUT has valid data to emit for the 1st byte + while (!(DUT.output_axis_tvalid == 1'b1)) { + step(); + } + + assert_eq(DUT.output_axis_tdata, data[15:8]); + + // We've already established above that keep[1] = 1, so output tkeep must be 1 for the 1st byte + assert_eq(DUT.output_axis_tkeep, 1'b1); + + // Lookahead and check if 2nd byte is meaningful + if (keep[2] == 1'b1) { + // 2nd byte is meaningful, so the 1st byte can't be the end of the packet, + // so output tlast must be 0 for the 1st byte + assert_eq(DUT.output_axis_tlast, 1'b0); + + // One clock cycle to emit the 1st byte + step(); + + while (!(DUT.output_axis_tvalid == 1'b1)) { + step(); + } + assert_eq(DUT.output_axis_tdata, data[23:16]); + + // We've already established above that keep[2] = 1, so output tkeep must be 1 for the 2nd byte + assert_eq(DUT.output_axis_tkeep, 1'b1); + + // Check if 3rd byte is meaningful + if (keep[3] == 1'b1) { + // 3rd byte is meaningful, so the 2nd byte can't be the end of the packet, + // so output tlast must be 0 for the 2nd byte + assert_eq(DUT.output_axis_tlast, 1'b0); + + // One clock cycle to emit the 2nd byte + step(); + + while (!(DUT.output_axis_tvalid == 1'b1)) { + step(); + } + assert_eq(DUT.output_axis_tdata, data[31:24]); + + // We've already established above that keep[3] = 1, so output tkeep must be 1 for the 3rd byte + assert_eq(DUT.output_axis_tkeep, 1'b1); + + if (keep[4] == 1'b1) { + // 4th byte is meaningful, so output tlast must be 0 for the 3rd byte + assert_eq(DUT.output_axis_tlast, 1'b0); + + step(); + + while (!(DUT.output_axis_tvalid == 1'b1)) { + step(); + } + + assert_eq(DUT.output_axis_tdata, data[39:32]); + + // We've already established above that keep[4] = 1, so output tkeep must be 1 for the 4th byte + assert_eq(DUT.output_axis_tkeep, 1'b1); + + if (keep[5] == 1'b1) { + // 5th byte is meaningful, so output tlast must be 0 for the 4th byte + assert_eq(DUT.output_axis_tlast, 1'b0); + + step(); + + while (!(DUT.output_axis_tvalid == 1'b1)) { + step(); + } + assert_eq(DUT.output_axis_tdata, data[47:40]); + + // We've already established above that keep[5] = 1, so output tkeep must be 1 for the 5th byte + assert_eq(DUT.output_axis_tkeep, 1'b1); + + if (keep[6] == 1'b1) { + // 6th byte is meaningful, so output tlast must be 0 for the 5th byte + assert_eq(DUT.output_axis_tlast, 1'b0); + + step(); + + while (!(DUT.output_axis_tvalid == 1'b1)) { + step(); + } + assert_eq(DUT.output_axis_tdata, data[55:48]); + + // We've already established above that keep[6] = 1, so output tkeep must be 1 for the 6th byte + assert_eq(DUT.output_axis_tkeep, 1'b1); + + if (keep[7] == 1'b1) { + // 7th byte is meaningful, so output tlast must be 0 for the 6th byte + assert_eq(DUT.output_axis_tlast, 1'b0); + + step(); + + while (!(DUT.output_axis_tvalid == 1'b1)) { + step(); + } + assert_eq(DUT.output_axis_tdata, data[63:56]); + + // We've already established above that keep[7] = 1, so output tkeep must be 1 for the 7th byte + assert_eq(DUT.output_axis_tkeep, 1'b1); + + // The 7th byte is the last byte for a 64-bit word, + // so we don't need to inspect the `tkeep` bit for the "next" byte + // We only need to check whether this byte is the end of the + // of the entire packet, which is determined by the `is_final_word_in_packet` parameter + assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); + + // One clock cycle to emit the 7th and final byte + step(); + } else { + // keep[6] = 1, keep[7] = 0 + assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); + step(); + } + } else { + // keep[5] = 1, keep[6] = 0 + assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); + step(); + } + } else { + // keep[4] = 1, keep[5] = 0 + assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); + step(); + } + } else { + // Here we have keep[3] = 1, keep[4] = 0 + // so the 3rd byte is the last byte emitted by the DUT + assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); + step(); + } + } else { + // Here we have keep[2] = 1 and keep[3] = 0, + // so the 2nd byte is the last byte emitted by the DUT + assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); + step(); + } + } else { + // Here we have keep[1] = 1 and keep[2] = 0, + // so the 1st byte is the last byte emitted by the DUT + assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); + step(); + } + } else { + // Here we have keep[0] = 1 and keep[1] = 0, + // so the 0th byte is the last byte emitted by the DUT + assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); + step(); + } + } else { + // keep[0] = 0, so output tkeep must also be 0 and no meaningful bytes are emitted + assert_eq(DUT.output_axis_tkeep, 1'b0); + assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); + step(); + } +} From 05abbc4611282fc3b775716cbba8b6ae38d329f6 Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Wed, 26 Aug 2026 16:51:53 -0400 Subject: [PATCH 19/29] Add --allow-branch-on-arg to s3 test cases --- scripts/test_catalog.py | 2 ++ 1 file changed, 2 insertions(+) diff --git a/scripts/test_catalog.py b/scripts/test_catalog.py index da099188..2171458d 100644 --- a/scripts/test_catalog.py +++ b/scripts/test_catalog.py @@ -717,6 +717,7 @@ "--time-unit", "ns", "--display-hex", + "--allow-branch-on-arg", ), }, "tests.fpga-debugging.axis-adapter-s3.s3_fixed": { @@ -732,6 +733,7 @@ "--time-unit", "ns", "--display-hex", + "--allow-branch-on-arg", ), }, "tests.fpga-debugging.axis-async-fifo-c4.c4_buggy": { From 1526f7d7eb437144c2036a2048a6a673b3af9b0e Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Wed, 26 Aug 2026 16:52:11 -0400 Subject: [PATCH 20/29] propagate contents of s3_new.prot to s3.prot --- tests/fpga-debugging/axis-adapter-s3/s3.prot | 294 ++++++++----------- 1 file changed, 124 insertions(+), 170 deletions(-) diff --git a/tests/fpga-debugging/axis-adapter-s3/s3.prot b/tests/fpga-debugging/axis-adapter-s3/s3.prot index 04742380..060f81c1 100644 --- a/tests/fpga-debugging/axis-adapter-s3/s3.prot +++ b/tests/fpga-debugging/axis-adapter-s3/s3.prot @@ -125,221 +125,175 @@ prot split_word(data: u64, keep: u8, is_final_word_in_packet: u1) { // Both ready & valid are now 1 in the output direction, // so the DUT can begin to emit the 0th byte - // 0th (rightmost) bit of `keep` is the current value of `tkeep` - assert_eq(DUT.output_axis_tkeep, keep[0]); - // Rightmost 8 bits of `data` are now on the `output_tdata` pin assert_eq(DUT.output_axis_tdata, data[7:0]); - // Check if the 0th byte is meaningful - if (DUT.output_axis_tkeep == 1'b1) { - // Check if it is the end of a packet - if (DUT.output_axis_tlast == 1'b1) { - // 0th byte is meaningful & also the end of a packet, so the 1st byte shouldn't be kept - assert_eq(keep[1], 1'b0); - // One clock cycle to emit the 0th byte - step(); - } else { - // 0th byte is meaningful but not the end of a packet, so the 1st byte should also be kept - assert_eq(keep[1], 1'b1); + // Check if 0th byte is meaningful + if (keep[0] == 1'b1) { + // keep[0] = 1, so the output tkeep must also be 1 + assert_eq(DUT.output_axis_tkeep, 1'b1); + + // Lookahead and check if 1st byte is also meaningful + if (keep[1] == 1'b1) { + // 1st byte is meaningful, so the 0th byte can't be the end of the packet, + // so output tlast must be 0 for the 0th byte + assert_eq(DUT.output_axis_tlast, 1'b0); // One clock cycle to emit the 0th byte step(); - // Wait until the DUT indicates that the next byte is valid for emitting + // Wait till DUT has valid data to emit for the 1st byte while (!(DUT.output_axis_tvalid == 1'b1)) { step(); } - // DUT provides the next byte of data and its `tkeep` on its output pins - assert_eq(DUT.output_axis_tkeep, keep[1]); assert_eq(DUT.output_axis_tdata, data[15:8]); - // Check if the 1st byte is meaningful - if (DUT.output_axis_tkeep == 1'b1) { - // Check if it's the end of a packet - if (DUT.output_axis_tlast == 1'b1) { - // 1st byte is meaningful & also the end of a packet, so the 2nd byte shouldn't be kept - assert_eq(keep[2], 1'b0); - // One clock cycle to emit the 1st byte - step(); - } else { - // 1st byte is meaningful but not the end of a packet, so the 2nd byte should also be kept - assert_eq(keep[2], 1'b1); + // We've already established above that keep[1] = 1, so output tkeep must be 1 for the 1st byte + assert_eq(DUT.output_axis_tkeep, 1'b1); - // One clock cycle to emit the 1st byte + // Lookahead and check if 2nd byte is meaningful + if (keep[2] == 1'b1) { + // 2nd byte is meaningful, so the 1st byte can't be the end of the packet, + // so output tlast must be 0 for the 1st byte + assert_eq(DUT.output_axis_tlast, 1'b0); + + // One clock cycle to emit the 1st byte + step(); + + while (!(DUT.output_axis_tvalid == 1'b1)) { step(); + } + assert_eq(DUT.output_axis_tdata, data[23:16]); + + // We've already established above that keep[2] = 1, so output tkeep must be 1 for the 2nd byte + assert_eq(DUT.output_axis_tkeep, 1'b1); - // Wait till DUT has valid data to emit + // Check if 3rd byte is meaningful + if (keep[3] == 1'b1) { + // 3rd byte is meaningful, so the 2nd byte can't be the end of the packet, + // so output tlast must be 0 for the 2nd byte + assert_eq(DUT.output_axis_tlast, 1'b0); + + // One clock cycle to emit the 2nd byte + step(); + while (!(DUT.output_axis_tvalid == 1'b1)) { step(); } - - // DUT provides the next byte of data and its `tkeep` on its output pins - assert_eq(DUT.output_axis_tkeep, keep[2]); - assert_eq(DUT.output_axis_tdata, data[23:16]); - - // Check if the 2nd byte is meaningful - if (DUT.output_axis_tkeep == 1'b1) { - // Check if the 2nd byte is the end of a packet - if (DUT.output_axis_tlast == 1'b1) { - // 2nd byte is meaningful & also the end of a packet, so the 3rd byte shouldn't be kept - assert_eq(keep[3], 1'b0); - // One clock cycle to emit the 2nd byte + assert_eq(DUT.output_axis_tdata, data[31:24]); + + // We've already established above that keep[3] = 1, so output tkeep must be 1 for the 3rd byte + assert_eq(DUT.output_axis_tkeep, 1'b1); + + if (keep[4] == 1'b1) { + // 4th byte is meaningful, so output tlast must be 0 for the 3rd byte + assert_eq(DUT.output_axis_tlast, 1'b0); + + step(); + + while (!(DUT.output_axis_tvalid == 1'b1)) { step(); - } else { - // 2nd byte is meaningful but not the end of a packet, so the 3rd byte should also be kept - assert_eq(keep[3], 1'b1); + } + + assert_eq(DUT.output_axis_tdata, data[39:32]); + + // We've already established above that keep[4] = 1, so output tkeep must be 1 for the 4th byte + assert_eq(DUT.output_axis_tkeep, 1'b1); + + if (keep[5] == 1'b1) { + // 5th byte is meaningful, so output tlast must be 0 for the 4th byte + assert_eq(DUT.output_axis_tlast, 1'b0); - // One clock cycle to emit the 2nd byte step(); - // Wait till DUT has valid data to emit + while (!(DUT.output_axis_tvalid == 1'b1)) { step(); } - // DUT provides the final byte of data and its `tkeep` on its output pins - assert_eq(DUT.output_axis_tkeep, keep[3]); - assert_eq(DUT.output_axis_tdata, data[31:24]); - - // Check if the 3rd byte is meaningful - if (DUT.output_axis_tkeep == 1'b1) { - // Check if the 3rd byte is the end of a packet - if (DUT.output_axis_tlast == 1'b1) { - // 3rd byte is meaningful & also the end of the packet, so the 4th byte shouldn't be kept - assert_eq(keep[4], 1'b0); - // One clock cycle to emit the 3rd byte + assert_eq(DUT.output_axis_tdata, data[47:40]); + + // We've already established above that keep[5] = 1, so output tkeep must be 1 for the 5th byte + assert_eq(DUT.output_axis_tkeep, 1'b1); + + if (keep[6] == 1'b1) { + // 6th byte is meaningful, so output tlast must be 0 for the 5th byte + assert_eq(DUT.output_axis_tlast, 1'b0); + + step(); + + while (!(DUT.output_axis_tvalid == 1'b1)) { step(); - } else { - // 3rd byte is meaningful but not the end of a packet, so the 4th byte should also be kept - assert_eq(keep[4], 1'b1); + } + assert_eq(DUT.output_axis_tdata, data[55:48]); + + // We've already established above that keep[6] = 1, so output tkeep must be 1 for the 6th byte + assert_eq(DUT.output_axis_tkeep, 1'b1); + + if (keep[7] == 1'b1) { + // 7th byte is meaningful, so output tlast must be 0 for the 6th byte + assert_eq(DUT.output_axis_tlast, 1'b0); - // One clock cycle to emit the 3rd byte step(); - // Wait till DUT has valid data to emit while (!(DUT.output_axis_tvalid == 1'b1)) { step(); - } - // DUT provides the final byte of data and its `tkeep` on its output pins - assert_eq(DUT.output_axis_tkeep, keep[4]); - assert_eq(DUT.output_axis_tdata, data[39:32]); - - // Check if the 4th byte is meaningful - if (DUT.output_axis_tkeep == 1'b1) { - // Check if the 4th byte is the end of a packet - if (DUT.output_axis_tlast == 1'b1) { - // 4th byte is meaningful and also the end of a packet, so the 5th byte shouldn't be kept - assert_eq(keep[5], 1'b0); - // One clock cycle to emit the 4th byte - step(); - } else { - // 4th byte is meaningful but not the end of a packet, so the 5th byte should also be kept - assert_eq(keep[5], 1'b1); - - // One clock cycle to emit the 5th byte - step(); - - // Wait until DUT has valid data to emit - while (!(DUT.output_axis_tvalid == 1'b1)) { - step(); - } - // DUT provides the final byte of data and its `tkeep` on its output pins - assert_eq(DUT.output_axis_tkeep, keep[5]); - assert_eq(DUT.output_axis_tdata, data[47:40]); - - // Check if the 5th byte is meaningful - if (DUT.output_axis_tkeep == 1'b1) { - // Check if the 5th byte is the end of a packet - if (DUT.output_axis_tlast == 1'b1) { - // 5th byte is meaningful and also the end of a packet, so the 6th byte shouldn't be kept - assert_eq(keep[6], 1'b0); - // One clock cycle to emit the 5th byte - step(); - } else { - // 5th byte is meaningful but not the end of a packet, so the 6th byte should also be kept - assert_eq(keep[6], 1'b1); - - // One clock cycle to emit the 5th byte - step(); - - // Wait until DUT has valid data to emit - while (!(DUT.output_axis_tvalid == 1'b1)) { - step(); - } - // DUT provides the final byte of data and its `tkeep` on its output pins - assert_eq(DUT.output_axis_tkeep, keep[6]); - assert_eq(DUT.output_axis_tdata, data[55:48]); - - // Check if the 6th byte is meaningful - if (DUT.output_axis_tkeep == 1'b1) { - if (DUT.output_axis_tlast == 1'b1) { - // 6th byte is meaningful and also the end of a packet, so the 7th byte shouldn't be kept - assert_eq(keep[7], 1'b0); - // One clock cycle to emit the 6th byte - step(); - } else { - // 6th byte is meaningful but not the end of a packet, so the 7th byte should also be kept - assert_eq(keep[7], 1'b1); - - // One clock cycle to emit the 6th byte - step(); - - // Wait until DUT has valid data to emit - while (!(DUT.output_axis_tvalid == 1'b1)) { - step(); - } - // DUT provides the final byte of data and its `tkeep` on its output pins - assert_eq(DUT.output_axis_tkeep, keep[7]); - assert_eq(DUT.output_axis_tdata, data[63:56]); - - // The 7th byte is the last byte for a 64-bit word, - // so we don't need to inspect the `tkeep` bit for the "next" byte - // We only need to check whether this byte is the end of the - // of the entire packet, which is determined by the `is_final_word_in_packet` parameter - assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); - - // One clock cycle to emit the 7th and final byte - step(); - } - } else { - // 6th byte isn't meaningful (tkeep = 0), so the DUT stops emitting bytes from this point onwards - assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); - step(); - } - } - } else { - // 5th byte isn't meaningful (tkeep = 0), so the DUT stops emitting bytes from this point onwards - assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); - step(); - } - } - } else { - // 4th byte isn't meaningful (tkeep = 0), so the DUT stops emitting bytes from this point onwards - assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); - step(); - } + } + assert_eq(DUT.output_axis_tdata, data[63:56]); + + // We've already established above that keep[7] = 1, so output tkeep must be 1 for the 7th byte + assert_eq(DUT.output_axis_tkeep, 1'b1); + + // The 7th byte is the last byte for a 64-bit word, + // so we don't need to inspect the `tkeep` bit for the "next" byte + // We only need to check whether this byte is the end of the + // of the entire packet, which is determined by the `is_final_word_in_packet` parameter + assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); + + // One clock cycle to emit the 7th and final byte + step(); + } else { + // keep[6] = 1, keep[7] = 0 + assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); + step(); } } else { - // 3rd byte isn't meaningful, so the DUT stops emitting bytes from this point onwards + // keep[5] = 1, keep[6] = 0 assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); - step(); + step(); } + } else { + // keep[4] = 1, keep[5] = 0 + assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); + step(); } } else { - // 2nd byte isn't meaningful (tkeep = 0), so the DUT stops emitting bytes from this point onwards + // Here we have keep[3] = 1, keep[4] = 0 + // so the 3rd byte is the last byte emitted by the DUT assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); step(); } + } else { + // Here we have keep[2] = 1 and keep[3] = 0, + // so the 2nd byte is the last byte emitted by the DUT + assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); + step(); } } else { - // 1st byte isn't meaningful (tkeep = 0) the DUT stops emitting bytes from this point onwards + // Here we have keep[1] = 1 and keep[2] = 0, + // so the 1st byte is the last byte emitted by the DUT assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); - step(); - } + step(); + } + } else { + // Here we have keep[0] = 1 and keep[1] = 0, + // so the 0th byte is the last byte emitted by the DUT + assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); + step(); } } else { - // 0th byte isn't meaningful (tkeep = 0), so the DUT stops emitting bytes from this point onwards + // keep[0] = 0, so output tkeep must also be 0 and no meaningful bytes are emitted + assert_eq(DUT.output_axis_tkeep, 1'b0); assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); step(); } -} \ No newline at end of file +} From e3a929fac353484cc7d4ca2bd67f3d4f4710e24f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Thu, 27 Aug 2026 10:47:22 -0400 Subject: [PATCH 21/29] make generate_runt_configs work with branch on argument --- cli/src/main.rs | 13 +++++++++++-- runt/bi/runt.toml | 4 ++-- runt/interp/runt.toml | 1 - scripts/generate_runt_configs.py | 1 + 4 files changed, 14 insertions(+), 5 deletions(-) diff --git a/cli/src/main.rs b/cli/src/main.rs index f9b929d6..1a8aa773 100644 --- a/cli/src/main.rs +++ b/cli/src/main.rs @@ -23,6 +23,10 @@ struct Args { )] protocol: Vec, + /// Allow arguments to appear in while/if conditions + #[arg(long)] + allow_branch_on_arg: bool, + #[command(subcommand)] command: Option, } @@ -203,8 +207,13 @@ fn main() { // we always parse and type check the protocol file let skip_static_step_fork_checks = false; let mut d = DiagnosticHandler::new(ColorChoice::Auto, false, true, false); - let (st, modules) = - frontend(&args.protocol, &mut d, skip_static_step_fork_checks, false).unwrap(); + let (st, modules) = frontend( + &args.protocol, + &mut d, + skip_static_step_fork_checks, + args.allow_branch_on_arg, + ) + .unwrap(); match args.command { None => {} diff --git a/runt/bi/runt.toml b/runt/bi/runt.toml index d86248eb..d450e56b 100644 --- a/runt/bi/runt.toml +++ b/runt/bi/runt.toml @@ -2383,7 +2383,7 @@ paths = [ ] expect_dir = "../../tests/fpga-debugging/axis-adapter-s3/expects" expect_name = "s3_buggy.bi.expect" -cmd = "cd ../.. && target/debug/bi --color never --protocol tests/fpga-debugging/axis-adapter-s3/s3.prot --wave tests/fpga-debugging/axis-adapter-s3/s3_buggy.fst --instances TOP.test_axis_adapter_64_8.UUT:AXIS --sample-posedge TOP.test_axis_adapter_64_8.UUT.clk --show-waveform-time --include-idle --time-unit ns --display-hex 2>&1" +cmd = "cd ../.. && target/debug/bi --color never --protocol tests/fpga-debugging/axis-adapter-s3/s3.prot --wave tests/fpga-debugging/axis-adapter-s3/s3_buggy.fst --instances TOP.test_axis_adapter_64_8.UUT:AXIS --sample-posedge TOP.test_axis_adapter_64_8.UUT.clk --show-waveform-time --include-idle --time-unit ns --display-hex --allow-branch-on-arg 2>&1" [[tests]] name = "bi.tests_fpga_debugging_axis_adapter_s3_s3.s3_fixed_bi" @@ -2392,7 +2392,7 @@ paths = [ ] expect_dir = "../../tests/fpga-debugging/axis-adapter-s3/expects" expect_name = "s3_fixed.bi.expect" -cmd = "cd ../.. && target/debug/bi --color never --protocol tests/fpga-debugging/axis-adapter-s3/s3.prot --wave tests/fpga-debugging/axis-adapter-s3/s3_fixed.fst --instances TOP.test_axis_adapter_64_8.UUT:AXIS --sample-posedge TOP.test_axis_adapter_64_8.UUT.clk --show-waveform-time --include-idle --time-unit ns --display-hex 2>&1" +cmd = "cd ../.. && target/debug/bi --color never --protocol tests/fpga-debugging/axis-adapter-s3/s3.prot --wave tests/fpga-debugging/axis-adapter-s3/s3_fixed.fst --instances TOP.test_axis_adapter_64_8.UUT:AXIS --sample-posedge TOP.test_axis_adapter_64_8.UUT.clk --show-waveform-time --include-idle --time-unit ns --display-hex --allow-branch-on-arg 2>&1" [[tests]] name = "bi.tests_fpga_debugging_axis_async_fifo_c4_c4.c4_buggy_bi" diff --git a/runt/interp/runt.toml b/runt/interp/runt.toml index 5c51a57f..4138ab28 100644 --- a/runt/interp/runt.toml +++ b/runt/interp/runt.toml @@ -450,7 +450,6 @@ expect_dir = "../../tests/fpga-debugging/axi-stream-s2/expects" expect_name = "s2_fixed.interp.expect" cmd = "cd ../.. && target/debug/protocols-interp --color never --transactions tests/fpga-debugging/axi-stream-s2/s2_fixed.tx --verilog tests/fpga-debugging/axi-stream-s2/s2_fixed.v --protocol tests/fpga-debugging/axi-stream-s2/s2.prot --module xlnxstream_2018_3 2>&1" - [[tests]] name = "interp.tests_fpga_debugging_axis_adapter_s3_s3_fixed.s3_fixed_interp" paths = [ diff --git a/scripts/generate_runt_configs.py b/scripts/generate_runt_configs.py index b3616023..97f4dc62 100644 --- a/scripts/generate_runt_configs.py +++ b/scripts/generate_runt_configs.py @@ -331,6 +331,7 @@ def protocol_constructs(protocol_path: str) -> frozenset[str]: "--bin", "protocols-cli", "--", + "--allow-branch-on-arg", "-p", protocol_path, "constructs", From feac58afd3f59201e7cfe336aad4df0fbda47b61 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Thu, 27 Aug 2026 11:04:10 -0400 Subject: [PATCH 22/29] remove duplicate protocol --- .../axis-adapter-s3/s3_new.prot | 303 ------------------ 1 file changed, 303 deletions(-) delete mode 100644 tests/fpga-debugging/axis-adapter-s3/s3_new.prot diff --git a/tests/fpga-debugging/axis-adapter-s3/s3_new.prot b/tests/fpga-debugging/axis-adapter-s3/s3_new.prot deleted file mode 100644 index eb43a95b..00000000 --- a/tests/fpga-debugging/axis-adapter-s3/s3_new.prot +++ /dev/null @@ -1,303 +0,0 @@ -// This file describes an AXI-Stream width adapter which -// converts a 64-bit input into 8-bit output chunks over multiple cycles - -// Notes: -// - The DUT has 3 termination conditions: -// - 1. All 8 bytes have been emitted (in the fixed DUT, this only happens when `tkeep = 11111111`, i.e. all bytes of `tdata` are meaningful) -// - 2. When emitting the i-th byte, the DUT sees that `tkeep[i] = 0`, in which case it treats the i-th byte as the last one and stops emitting any further bytes -// - 3. For the fixed DUT only, if `tkeep[i] = 1` but `tkeep[i+1] = 0`, then the DUT treats the `i`-th byte as the last one -// and stops emitting any further bytes (the fixed DUT gains this "lookahead" logic) -// - The `tlast` parameter indicates if the data word corresponds to the final word of a packet -// (Note: there can be multiple words in a packet. Moreover, the last byte of a non-final word in a packet -// still gets `tlast = 0`, since it is not the last word of a packet.) -// - AXI-Stream spec says that for "downsizing" operations in which data with larger bit-widths -// are converted to smaller bitwidths (section 2.3.3), which this DUT is doing, -// if the input data word happens to be the last word of a packet (i.e. `tlast = 1` for the input), -// in the output sequence of bytes, `tlast` can only be asserted for the last byte emitted -// - The DUT cannot accept a new 64-bit input when it is still emitting the bytes of the existing data -// - The DUT examines `tkeep` from right to left, i.e. the 0th byte emitted -// corresponds to `tdata[7:0]` and `tkeep[0]` (the LSB of `tkeep`) -// - The fixed waveform has `tkeep = 0001 1111`, so only 5 bytes are emitted and the -// waveform ends after the 5 bytes are emitted -// - The `output_bytes` parameter to the `send_word` protocol below contains -// the bytes in the order they're emitted, and since the DUT examines `tdata` right to left, -// this means if `tdata = 0xABCD`, the output bytes are `[0xCD, 0xAB]` -// (i.e. the bytes corresponding to less significant bits are emitted first) - -struct AXIS { - // Reset is active-high - in rst: u1, - - // Signals related to the DUT accepting input data from the environment - - // 64-bit data that the DUT accepts as input from the environment - in input_axis_tdata: u64, - - // bitmask indicating which bytes of `tdata` are meaningful - in input_axis_tkeep: u8, - - // 1 if this is the last word in a packet - in input_axis_tlast: u1, - - // Indicates if `input_tdata` contains valid data - in input_axis_tvalid: u1, - - // Signal indicating whether the DUT - // is ready to accept data from the environment as input - out input_axis_tready: u1, - - //---------------------------------------------------------------- - // Signals related to the DUT emitting data as output - - // 8-bit data that the DUT emits as output - out output_axis_tdata: u8, - - // Output data is 8 bits, so `tkeep` is now just 1 bit wide - // `tkeep` is 1 if `output_tdata` contains meaningful data - out output_axis_tkeep: u1, - - // 1 if this is the last word in a packet - out output_axis_tlast: u1, - - // Indicates if `output_data` contains valid data - out output_axis_tvalid: u1, - - // Signal indicating whether the environment is ready to - // accept the data emitted by the DUT as output - in output_axis_tready: u1, -} - -prot reset() { - DUT.rst := 1'b1; - - // Valid pin (for both directions) must be low when - // reset is asserted (AXI-Stream spec section 2.7.2) - DUT.input_axis_tvalid := 1'b0; - assert_eq(DUT.output_axis_tvalid, 1'b0); - - step(); -} - -// When idle, the DUT neither accepts data from the environment, -// nor does it emit data as output -#[idle] -prot idle() { - DUT.rst := 1'b0; - DUT.input_axis_tvalid := 1'b0; - - assert_eq(DUT.output_axis_tvalid, 1'b0); - step(); -} - -// Note: the `split_word` protocol below is a variant of the one in `s3.prot`, -// except it branches on `keep[i]`, where `keep` is a parameter to the protocol -// (Branching on parameters is currently not permitted in our DSL) - -// - `is_final_word_in_packet` is a parameter that represents `tlast` -// (this variable name was chosen to be more informative and to avoid confusion with our DSL's `is_last()` construct) -prot split_word(data: u64, keep: u8, is_final_word_in_packet: u1) { - DUT.rst := 1'b0; - DUT.input_axis_tdata := data; - DUT.input_axis_tkeep := keep; - DUT.input_axis_tlast := is_final_word_in_packet; - - // There is valid data (namely the input word), so set `valid = 1` - DUT.input_axis_tvalid := 1'b1; - - // Wait until the DUT signals it is ready to accept to the input word - while (!(DUT.input_axis_tready == 1'b1)) { - step(); - } - // One cycle for DUT to accept input data from environment - step(); - - // DUT has accepted input data, so we set the input pins to DontCare - DUT.input_axis_tdata := X; - DUT.input_axis_tkeep := X; - DUT.input_axis_tlast := X; - - // Since input pins are DontCare, there is no longer valid data, so set `valid = 0` - DUT.input_axis_tvalid := 1'b0; - - // Environment is now ready to accept the output data emitted by the DUT - DUT.output_axis_tready := 1'b1; - - // Wait until the DUT indicates that there is valid data to emit - while (!(DUT.output_axis_tvalid == 1'b1)) { - step(); - } - // Both ready & valid are now 1 in the output direction, - // so the DUT can begin to emit the 0th byte - - // Rightmost 8 bits of `data` are now on the `output_tdata` pin - assert_eq(DUT.output_axis_tdata, data[7:0]); - - // Check if 0th byte is meaningful - if (keep[0] == 1'b1) { - // keep[0] = 1, so the output tkeep must also be 1 - assert_eq(DUT.output_axis_tkeep, 1'b1); - - // Lookahead and check if 1st byte is also meaningful - if (keep[1] == 1'b1) { - // 1st byte is meaningful, so the 0th byte can't be the end of the packet, - // so output tlast must be 0 for the 0th byte - assert_eq(DUT.output_axis_tlast, 1'b0); - - // One clock cycle to emit the 0th byte - step(); - - // Wait till DUT has valid data to emit for the 1st byte - while (!(DUT.output_axis_tvalid == 1'b1)) { - step(); - } - - assert_eq(DUT.output_axis_tdata, data[15:8]); - - // We've already established above that keep[1] = 1, so output tkeep must be 1 for the 1st byte - assert_eq(DUT.output_axis_tkeep, 1'b1); - - // Lookahead and check if 2nd byte is meaningful - if (keep[2] == 1'b1) { - // 2nd byte is meaningful, so the 1st byte can't be the end of the packet, - // so output tlast must be 0 for the 1st byte - assert_eq(DUT.output_axis_tlast, 1'b0); - - // One clock cycle to emit the 1st byte - step(); - - while (!(DUT.output_axis_tvalid == 1'b1)) { - step(); - } - assert_eq(DUT.output_axis_tdata, data[23:16]); - - // We've already established above that keep[2] = 1, so output tkeep must be 1 for the 2nd byte - assert_eq(DUT.output_axis_tkeep, 1'b1); - - // Check if 3rd byte is meaningful - if (keep[3] == 1'b1) { - // 3rd byte is meaningful, so the 2nd byte can't be the end of the packet, - // so output tlast must be 0 for the 2nd byte - assert_eq(DUT.output_axis_tlast, 1'b0); - - // One clock cycle to emit the 2nd byte - step(); - - while (!(DUT.output_axis_tvalid == 1'b1)) { - step(); - } - assert_eq(DUT.output_axis_tdata, data[31:24]); - - // We've already established above that keep[3] = 1, so output tkeep must be 1 for the 3rd byte - assert_eq(DUT.output_axis_tkeep, 1'b1); - - if (keep[4] == 1'b1) { - // 4th byte is meaningful, so output tlast must be 0 for the 3rd byte - assert_eq(DUT.output_axis_tlast, 1'b0); - - step(); - - while (!(DUT.output_axis_tvalid == 1'b1)) { - step(); - } - - assert_eq(DUT.output_axis_tdata, data[39:32]); - - // We've already established above that keep[4] = 1, so output tkeep must be 1 for the 4th byte - assert_eq(DUT.output_axis_tkeep, 1'b1); - - if (keep[5] == 1'b1) { - // 5th byte is meaningful, so output tlast must be 0 for the 4th byte - assert_eq(DUT.output_axis_tlast, 1'b0); - - step(); - - while (!(DUT.output_axis_tvalid == 1'b1)) { - step(); - } - assert_eq(DUT.output_axis_tdata, data[47:40]); - - // We've already established above that keep[5] = 1, so output tkeep must be 1 for the 5th byte - assert_eq(DUT.output_axis_tkeep, 1'b1); - - if (keep[6] == 1'b1) { - // 6th byte is meaningful, so output tlast must be 0 for the 5th byte - assert_eq(DUT.output_axis_tlast, 1'b0); - - step(); - - while (!(DUT.output_axis_tvalid == 1'b1)) { - step(); - } - assert_eq(DUT.output_axis_tdata, data[55:48]); - - // We've already established above that keep[6] = 1, so output tkeep must be 1 for the 6th byte - assert_eq(DUT.output_axis_tkeep, 1'b1); - - if (keep[7] == 1'b1) { - // 7th byte is meaningful, so output tlast must be 0 for the 6th byte - assert_eq(DUT.output_axis_tlast, 1'b0); - - step(); - - while (!(DUT.output_axis_tvalid == 1'b1)) { - step(); - } - assert_eq(DUT.output_axis_tdata, data[63:56]); - - // We've already established above that keep[7] = 1, so output tkeep must be 1 for the 7th byte - assert_eq(DUT.output_axis_tkeep, 1'b1); - - // The 7th byte is the last byte for a 64-bit word, - // so we don't need to inspect the `tkeep` bit for the "next" byte - // We only need to check whether this byte is the end of the - // of the entire packet, which is determined by the `is_final_word_in_packet` parameter - assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); - - // One clock cycle to emit the 7th and final byte - step(); - } else { - // keep[6] = 1, keep[7] = 0 - assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); - step(); - } - } else { - // keep[5] = 1, keep[6] = 0 - assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); - step(); - } - } else { - // keep[4] = 1, keep[5] = 0 - assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); - step(); - } - } else { - // Here we have keep[3] = 1, keep[4] = 0 - // so the 3rd byte is the last byte emitted by the DUT - assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); - step(); - } - } else { - // Here we have keep[2] = 1 and keep[3] = 0, - // so the 2nd byte is the last byte emitted by the DUT - assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); - step(); - } - } else { - // Here we have keep[1] = 1 and keep[2] = 0, - // so the 1st byte is the last byte emitted by the DUT - assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); - step(); - } - } else { - // Here we have keep[0] = 1 and keep[1] = 0, - // so the 0th byte is the last byte emitted by the DUT - assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); - step(); - } - } else { - // keep[0] = 0, so output tkeep must also be 0 and no meaningful bytes are emitted - assert_eq(DUT.output_axis_tkeep, 1'b0); - assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); - step(); - } -} From 0f69a98298d5138157abd12e3daaeec89ad5f655 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Thu, 27 Aug 2026 11:07:56 -0400 Subject: [PATCH 23/29] interp: add allow-branch-on-arg flag --- interp/src/main.rs | 6 +++++- runt/graph_interp/runt.toml | 6 +++--- runt/interp/runt.toml | 2 +- runt/waveform/runt.toml | 6 +++--- scripts/test_catalog.py | 1 + 5 files changed, 13 insertions(+), 8 deletions(-) diff --git a/interp/src/main.rs b/interp/src/main.rs index 9e4e7b19..ca1a1b6c 100644 --- a/interp/src/main.rs +++ b/interp/src/main.rs @@ -69,6 +69,10 @@ struct Cli { /// Prints only trace status lines and ASCII waveforms #[arg(long)] ascii_waveform: bool, + + /// Allow arguments to appear in while/if conditions + #[arg(long)] + allow_branch_on_arg: bool, } /// Examples (enables all tracing logs): @@ -136,7 +140,7 @@ fn main() -> anyhow::Result<()> { &cli.protocol, &mut protocols_handler, cli.skip_static_step_fork_checks, - false, + cli.allow_branch_on_arg, ) { Ok(result) => result, Err(error) => exit_after_setup_error(error, !protocols_handler.error_string().is_empty()), diff --git a/runt/graph_interp/runt.toml b/runt/graph_interp/runt.toml index f273a862..0c71e46b 100644 --- a/runt/graph_interp/runt.toml +++ b/runt/graph_interp/runt.toml @@ -538,7 +538,7 @@ paths = [ ] expect_dir = "../../tests/fpga-debugging/axis-adapter-s3/expects" expect_name = "s3_fixed.graph_interp.expect" -cmd = "cd ../.. && target/debug/graph-interp --transactions tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx --verilog tests/fpga-debugging/axis-adapter-s3/s3_fixed.v --protocol tests/fpga-debugging/axis-adapter-s3/s3.prot --module axis_adapter 2>/dev/null" +cmd = "cd ../.. && target/debug/graph-interp --transactions tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx --allow-branch-on-arg --verilog tests/fpga-debugging/axis-adapter-s3/s3_fixed.v --protocol tests/fpga-debugging/axis-adapter-s3/s3.prot --module axis_adapter 2>/dev/null" [[tests]] name = "graph_interp.tests_fpga_debugging_axis_adapter_s3_s3_fixed.s3_fixed_graph_interp.contract_edges" @@ -547,7 +547,7 @@ paths = [ ] expect_dir = "../../tests/fpga-debugging/axis-adapter-s3/expects" expect_name = "s3_fixed.graph_interp.expect" -cmd = "cd ../.. && target/debug/graph-interp --transactions tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx --verilog tests/fpga-debugging/axis-adapter-s3/s3_fixed.v --protocol tests/fpga-debugging/axis-adapter-s3/s3.prot --module axis_adapter --contract-edges 2>/dev/null" +cmd = "cd ../.. && target/debug/graph-interp --transactions tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx --allow-branch-on-arg --verilog tests/fpga-debugging/axis-adapter-s3/s3_fixed.v --protocol tests/fpga-debugging/axis-adapter-s3/s3.prot --module axis_adapter --contract-edges 2>/dev/null" [[tests]] name = "graph_interp.tests_fpga_debugging_axis_adapter_s3_s3_fixed.s3_fixed_graph_interp.respect_forks" @@ -556,7 +556,7 @@ paths = [ ] expect_dir = "../../tests/fpga-debugging/axis-adapter-s3/expects" expect_name = "s3_fixed.graph_interp.expect" -cmd = "cd ../.. && target/debug/graph-interp --transactions tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx --verilog tests/fpga-debugging/axis-adapter-s3/s3_fixed.v --protocol tests/fpga-debugging/axis-adapter-s3/s3.prot --module axis_adapter --respect-forks --determinize 2>/dev/null" +cmd = "cd ../.. && target/debug/graph-interp --transactions tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx --allow-branch-on-arg --verilog tests/fpga-debugging/axis-adapter-s3/s3_fixed.v --protocol tests/fpga-debugging/axis-adapter-s3/s3.prot --module axis_adapter --respect-forks --determinize 2>/dev/null" [[tests]] name = "graph_interp.tests_fpga_debugging_axis_async_fifo_c4_c4_fixed.c4_fixed_graph_interp" diff --git a/runt/interp/runt.toml b/runt/interp/runt.toml index 4138ab28..03703603 100644 --- a/runt/interp/runt.toml +++ b/runt/interp/runt.toml @@ -457,7 +457,7 @@ paths = [ ] expect_dir = "../../tests/fpga-debugging/axis-adapter-s3/expects" expect_name = "s3_fixed.interp.expect" -cmd = "cd ../.. && target/debug/protocols-interp --color never --transactions tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx --verilog tests/fpga-debugging/axis-adapter-s3/s3_fixed.v --protocol tests/fpga-debugging/axis-adapter-s3/s3.prot --module axis_adapter 2>&1" +cmd = "cd ../.. && target/debug/protocols-interp --color never --transactions tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx --allow-branch-on-arg --verilog tests/fpga-debugging/axis-adapter-s3/s3_fixed.v --protocol tests/fpga-debugging/axis-adapter-s3/s3.prot --module axis_adapter 2>&1" [[tests]] name = "interp.tests_fpga_debugging_axis_async_fifo_c4_c4_buggy.c4_buggy_interp" diff --git a/runt/waveform/runt.toml b/runt/waveform/runt.toml index 7d5da4f4..15fd8bfd 100644 --- a/runt/waveform/runt.toml +++ b/runt/waveform/runt.toml @@ -682,7 +682,7 @@ paths = [ ] expect_dir = "../../tests/fpga-debugging/axis-adapter-s3/expects" expect_name = "s3_fixed.waveform.expect" -cmd = "cd ../.. && target/debug/protocols-interp --color never --transactions tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx --ascii-waveform --verilog tests/fpga-debugging/axis-adapter-s3/s3_fixed.v --protocol tests/fpga-debugging/axis-adapter-s3/s3.prot --module axis_adapter 2>/dev/null" +cmd = "cd ../.. && target/debug/protocols-interp --color never --transactions tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx --ascii-waveform --allow-branch-on-arg --verilog tests/fpga-debugging/axis-adapter-s3/s3_fixed.v --protocol tests/fpga-debugging/axis-adapter-s3/s3.prot --module axis_adapter 2>/dev/null" [[tests]] name = "waveform.tests_fpga_debugging_axis_adapter_s3_s3_fixed.s3_fixed_waveform.graph" @@ -691,7 +691,7 @@ paths = [ ] expect_dir = "../../tests/fpga-debugging/axis-adapter-s3/expects" expect_name = "s3_fixed.waveform.expect" -cmd = "cd ../.. && target/debug/graph-interp --transactions tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx --respect-forks --determinize --ascii-waveform --verilog tests/fpga-debugging/axis-adapter-s3/s3_fixed.v --protocol tests/fpga-debugging/axis-adapter-s3/s3.prot --module axis_adapter 2>/dev/null" +cmd = "cd ../.. && target/debug/graph-interp --transactions tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx --respect-forks --determinize --ascii-waveform --allow-branch-on-arg --verilog tests/fpga-debugging/axis-adapter-s3/s3_fixed.v --protocol tests/fpga-debugging/axis-adapter-s3/s3.prot --module axis_adapter 2>/dev/null" [[tests]] name = "waveform.tests_fpga_debugging_axis_adapter_s3_s3_fixed.s3_fixed_waveform.ts" @@ -700,7 +700,7 @@ paths = [ ] expect_dir = "../../tests/fpga-debugging/axis-adapter-s3/expects" expect_name = "s3_fixed.waveform.expect" -cmd = "cd ../.. && target/debug/graph-interp --transactions tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx --transition-system --ascii-waveform --verilog tests/fpga-debugging/axis-adapter-s3/s3_fixed.v --protocol tests/fpga-debugging/axis-adapter-s3/s3.prot --module axis_adapter 2>/dev/null" +cmd = "cd ../.. && target/debug/graph-interp --transactions tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx --transition-system --ascii-waveform --allow-branch-on-arg --verilog tests/fpga-debugging/axis-adapter-s3/s3_fixed.v --protocol tests/fpga-debugging/axis-adapter-s3/s3.prot --module axis_adapter 2>/dev/null" [[tests]] name = "waveform.tests_fpga_debugging_axis_async_fifo_c4_c4_fixed.c4_fixed_waveform.ast" diff --git a/scripts/test_catalog.py b/scripts/test_catalog.py index 2171458d..703522e8 100644 --- a/scripts/test_catalog.py +++ b/scripts/test_catalog.py @@ -310,6 +310,7 @@ "verilog": ("tests/fpga-debugging/axis-adapter-s3/s3_fixed.v",), "top": "axis_adapter", "expect": "pass", + "extra_args": ("--allow-branch-on-arg",), }, "tests/fpga-debugging/axi-stream-s2/s2_fixed.tx": { "protocol": "tests/fpga-debugging/axi-stream-s2/s2.prot", From ae14213c2fee5398674c2729755a4887ac8151a6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Thu, 27 Aug 2026 11:17:40 -0400 Subject: [PATCH 24/29] runt: graph interpreter fails on s3.prot and that is ok for now --- .../axis-adapter-s3/expects/s3_fixed.graph_interp.expect | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/tests/fpga-debugging/axis-adapter-s3/expects/s3_fixed.graph_interp.expect b/tests/fpga-debugging/axis-adapter-s3/expects/s3_fixed.graph_interp.expect index f5f6cb49..57404ebb 100644 --- a/tests/fpga-debugging/axis-adapter-s3/expects/s3_fixed.graph_interp.expect +++ b/tests/fpga-debugging/axis-adapter-s3/expects/s3_fixed.graph_interp.expect @@ -1 +1,2 @@ -Trace 0 executed successfully! +---CODE--- +2 From c0b04d5e4bb78c449ef340dd771a85e809a0e05f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Thu, 27 Aug 2026 11:49:16 -0400 Subject: [PATCH 25/29] protocol: add more information to error message --- protocols/src/errors.rs | 11 +++++++++-- protocols/src/scheduler.rs | 2 ++ 2 files changed, 11 insertions(+), 2 deletions(-) diff --git a/protocols/src/errors.rs b/protocols/src/errors.rs index d2e0b057..461b2f48 100644 --- a/protocols/src/errors.rs +++ b/protocols/src/errors.rs @@ -120,6 +120,7 @@ pub enum ThreadError { thread_idx: usize, transaction_name: String, stmt_id: StmtId, + step_count: u32, }, /// Thread execution limit exceeded (for infinite loop protection) ExecutionLimitExceeded { max_steps: usize }, @@ -344,11 +345,13 @@ impl fmt::Display for ThreadError { new_value, thread_idx, transaction_name, + step_count, .. } => { write!( f, - "Thread {} (`{}`) attempted conflicting assignment to '{}': current={}, new={}", + "@{} Thread {} (`{}`) attempted conflicting assignment to '{}': current={}, new={}", + step_count, thread_idx, transaction_name, symbol_name, @@ -514,6 +517,7 @@ impl ExecutionError { thread_idx: usize, transaction_name: String, stmt_id: StmtId, + step_count: u32, ) -> Self { ExecutionError::Thread(ThreadError::ConflictingAssignment { symbol_name, @@ -522,6 +526,7 @@ impl ExecutionError { thread_idx, transaction_name, stmt_id, + step_count, }) } @@ -895,13 +900,15 @@ impl DiagnosticEmitter { thread_idx, transaction_name, stmt_id, + step_count, .. } => { handler.emit_diagnostic_stmt( transaction, stmt_id, &format!( - "Thread {} (`{}`) attempted conflicting assignment to '{}': current={}, new={}", + "@{} Thread {} (`{}`) attempted conflicting assignment to '{}': current={}, new={}", + step_count, thread_idx, transaction_name, symbol_name, diff --git a/protocols/src/scheduler.rs b/protocols/src/scheduler.rs index b264387c..9890123f 100644 --- a/protocols/src/scheduler.rs +++ b/protocols/src/scheduler.rs @@ -448,6 +448,7 @@ impl<'a> Scheduler<'a> { *first_idx, first_transaction_name, first_stmt_id.expect("Concrete values should have stmt_id"), + self.step_count, ), )); @@ -461,6 +462,7 @@ impl<'a> Scheduler<'a> { *second_idx, second_transaction_name, second_stmt_id.expect("Concrete values should have stmt_id"), + self.step_count, ), )); From 9cb125a9a3b34991a44299b15258ca4baf5f2bad Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Thu, 27 Aug 2026 11:49:35 -0400 Subject: [PATCH 26/29] s3: allow some overlap between transactions and add more extensive transaction test --- tests/fpga-debugging/axis-adapter-s3/s3.prot | 30 ++++++++-- .../axis-adapter-s3/s3_fixed.tx | 56 ++++++++++++++++++ .../axis-adapter-s3/s3_fixed_tx.fst | Bin 0 -> 2924 bytes 3 files changed, 80 insertions(+), 6 deletions(-) create mode 100644 tests/fpga-debugging/axis-adapter-s3/s3_fixed_tx.fst diff --git a/tests/fpga-debugging/axis-adapter-s3/s3.prot b/tests/fpga-debugging/axis-adapter-s3/s3.prot index 060f81c1..fa99b267 100644 --- a/tests/fpga-debugging/axis-adapter-s3/s3.prot +++ b/tests/fpga-debugging/axis-adapter-s3/s3.prot @@ -73,8 +73,13 @@ prot reset() { // Valid pin (for both directions) must be low when // reset is asserted (AXI-Stream spec section 2.7.2) DUT.input_axis_tvalid := 1'b0; - assert_eq(DUT.output_axis_tvalid, 1'b0); + step(); + DUT.rst := X; + DUT.input_axis_tvalid := X; + // one cycle after reset, the output t_valid must be deasserted + assert_eq(DUT.output_axis_tvalid, 1'b0); + fork(); step(); } @@ -84,8 +89,6 @@ prot reset() { prot idle() { DUT.rst := 1'b0; DUT.input_axis_tvalid := 1'b0; - - assert_eq(DUT.output_axis_tvalid, 1'b0); step(); } @@ -111,15 +114,16 @@ prot split_word(data: u64, keep: u8, is_final_word_in_packet: u1) { DUT.input_axis_tdata := X; DUT.input_axis_tkeep := X; DUT.input_axis_tlast := X; - - // Since input pins are DontCare, there is no longer valid data, so set `valid = 0` - DUT.input_axis_tvalid := 1'b0; + // valid can be anything from now on, it is on the DUT to assert backpressure until it is ready + DUT.input_axis_tvalid := X; + fork(); // Environment is now ready to accept the output data emitted by the DUT DUT.output_axis_tready := 1'b1; // Wait until the DUT indicates that there is valid data to emit while (!(DUT.output_axis_tvalid == 1'b1)) { + assert_eq(DUT.input_axis_tready, 1'b0); step(); } // Both ready & valid are now 1 in the output direction, @@ -138,12 +142,14 @@ prot split_word(data: u64, keep: u8, is_final_word_in_packet: u1) { // 1st byte is meaningful, so the 0th byte can't be the end of the packet, // so output tlast must be 0 for the 0th byte assert_eq(DUT.output_axis_tlast, 1'b0); + assert_eq(DUT.input_axis_tready, 1'b0); // One clock cycle to emit the 0th byte step(); // Wait till DUT has valid data to emit for the 1st byte while (!(DUT.output_axis_tvalid == 1'b1)) { + assert_eq(DUT.input_axis_tready, 1'b0); step(); } @@ -157,11 +163,13 @@ prot split_word(data: u64, keep: u8, is_final_word_in_packet: u1) { // 2nd byte is meaningful, so the 1st byte can't be the end of the packet, // so output tlast must be 0 for the 1st byte assert_eq(DUT.output_axis_tlast, 1'b0); + assert_eq(DUT.input_axis_tready, 1'b0); // One clock cycle to emit the 1st byte step(); while (!(DUT.output_axis_tvalid == 1'b1)) { + assert_eq(DUT.input_axis_tready, 1'b0); step(); } assert_eq(DUT.output_axis_tdata, data[23:16]); @@ -174,11 +182,13 @@ prot split_word(data: u64, keep: u8, is_final_word_in_packet: u1) { // 3rd byte is meaningful, so the 2nd byte can't be the end of the packet, // so output tlast must be 0 for the 2nd byte assert_eq(DUT.output_axis_tlast, 1'b0); + assert_eq(DUT.input_axis_tready, 1'b0); // One clock cycle to emit the 2nd byte step(); while (!(DUT.output_axis_tvalid == 1'b1)) { + assert_eq(DUT.input_axis_tready, 1'b0); step(); } assert_eq(DUT.output_axis_tdata, data[31:24]); @@ -189,10 +199,12 @@ prot split_word(data: u64, keep: u8, is_final_word_in_packet: u1) { if (keep[4] == 1'b1) { // 4th byte is meaningful, so output tlast must be 0 for the 3rd byte assert_eq(DUT.output_axis_tlast, 1'b0); + assert_eq(DUT.input_axis_tready, 1'b0); step(); while (!(DUT.output_axis_tvalid == 1'b1)) { + assert_eq(DUT.input_axis_tready, 1'b0); step(); } @@ -204,10 +216,12 @@ prot split_word(data: u64, keep: u8, is_final_word_in_packet: u1) { if (keep[5] == 1'b1) { // 5th byte is meaningful, so output tlast must be 0 for the 4th byte assert_eq(DUT.output_axis_tlast, 1'b0); + assert_eq(DUT.input_axis_tready, 1'b0); step(); while (!(DUT.output_axis_tvalid == 1'b1)) { + assert_eq(DUT.input_axis_tready, 1'b0); step(); } assert_eq(DUT.output_axis_tdata, data[47:40]); @@ -218,10 +232,12 @@ prot split_word(data: u64, keep: u8, is_final_word_in_packet: u1) { if (keep[6] == 1'b1) { // 6th byte is meaningful, so output tlast must be 0 for the 5th byte assert_eq(DUT.output_axis_tlast, 1'b0); + assert_eq(DUT.input_axis_tready, 1'b0); step(); while (!(DUT.output_axis_tvalid == 1'b1)) { + assert_eq(DUT.input_axis_tready, 1'b0); step(); } assert_eq(DUT.output_axis_tdata, data[55:48]); @@ -232,10 +248,12 @@ prot split_word(data: u64, keep: u8, is_final_word_in_packet: u1) { if (keep[7] == 1'b1) { // 7th byte is meaningful, so output tlast must be 0 for the 6th byte assert_eq(DUT.output_axis_tlast, 1'b0); + assert_eq(DUT.input_axis_tready, 1'b0); step(); while (!(DUT.output_axis_tvalid == 1'b1)) { + assert_eq(DUT.input_axis_tready, 1'b0); step(); } assert_eq(DUT.output_axis_tdata, data[63:56]); diff --git a/tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx b/tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx index 9bb3da82..fe97f8f5 100644 --- a/tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx +++ b/tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx @@ -1,6 +1,62 @@ trace { + idle(); reset(); idle(); // Same transaction with the same input data, as in `s3_fixed.fst` (waveform from Brave New World artifact) split_word(0xabcdabcdabcdabcd, 0x1f, 0b1); + // enough idle transactions to wait for split_word to finish before we can assert reset + idle(); idle(); idle(); idle(); idle(); idle(); + + // test a couple of input argument values + reset(); + idle(); + split_word(0x0000000000000011, 0b00000001, 0); + split_word(0x0000000000002211, 0b00000011, 0); + split_word(0x0000000000332211, 0b00000111, 0); + split_word(0x0000000044332211, 0b00001111, 0); + split_word(0x0000005544332211, 0b00011111, 0); + split_word(0x0000665544332211, 0b00111111, 0); + split_word(0x0077665544332211, 0b01111111, 0); + split_word(0x8877665544332211, 0b11111111, 0); + split_word(0x0000000000000011, 0b00000001, 0); + split_word(0x0000000000002211, 0b00000011, 1); + split_word(0x0000000000332211, 0b00000111, 1); + split_word(0x0000000044332211, 0b00001111, 1); + split_word(0x0000005544332211, 0b00011111, 1); + split_word(0x0000665544332211, 0b00111111, 1); + split_word(0x0077665544332211, 0b01111111, 1); + split_word(0x8877665544332211, 0b11111111, 1); + idle(); + split_word(0x0000000000000011, 0b00000001, 0); + idle(); + split_word(0x0000000000002211, 0b00000011, 0); + idle(); + split_word(0x0000000000332211, 0b00000111, 0); + idle(); + split_word(0x0000000044332211, 0b00001111, 0); + idle(); + split_word(0x0000005544332211, 0b00011111, 0); + idle(); + split_word(0x0000665544332211, 0b00111111, 0); + idle(); + split_word(0x0077665544332211, 0b01111111, 0); + idle(); + split_word(0x8877665544332211, 0b11111111, 0); + idle(); + split_word(0x0000000000000011, 0b00000001, 0); + idle(); + split_word(0x0000000000002211, 0b00000011, 1); + idle(); + split_word(0x0000000000332211, 0b00000111, 1); + idle(); + split_word(0x0000000044332211, 0b00001111, 1); + idle(); + split_word(0x0000005544332211, 0b00011111, 1); + idle(); + split_word(0x0000665544332211, 0b00111111, 1); + idle(); + split_word(0x0077665544332211, 0b01111111, 1); + idle(); + split_word(0x8877665544332211, 0b11111111, 1); + idle(); } diff --git a/tests/fpga-debugging/axis-adapter-s3/s3_fixed_tx.fst b/tests/fpga-debugging/axis-adapter-s3/s3_fixed_tx.fst new file mode 100644 index 0000000000000000000000000000000000000000..c0ff5b0e3329a86916cf395d0d27b04d11cc3c34 GIT binary patch literal 2924 zcmeHIdu)@}760Ai>+8?X*UyiTU?))=3t(DB2>DnW8JzTjj~RCFs-Vltr{xgj{urf7?7RMcA~7> zpZlxYvClof^SJli``vSNfeeY}tehHO>3C?yGp={-(J4z7P)?71O$w}zo4ws#slKwl zfj%?&WLZa-ne6T9P4f7)HNKgu${veWWu^U2%U!HbnG%1!i#hR>**z!TH_(-c*zr$4 z;6WmBf26+d{^aIlB4sA$)K}I*V8Vk~M^{hEjD=ad2Z2iFumM*I0ukma1A%Jh8UuI= z_H8JytYdS%0e^!5XE#R;XSgV`0M0C&G+DAKQV(s8m>;pC<0!8R7jq8A!zik%&&;Ue zSyLPlfvSjbKFC?w%sjt3@>7&o^FC^;5xvEbw-TsjuH#iWyqd#5=M8fBG@f5m&C_Z) zwzd|w(+oL$YTF&6yf(LyK!oknPHCN?b{Nh}!uhG7Pef&+bEC(04T*t7XEK)PPIZ~F z-sFa_K<90v@y#85F>`&~jPDm(0ak8ICVLiOac8{Gd=T0KtnE$4*AEn8WvVaPTY#2L z@y?F*g$Q@2%oWnH1E{b$3n6v_w=7`a1s>II7&8&!YdH;PG3@%GSs4yjhBG50#+Ggk8JP2AOl-9rlRhgXYsi_bDU+0$KdJoB zWvsg4rYQ9*>5_)@$wFBqOEm*Q-2k;^)iJtGN)VBaB-s_DkVGDkLcTOm$2J!NN=LE7 zK!rw4s1B-U5pg%+zBW?iAnh;my28~%TNZ`KkIbhNYiqoTb%%dU$1f1BEu!0VhtF(1 zdEx`AxOnz6_qMzj>B>V-d48A|{2hIvfBD*tcOKhH%V&>1uyqNorWwr(MCrli68c+z zr0K|A=P>5N~2kwSM|~zn+ho^ghNk&$f4ce`pSP=_1Bl zpIrBM>a`ynpi4;WCwGr_AM(1tz1-UR5w9`cFGrTf7g09jZy&8pJl!5##wpU+v9Ipo zbE`l5dz3SzvHkls+tsZ0qL>eq#?X6T`j73|*B}{U+1~e$F8#?L8I~Wt^myyG^9R!y zuQ!L6dJq2Q_GPL$vE||;n}0t<-`f4N4FhXdw9x3h8%_3|XTo&kiMgr5FK)a{S1Qu) zG;X@Pl1|PSG8@O6y2)c{rq7 z1+_-kpgv&;j|bz?wIqyP?Agd=@DjP@FDR(aQloaA23?&rp})ZXne4yJ{_X6)%Ki@a zpJ4yT>|acW=yRGyd7SY{x(V|5kD8(U9<*6Pd45jcQy1tsNiG4+D?{X^5LGD@EYUD?4HtSl z7kWPz`d+KhXAxTAP9yAIfr>V2r+(TCV}@^xR9YyM%41^sZse=~p#nyUI?8>-TQ5`7 z=8+6ZbHb;h8uTcEqLP`zSf{9qS!XsNOP~c+2};|t`YDPitEXlg{QBif4P2*AghF0l zrXQ3q+Yi?BWc7n9+YfrC9}KG>JPWNpXdr$_)2LuLx2=7R)j~_|C>7*{e96+G+*;7p zs1F(we8t7G43fWI*1!iE5zmSdVcRd>!_(q`V+U2yhp=$LIe6)wf;`t{oE9H)!Dngq g=EpAlN;p~BUUqx%Z1MTl$OAZ>bLL)56in*>28TTmk^lez literal 0 HcmV?d00001 From 7d23fd00c766ca0fb275fb6d20ddb01cc8a3a41d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Thu, 27 Aug 2026 11:50:21 -0400 Subject: [PATCH 27/29] runt: updated error messages --- tests/adders/adder_d1/expects/add_incorrect.interp.expect | 8 ++++---- .../adder_d1/expects/add_incorrect_implicit.interp.expect | 8 ++++---- .../expects/wait_and_add_incorrect_implicit.interp.expect | 8 ++++---- .../adder_d2/expects/no_dontcare_conflict.interp.expect | 8 ++++---- .../expects/two_different_assignments_error.interp.expect | 8 ++++---- 5 files changed, 20 insertions(+), 20 deletions(-) diff --git a/tests/adders/adder_d1/expects/add_incorrect.interp.expect b/tests/adders/adder_d1/expects/add_incorrect.interp.expect index d0eb1d14..d71f4222 100644 --- a/tests/adders/adder_d1/expects/add_incorrect.interp.expect +++ b/tests/adders/adder_d1/expects/add_incorrect.interp.expect @@ -1,14 +1,14 @@ -error: Thread 0 (`add_incorrect`) attempted conflicting assignment to 'b': current=5, new=2 +error: @1 Thread 0 (`add_incorrect`) attempted conflicting assignment to 'b': current=5, new=2 ┌─ tests/adders/adder_d1/add_d1.prot:35:3 │ 35 │ DUT.b := b; - │ ^^^^^^^^^^^ Thread 0 (`add_incorrect`) attempted conflicting assignment to 'b': current=5, new=2 + │ ^^^^^^^^^^^ @1 Thread 0 (`add_incorrect`) attempted conflicting assignment to 'b': current=5, new=2 -error: Thread 1 (`add_incorrect`) attempted conflicting assignment to 'b': current=2, new=5 +error: @1 Thread 1 (`add_incorrect`) attempted conflicting assignment to 'b': current=2, new=5 ┌─ tests/adders/adder_d1/add_d1.prot:32:3 │ 32 │ DUT.b := b; - │ ^^^^^^^^^^^ Thread 1 (`add_incorrect`) attempted conflicting assignment to 'b': current=2, new=5 + │ ^^^^^^^^^^^ @1 Thread 1 (`add_incorrect`) attempted conflicting assignment to 'b': current=2, new=5 Trace 0 execution failed. ---CODE--- diff --git a/tests/adders/adder_d1/expects/add_incorrect_implicit.interp.expect b/tests/adders/adder_d1/expects/add_incorrect_implicit.interp.expect index dddb0b90..bd12e778 100644 --- a/tests/adders/adder_d1/expects/add_incorrect_implicit.interp.expect +++ b/tests/adders/adder_d1/expects/add_incorrect_implicit.interp.expect @@ -1,14 +1,14 @@ -error: Thread 0 (`add_incorrect_implicit`) attempted conflicting assignment to 'b': current=5, new=2 +error: @1 Thread 0 (`add_incorrect_implicit`) attempted conflicting assignment to 'b': current=5, new=2 ┌─ tests/adders/adder_d1/add_d1.prot:43:3 │ 43 │ DUT.b := b; - │ ^^^^^^^^^^^ Thread 0 (`add_incorrect_implicit`) attempted conflicting assignment to 'b': current=5, new=2 + │ ^^^^^^^^^^^ @1 Thread 0 (`add_incorrect_implicit`) attempted conflicting assignment to 'b': current=5, new=2 -error: Thread 1 (`add_incorrect_implicit`) attempted conflicting assignment to 'b': current=2, new=5 +error: @1 Thread 1 (`add_incorrect_implicit`) attempted conflicting assignment to 'b': current=2, new=5 ┌─ tests/adders/adder_d1/add_d1.prot:43:3 │ 43 │ DUT.b := b; - │ ^^^^^^^^^^^ Thread 1 (`add_incorrect_implicit`) attempted conflicting assignment to 'b': current=2, new=5 + │ ^^^^^^^^^^^ @1 Thread 1 (`add_incorrect_implicit`) attempted conflicting assignment to 'b': current=2, new=5 Trace 0 execution failed. ---CODE--- diff --git a/tests/adders/adder_d1/expects/wait_and_add_incorrect_implicit.interp.expect b/tests/adders/adder_d1/expects/wait_and_add_incorrect_implicit.interp.expect index cf5d0666..8f0a1b3b 100644 --- a/tests/adders/adder_d1/expects/wait_and_add_incorrect_implicit.interp.expect +++ b/tests/adders/adder_d1/expects/wait_and_add_incorrect_implicit.interp.expect @@ -1,14 +1,14 @@ -error: Thread 0 (`wait_and_add`) attempted conflicting assignment to 'b': current=5, new=2 +error: @2 Thread 0 (`wait_and_add`) attempted conflicting assignment to 'b': current=5, new=2 ┌─ tests/adders/adder_d1/add_d1.prot:62:3 │ 62 │ DUT.b := b; - │ ^^^^^^^^^^^ Thread 0 (`wait_and_add`) attempted conflicting assignment to 'b': current=5, new=2 + │ ^^^^^^^^^^^ @2 Thread 0 (`wait_and_add`) attempted conflicting assignment to 'b': current=5, new=2 -error: Thread 1 (`add_incorrect_implicit`) attempted conflicting assignment to 'b': current=2, new=5 +error: @2 Thread 1 (`add_incorrect_implicit`) attempted conflicting assignment to 'b': current=2, new=5 ┌─ tests/adders/adder_d1/add_d1.prot:43:3 │ 43 │ DUT.b := b; - │ ^^^^^^^^^^^ Thread 1 (`add_incorrect_implicit`) attempted conflicting assignment to 'b': current=2, new=5 + │ ^^^^^^^^^^^ @2 Thread 1 (`add_incorrect_implicit`) attempted conflicting assignment to 'b': current=2, new=5 Trace 0 execution failed. ---CODE--- diff --git a/tests/adders/adder_d2/expects/no_dontcare_conflict.interp.expect b/tests/adders/adder_d2/expects/no_dontcare_conflict.interp.expect index 10afa5ec..91f474f5 100644 --- a/tests/adders/adder_d2/expects/no_dontcare_conflict.interp.expect +++ b/tests/adders/adder_d2/expects/no_dontcare_conflict.interp.expect @@ -1,14 +1,14 @@ -error: Thread 0 (`add`) attempted conflicting assignment to 'b': current=5, new=2 +error: @1 Thread 0 (`add`) attempted conflicting assignment to 'b': current=5, new=2 ┌─ tests/adders/adder_d2/no_dontcare_conflict.prot:13:3 │ 13 │ DUT.b := b; - │ ^^^^^^^^^^^ Thread 0 (`add`) attempted conflicting assignment to 'b': current=5, new=2 + │ ^^^^^^^^^^^ @1 Thread 0 (`add`) attempted conflicting assignment to 'b': current=5, new=2 -error: Thread 1 (`add`) attempted conflicting assignment to 'b': current=2, new=5 +error: @1 Thread 1 (`add`) attempted conflicting assignment to 'b': current=2, new=5 ┌─ tests/adders/adder_d2/no_dontcare_conflict.prot:13:3 │ 13 │ DUT.b := b; - │ ^^^^^^^^^^^ Thread 1 (`add`) attempted conflicting assignment to 'b': current=2, new=5 + │ ^^^^^^^^^^^ @1 Thread 1 (`add`) attempted conflicting assignment to 'b': current=2, new=5 Trace 0 execution failed. ---CODE--- diff --git a/tests/identities/identity_d2/expects/two_different_assignments_error.interp.expect b/tests/identities/identity_d2/expects/two_different_assignments_error.interp.expect index 8240ded2..1fcd4e59 100644 --- a/tests/identities/identity_d2/expects/two_different_assignments_error.interp.expect +++ b/tests/identities/identity_d2/expects/two_different_assignments_error.interp.expect @@ -1,14 +1,14 @@ -error: Thread 0 (`multiple_assign`) attempted conflicting assignment to 'a': current=2, new=1 +error: @1 Thread 0 (`multiple_assign`) attempted conflicting assignment to 'a': current=2, new=1 ┌─ tests/identities/identity_d2/identity_d2.prot:12:3 │ 12 │ DUT.a := a; - │ ^^^^^^^^^^^ Thread 0 (`multiple_assign`) attempted conflicting assignment to 'a': current=2, new=1 + │ ^^^^^^^^^^^ @1 Thread 0 (`multiple_assign`) attempted conflicting assignment to 'a': current=2, new=1 -error: Thread 1 (`multiple_assign`) attempted conflicting assignment to 'a': current=1, new=2 +error: @1 Thread 1 (`multiple_assign`) attempted conflicting assignment to 'a': current=1, new=2 ┌─ tests/identities/identity_d2/identity_d2.prot:9:3 │ 9 │ DUT.a := a; - │ ^^^^^^^^^^^ Thread 1 (`multiple_assign`) attempted conflicting assignment to 'a': current=1, new=2 + │ ^^^^^^^^^^^ @1 Thread 1 (`multiple_assign`) attempted conflicting assignment to 'a': current=1, new=2 Trace 0 execution failed. ---CODE--- From 7940169e3a8f742b50246e955fbbfb763be2330c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Thu, 27 Aug 2026 11:56:47 -0400 Subject: [PATCH 28/29] s3: add roundtrip test --- runt/bi/runt.toml | 9 +++ scripts/test_catalog.py | 12 +++ .../expects/s3_buggy.bi.expect | 26 ++++++- .../expects/s3_fixed.bi.expect | 7 +- .../expects/s3_fixed_tx.bi.expect | 71 ++++++++++++++++++ .../axis-adapter-s3/s3_fixed.tx | 3 +- .../axis-adapter-s3/s3_fixed_tx.fst | Bin 2924 -> 2923 bytes 7 files changed, 122 insertions(+), 6 deletions(-) create mode 100644 tests/fpga-debugging/axis-adapter-s3/expects/s3_fixed_tx.bi.expect diff --git a/runt/bi/runt.toml b/runt/bi/runt.toml index d450e56b..63d4f7df 100644 --- a/runt/bi/runt.toml +++ b/runt/bi/runt.toml @@ -2394,6 +2394,15 @@ expect_dir = "../../tests/fpga-debugging/axis-adapter-s3/expects" expect_name = "s3_fixed.bi.expect" cmd = "cd ../.. && target/debug/bi --color never --protocol tests/fpga-debugging/axis-adapter-s3/s3.prot --wave tests/fpga-debugging/axis-adapter-s3/s3_fixed.fst --instances TOP.test_axis_adapter_64_8.UUT:AXIS --sample-posedge TOP.test_axis_adapter_64_8.UUT.clk --show-waveform-time --include-idle --time-unit ns --display-hex --allow-branch-on-arg 2>&1" +[[tests]] +name = "bi.tests_fpga_debugging_axis_adapter_s3_s3.s3_fixed_tx_bi" +paths = [ + "../../tests/fpga-debugging/axis-adapter-s3/s3.prot", +] +expect_dir = "../../tests/fpga-debugging/axis-adapter-s3/expects" +expect_name = "s3_fixed_tx.bi.expect" +cmd = "cd ../.. && target/debug/bi --color never --protocol tests/fpga-debugging/axis-adapter-s3/s3.prot --wave tests/fpga-debugging/axis-adapter-s3/s3_fixed_tx.fst --instances dut:AXIS --show-steps --include-idle --display-hex --allow-branch-on-arg 2>&1" + [[tests]] name = "bi.tests_fpga_debugging_axis_async_fifo_c4_c4.c4_buggy_bi" paths = [ diff --git a/scripts/test_catalog.py b/scripts/test_catalog.py index 703522e8..8c048c8e 100644 --- a/scripts/test_catalog.py +++ b/scripts/test_catalog.py @@ -737,6 +737,18 @@ "--allow-branch-on-arg", ), }, + "tests.fpga-debugging.axis-adapter-s3.s3_fixed.on_test_trace": { + "protocol": "tests/fpga-debugging/axis-adapter-s3/s3.prot", + "wave": "tests/fpga-debugging/axis-adapter-s3/s3_fixed_tx.fst", + "instances": ("dut:AXIS",), + "expect": "pass", + "extra_args": ( + "--show-steps", + "--include-idle", + "--display-hex", + "--allow-branch-on-arg", + ), + }, "tests.fpga-debugging.axis-async-fifo-c4.c4_buggy": { "protocol": "tests/fpga-debugging/axis-async-fifo-c4/c4.prot", "wave": "tests/fpga-debugging/axis-async-fifo-c4/c4_buggy.fst", diff --git a/tests/fpga-debugging/axis-adapter-s3/expects/s3_buggy.bi.expect b/tests/fpga-debugging/axis-adapter-s3/expects/s3_buggy.bi.expect index 6cf58529..b22c8c43 100644 --- a/tests/fpga-debugging/axis-adapter-s3/expects/s3_buggy.bi.expect +++ b/tests/fpga-debugging/axis-adapter-s3/expects/s3_buggy.bi.expect @@ -1,14 +1,32 @@ // trace 0 trace { - reset(); // [time: 0ns -> 25ns] + reset(); // [time: 0ns -> 50ns] idle(); // [time: 25ns -> 50ns] idle(); // [time: 50ns -> 75ns] + idle(); // [time: 100ns -> 125ns] + idle(); // [time: 125ns -> 150ns] + idle(); // [time: 150ns -> 175ns] + idle(); // [time: 175ns -> 200ns] } error: [split_word@3] executing step 5 of the transaction: 0 != 1 - ┌─ tests/fpga-debugging/axis-adapter-s3/s3.prot:237:45 + ┌─ tests/fpga-debugging/axis-adapter-s3/s3.prot:284:29 │ -237 │ assert_eq(keep[5], 1'b1); - │ ^^^^^^^^^^^^^^^^^^^^^^^^^ [split_word@3] executing step 5 of the transaction: 0 != 1 +284 │ assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); + │ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ [split_word@3] executing step 5 of the transaction: 0 != 1 + + +error: [split_word@3] executing step 5 of the transaction: 0 != 1 + ┌─ tests/fpga-debugging/axis-adapter-s3/s3.prot:284:29 + │ +284 │ assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); + │ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ [split_word@3] executing step 5 of the transaction: 0 != 1 + + +error: [split_word@3] executing step 5 of the transaction: 0 != 1 + ┌─ tests/fpga-debugging/axis-adapter-s3/s3.prot:284:29 + │ +284 │ assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); + │ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ [split_word@3] executing step 5 of the transaction: 0 != 1 ---CODE--- 1 diff --git a/tests/fpga-debugging/axis-adapter-s3/expects/s3_fixed.bi.expect b/tests/fpga-debugging/axis-adapter-s3/expects/s3_fixed.bi.expect index 3edc3603..9a7036dc 100644 --- a/tests/fpga-debugging/axis-adapter-s3/expects/s3_fixed.bi.expect +++ b/tests/fpga-debugging/axis-adapter-s3/expects/s3_fixed.bi.expect @@ -1,7 +1,12 @@ // trace 0 trace { - reset(); // [time: 0ns -> 25ns] + reset(); // [time: 0ns -> 50ns] idle(); // [time: 25ns -> 50ns] idle(); // [time: 50ns -> 75ns] + idle(); // [time: 100ns -> 125ns] + idle(); // [time: 125ns -> 150ns] + idle(); // [time: 150ns -> 175ns] + idle(); // [time: 175ns -> 200ns] split_word(0xabcdabcdabcdabcd, 0x1f, 0x1); // [time: 75ns -> 200ns] + idle(); // [time: 200ns -> 200ns] } diff --git a/tests/fpga-debugging/axis-adapter-s3/expects/s3_fixed_tx.bi.expect b/tests/fpga-debugging/axis-adapter-s3/expects/s3_fixed_tx.bi.expect new file mode 100644 index 00000000..9a51880f --- /dev/null +++ b/tests/fpga-debugging/axis-adapter-s3/expects/s3_fixed_tx.bi.expect @@ -0,0 +1,71 @@ +// trace 0 +trace { + idle(); [0] + reset(); [1 .. 2] + idle(); [2] + idle(); [4] + idle(); [5] + idle(); [6] + idle(); [7] + split_word(0xabcdabcdabcdabcd, 0x1f, 0x1); [3 .. 8] + idle(); [8] + idle(); [9] + reset(); [10 .. 11] + idle(); [11] + split_word(0x0000000000000011, 0x01, 0x0); [12 .. 13] + split_word(0x0000000000002211, 0x03, 0x0); [13 .. 15] + split_word(0x0000000000332211, 0x07, 0x0); [14 .. 18] + split_word(0x0000000044332211, 0x0f, 0x0); [16 .. 22] + split_word(0x0000005544332211, 0x1f, 0x0); [19 .. 27] + split_word(0x0000665544332211, 0x3f, 0x0); [23 .. 33] + split_word(0x0077665544332211, 0x7f, 0x0); [28 .. 40] + split_word(0x8877665544332211, 0xff, 0x0); [34 .. 48] + split_word(0x0000000000000011, 0x01, 0x0); [41 .. 49] + split_word(0x0000000000002211, 0x03, 0x1); [49 .. 51] + split_word(0x0000000000332211, 0x07, 0x1); [50 .. 54] + split_word(0x0000000044332211, 0x0f, 0x1); [52 .. 58] + split_word(0x0000005544332211, 0x1f, 0x1); [55 .. 63] + split_word(0x0000665544332211, 0x3f, 0x1); [59 .. 69] + split_word(0x0077665544332211, 0x7f, 0x1); [64 .. 76] + idle(); [77] + split_word(0x8877665544332211, 0xff, 0x1); [70 .. 84] + split_word(0x0000000000000011, 0x01, 0x0); [78 .. 85] + idle(); [85] + idle(); [87] + split_word(0x0000000000002211, 0x03, 0x0); [86 .. 88] + idle(); [89] + split_word(0x0000000000332211, 0x07, 0x0); [88 .. 91] + idle(); [92] + split_word(0x0000000044332211, 0x0f, 0x0); [90 .. 95] + idle(); [96] + split_word(0x0000005544332211, 0x1f, 0x0); [93 .. 100] + idle(); [101] + split_word(0x0000665544332211, 0x3f, 0x0); [97 .. 106] + idle(); [107] + split_word(0x0077665544332211, 0x7f, 0x0); [102 .. 113] + idle(); [114] + split_word(0x8877665544332211, 0xff, 0x0); [108 .. 121] + split_word(0x0000000000000011, 0x01, 0x0); [115 .. 122] + idle(); [122] + idle(); [124] + split_word(0x0000000000002211, 0x03, 0x1); [123 .. 125] + idle(); [126] + split_word(0x0000000000332211, 0x07, 0x1); [125 .. 128] + idle(); [129] + split_word(0x0000000044332211, 0x0f, 0x1); [127 .. 132] + idle(); [133] + split_word(0x0000005544332211, 0x1f, 0x1); [130 .. 137] + idle(); [138] + split_word(0x0000665544332211, 0x3f, 0x1); [134 .. 143] + idle(); [144] + split_word(0x0077665544332211, 0x7f, 0x1); [139 .. 150] + idle(); [151] + idle(); [152] + idle(); [153] + idle(); [154] + idle(); [155] + idle(); [156] + idle(); [157] + split_word(0x8877665544332211, 0xff, 0x1); [145 .. 158] + idle(); [158] +} diff --git a/tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx b/tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx index fe97f8f5..1895f1a1 100644 --- a/tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx +++ b/tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx @@ -58,5 +58,6 @@ trace { split_word(0x0077665544332211, 0b01111111, 1); idle(); split_word(0x8877665544332211, 0b11111111, 1); - idle(); + // enough idle transactions to finish the last split_word + idle(); idle(); idle(); idle(); idle(); idle(); idle(); idle(); } diff --git a/tests/fpga-debugging/axis-adapter-s3/s3_fixed_tx.fst b/tests/fpga-debugging/axis-adapter-s3/s3_fixed_tx.fst index c0ff5b0e3329a86916cf395d0d27b04d11cc3c34..ae042ba4f2da61c5047fc907586c9e165543fae4 100644 GIT binary patch delta 185 zcmaDO_F8O%B#T@m11gvg;c`f{v9__sZ+2uk!8kd9g=;e>+Y%M_+4N9n3)6PHoYj3ZtF)O8zmVwYP!?avw0x({gJTVx z6_a0c6sxXgGGKba^nhs|lP^;c1CxLd%RI&sITkh`Y+@8(lVI~;6JVR%!l}We`fc($ YPAOIaHW4<7&1X4-7#R&GD{%V&0A_YIegFUf delta 186 zcmaDY_C{=jB#T@W11gvg;c`f~v9__sZ+2uk!8kd9g=;e>+Y%-_)3sISqbp9dG3m6d zOs@>}3S?TS{@IPSX}bZ_;w-gNu_vErGriKEu-CrqpD)vfpG#DG3!bGjZMVx=-8ZvJ zd-7|JVzoI;_m~u!xS8aca+!WIFbN2;%wsH(V_^frCPo1^2{sQl4mOs_&72xc>OUs0 X<& Date: Thu, 27 Aug 2026 12:06:02 -0400 Subject: [PATCH 29/29] s3: remove from graph interpreter tests --- runt/graph_interp/runt.toml | 27 ------------------- runt/waveform/runt.toml | 27 ------------------- scripts/generate_runt_configs.py | 4 +++ .../expects/s3_fixed.graph_interp.expect | 2 -- .../expects/s3_fixed.waveform.expect | 12 --------- 5 files changed, 4 insertions(+), 68 deletions(-) delete mode 100644 tests/fpga-debugging/axis-adapter-s3/expects/s3_fixed.graph_interp.expect delete mode 100644 tests/fpga-debugging/axis-adapter-s3/expects/s3_fixed.waveform.expect diff --git a/runt/graph_interp/runt.toml b/runt/graph_interp/runt.toml index 0c71e46b..373c5075 100644 --- a/runt/graph_interp/runt.toml +++ b/runt/graph_interp/runt.toml @@ -531,33 +531,6 @@ 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_adapter_s3_s3_fixed.s3_fixed_graph_interp" -paths = [ - "../../tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx", -] -expect_dir = "../../tests/fpga-debugging/axis-adapter-s3/expects" -expect_name = "s3_fixed.graph_interp.expect" -cmd = "cd ../.. && target/debug/graph-interp --transactions tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx --allow-branch-on-arg --verilog tests/fpga-debugging/axis-adapter-s3/s3_fixed.v --protocol tests/fpga-debugging/axis-adapter-s3/s3.prot --module axis_adapter 2>/dev/null" - -[[tests]] -name = "graph_interp.tests_fpga_debugging_axis_adapter_s3_s3_fixed.s3_fixed_graph_interp.contract_edges" -paths = [ - "../../tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx", -] -expect_dir = "../../tests/fpga-debugging/axis-adapter-s3/expects" -expect_name = "s3_fixed.graph_interp.expect" -cmd = "cd ../.. && target/debug/graph-interp --transactions tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx --allow-branch-on-arg --verilog tests/fpga-debugging/axis-adapter-s3/s3_fixed.v --protocol tests/fpga-debugging/axis-adapter-s3/s3.prot --module axis_adapter --contract-edges 2>/dev/null" - -[[tests]] -name = "graph_interp.tests_fpga_debugging_axis_adapter_s3_s3_fixed.s3_fixed_graph_interp.respect_forks" -paths = [ - "../../tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx", -] -expect_dir = "../../tests/fpga-debugging/axis-adapter-s3/expects" -expect_name = "s3_fixed.graph_interp.expect" -cmd = "cd ../.. && target/debug/graph-interp --transactions tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx --allow-branch-on-arg --verilog tests/fpga-debugging/axis-adapter-s3/s3_fixed.v --protocol tests/fpga-debugging/axis-adapter-s3/s3.prot --module axis_adapter --respect-forks --determinize 2>/dev/null" - [[tests]] name = "graph_interp.tests_fpga_debugging_axis_async_fifo_c4_c4_fixed.c4_fixed_graph_interp" paths = [ diff --git a/runt/waveform/runt.toml b/runt/waveform/runt.toml index 15fd8bfd..579c1232 100644 --- a/runt/waveform/runt.toml +++ b/runt/waveform/runt.toml @@ -675,33 +675,6 @@ 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 --bound 6 --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_adapter_s3_s3_fixed.s3_fixed_waveform.ast" -paths = [ - "../../tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx", -] -expect_dir = "../../tests/fpga-debugging/axis-adapter-s3/expects" -expect_name = "s3_fixed.waveform.expect" -cmd = "cd ../.. && target/debug/protocols-interp --color never --transactions tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx --ascii-waveform --allow-branch-on-arg --verilog tests/fpga-debugging/axis-adapter-s3/s3_fixed.v --protocol tests/fpga-debugging/axis-adapter-s3/s3.prot --module axis_adapter 2>/dev/null" - -[[tests]] -name = "waveform.tests_fpga_debugging_axis_adapter_s3_s3_fixed.s3_fixed_waveform.graph" -paths = [ - "../../tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx", -] -expect_dir = "../../tests/fpga-debugging/axis-adapter-s3/expects" -expect_name = "s3_fixed.waveform.expect" -cmd = "cd ../.. && target/debug/graph-interp --transactions tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx --respect-forks --determinize --ascii-waveform --allow-branch-on-arg --verilog tests/fpga-debugging/axis-adapter-s3/s3_fixed.v --protocol tests/fpga-debugging/axis-adapter-s3/s3.prot --module axis_adapter 2>/dev/null" - -[[tests]] -name = "waveform.tests_fpga_debugging_axis_adapter_s3_s3_fixed.s3_fixed_waveform.ts" -paths = [ - "../../tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx", -] -expect_dir = "../../tests/fpga-debugging/axis-adapter-s3/expects" -expect_name = "s3_fixed.waveform.expect" -cmd = "cd ../.. && target/debug/graph-interp --transactions tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx --transition-system --ascii-waveform --allow-branch-on-arg --verilog tests/fpga-debugging/axis-adapter-s3/s3_fixed.v --protocol tests/fpga-debugging/axis-adapter-s3/s3.prot --module axis_adapter 2>/dev/null" - [[tests]] name = "waveform.tests_fpga_debugging_axis_async_fifo_c4_c4_fixed.c4_fixed_waveform.ast" paths = [ diff --git a/scripts/generate_runt_configs.py b/scripts/generate_runt_configs.py index 97f4dc62..401c649d 100644 --- a/scripts/generate_runt_configs.py +++ b/scripts/generate_runt_configs.py @@ -360,6 +360,10 @@ def graph_interp_cases(cases: list[dict]) -> list[dict]: if c["expected"] == "pass" and not graph_interp_unsupported & protocol_constructs(c["protocol_path"]) ] + # exclude s3 from graph_interp cases + # TODO: re-include + selected = [c for c in selected if not c["protocol_path"].endswith("s3.prot")] + return sorted(selected, key=lambda c: c["paths"][0]) diff --git a/tests/fpga-debugging/axis-adapter-s3/expects/s3_fixed.graph_interp.expect b/tests/fpga-debugging/axis-adapter-s3/expects/s3_fixed.graph_interp.expect deleted file mode 100644 index 57404ebb..00000000 --- a/tests/fpga-debugging/axis-adapter-s3/expects/s3_fixed.graph_interp.expect +++ /dev/null @@ -1,2 +0,0 @@ ----CODE--- -2 diff --git a/tests/fpga-debugging/axis-adapter-s3/expects/s3_fixed.waveform.expect b/tests/fpga-debugging/axis-adapter-s3/expects/s3_fixed.waveform.expect deleted file mode 100644 index fcba3353..00000000 --- a/tests/fpga-debugging/axis-adapter-s3/expects/s3_fixed.waveform.expect +++ /dev/null @@ -1,12 +0,0 @@ -Trace 0 executed successfully! -output_axis_tready x x x 1 1 1 1 1 -input_axis_tlast x x 1 x x x x x -input_axis_tvalid 0 0 1 0 0 0 0 0 -input_axis_tkeep[7:0] x x 31 x x x x x -input_axis_tdata[63:0] x x 12379739850550389709 x x x x x -rst 1 0 0 0 0 0 0 0 -output_axis_tlast 0 0 0 0 0 0 0 1 -output_axis_tvalid 0 0 0 1 1 1 1 1 -output_axis_tkeep 0 0 0 1 1 1 1 1 -output_axis_tdata[7:0] 0 0 0 205 171 205 171 205 -input_axis_tready 0 0 1 0 0 0 0 1