From 97e39bf7e0840d26d429148f588168d8304a8b16 Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Sun, 5 Jul 2026 13:58:31 -0400 Subject: [PATCH 01/13] update gitignore --- .gitignore | 1 + 1 file changed, 1 insertion(+) diff --git a/.gitignore b/.gitignore index 20fbc471..6d40fff4 100644 --- a/.gitignore +++ b/.gitignore @@ -36,3 +36,4 @@ scripts/_catalog_gen.py !tests/fpga-debugging/axis-async-fifo-c4/*.png /*.fst +scripts/__pycache__/ From 36943358bd2292c4e17ceefea14edeaa610206aa Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Sun, 5 Jul 2026 14:28:14 -0400 Subject: [PATCH 02/13] Add version of axi-lite-s1 protocol suitable for driving via interpreter --- .../fpga-debugging/axi-lite-s1/s1_interp.prot | 121 ++++++++++++++++++ 1 file changed, 121 insertions(+) create mode 100644 tests/fpga-debugging/axi-lite-s1/s1_interp.prot diff --git a/tests/fpga-debugging/axi-lite-s1/s1_interp.prot b/tests/fpga-debugging/axi-lite-s1/s1_interp.prot new file mode 100644 index 00000000..fd060321 --- /dev/null +++ b/tests/fpga-debugging/axi-lite-s1/s1_interp.prot @@ -0,0 +1,121 @@ +// Modified version of the protocol for the `axi-lite-s1` Brave New World example. +// This file is largely similar to `s1_buggy.prot` / `s1_fixed.prot`, +// except it only contains one struct. +// The AST interpreter currently rejects .prot files containing multiple +// structs, so we keep only the `WriteSubordinate` struct in this file +// (since the bug is only related to write requests). + +struct WriteSubordinate { + // Active-low reset + in S_AXI_ARESETN: u1, + + // Write address channel + in S_AXI_AWVALID: u1, + in S_AXI_AWADDR: u7, + out S_AXI_AWREADY: u1, + + // Write data channel + in S_AXI_WVALID: u1, + in S_AXI_WDATA: u32, + out S_AXI_WREADY: u1, + + // Write response channel + in S_AXI_BREADY: u1, + out S_AXI_BVALID: u1, + out S_AXI_BRESP: u2, +} + +prot reset() { + // Reset is active-low + DUT.S_AXI_ARESETN := 1'b0; + + // Set valid = 0 for the write data / write address channels + DUT.S_AXI_AWVALID := 1'b0; + DUT.S_AXI_WVALID := 1'b0; + + // Set ready = 0 for write response + DUT.S_AXI_BREADY := 1'b0; + + step(); +} + +// Write transaction where the manager waits `n` cycles before setting AWVALID = 1 +// and stalls the response channel for `n` cycles before setting BREADY = 1. +// The `resp` argument is a 2-bit pattern containing the subordinate's response +// to the write request (indicating whether the transaction succeeded). +prot write(addr: u7, data: u32, resp: u2, n: uint) { + // Reset is active-low + DUT.S_AXI_ARESETN := 1'b1; + + // Wait for `n` cycles before starting write request + DUT.S_AXI_AWVALID := 1'b0; + repeat n iterations { + step(); + } + DUT.S_AXI_AWVALID := 1'b1; + DUT.S_AXI_AWADDR := addr; + + DUT.S_AXI_WVALID := 1'b1; + DUT.S_AXI_WDATA := data; + + // Technically this should be `while !AWREADY && !WREADY { step() }`, + // but our DSL doesn't have `&&`. Without loss of generality, + // we wait for AWREADY to become 1 + while !(DUT.S_AXI_AWREADY == 1'b1) { + step(); + } + // Here we're assuming AWREADY & WREADY become 1 together + // (this is allowed in the AXI spec and the DUT exhibits this behavior) + assert_eq(DUT.S_AXI_WREADY, 1'b1); + + step(); + + // The data transfer for the write address + write data is done, + // so we set these channels to `DontCare` + DUT.S_AXI_AWVALID := X; + DUT.S_AXI_WVALID := X; + DUT.S_AXI_AWADDR := X; + DUT.S_AXI_WDATA := X; + + // We use `fork` to indicate that another transaction can begin concurrently + // According to B1.1.4 of the AXI-Lite spec, a manager can send a + // new write request while awaiting a response for a previous request, + // but it is the subordinate's responsibility to acknowledge these + // requests in the order they were issued. + fork(); + + // Wait BVALID to become 1 + // Before BVALID becomes 1, we have to keep BVALID = 0 + DUT.S_AXI_BREADY := 1'b0; + while !(DUT.S_AXI_BVALID == 1'b1) { + step(); + } + // BVALID is now 1 + // Wait `n` cycles before asserting BREADY + repeat n iterations { + step(); + // BVALID must remain stable after it becomes 1 + assert_eq(DUT.S_AXI_BVALID, 1'b1); + } + // Assert BREADY and check that the response is transffered + DUT.S_AXI_BREADY := 1'b1; + assert_eq(DUT.S_AXI_BRESP, resp); + step(); + + // Set BREADY back to 0 + // (transaction is over so there is no data on the response channel) + DUT.S_AXI_BREADY := 1'b0; + step(); +} + +#[idle] +prot idle() { + // Reset is active-low, so we set reset = 1 here + // to indicate that the DUT is *not* reset during an `idle` transaction + DUT.S_AXI_ARESETN := 1'b1; + DUT.S_AXI_AWVALID := 1'b0; + DUT.S_AXI_AWADDR := X; + DUT.S_AXI_WVALID := 1'b0; + DUT.S_AXI_WDATA := X; + step(); +} From 09e559aa7c3de71e966be45b0130db01fc3dd1fc Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Sun, 5 Jul 2026 14:58:06 -0400 Subject: [PATCH 03/13] Propagate updates to s1_buggy/fixed.prot --- .../fpga-debugging/axi-lite-s1/s1_buggy.prot | 164 ++++++------------ .../fpga-debugging/axi-lite-s1/s1_fixed.prot | 164 ++++++------------ 2 files changed, 102 insertions(+), 226 deletions(-) diff --git a/tests/fpga-debugging/axi-lite-s1/s1_buggy.prot b/tests/fpga-debugging/axi-lite-s1/s1_buggy.prot index 2063b7e6..75ce47f6 100644 --- a/tests/fpga-debugging/axi-lite-s1/s1_buggy.prot +++ b/tests/fpga-debugging/axi-lite-s1/s1_buggy.prot @@ -1,16 +1,7 @@ -struct ReadSubordinate { - // Read address channel - in S_AXI_ARVALID: u1, - in S_AXI_ARADDR: u7, - out S_AXI_ARREADY: u1, - - // Read data channel - in S_AXI_RREADY: u1, - out S_AXI_RVALID: u1, - out S_AXI_RDATA: u32, -} - struct WriteSubordinate { + // Active-low reset + in S_AXI_ARESETN: u1, + // Write address channel in S_AXI_AWVALID: u1, in S_AXI_AWADDR: u7, @@ -27,11 +18,31 @@ struct WriteSubordinate { out S_AXI_BRESP: u2, } -// Note: this is still WIP (this is simpler than the protocol we discussed -// yesterday for ease of debugging for now) +prot reset() { + // Reset is active-low + DUT.S_AXI_ARESETN := 1'b0; + + // Set valid = 0 for the write data / write address channels + DUT.S_AXI_AWVALID := 1'b0; + DUT.S_AXI_WVALID := 1'b0; + + // Set ready = 0 for write response + DUT.S_AXI_BREADY := 1'b0; + + step(); +} + +// Write transaction where the manager waits `n` cycles before setting AWVALID = 1 +// and stalls the response channel for `n` cycles before setting BREADY = 1. +// The `resp` argument is a 2-bit pattern containing the subordinate's response +// to the write request (indicating whether the transaction succeeded). prot write(addr: u7, data: u32, resp: u2, n: uint) { + // Reset is active-low + DUT.S_AXI_ARESETN := 1'b1; + + // Wait for `n` cycles before starting write request + DUT.S_AXI_AWVALID := 1'b0; repeat n iterations { - DUT.S_AXI_AWVALID := 1'b0; step(); } DUT.S_AXI_AWVALID := 1'b1; @@ -40,137 +51,64 @@ prot write(addr: u7, data: u32, resp: u2, n: uint) { DUT.S_AXI_WVALID := 1'b1; DUT.S_AXI_WDATA := data; - // technically this should be `while !AWREADY && !WREADY { step() }` + // Technically this should be `while !AWREADY && !WREADY { step() }`, // but our DSL doesn't have `&&`. Without loss of generality, // we wait for AWREADY to become 1 while !(DUT.S_AXI_AWREADY == 1'b1) { step(); } - // Assuming AWREADY & WREADY become 1 together + // Here we're assuming AWREADY & WREADY become 1 together // (this is allowed in the AXI spec and the DUT exhibits this behavior) assert_eq(DUT.S_AXI_WREADY, 1'b1); step(); - // Remove constraints on AWVALID and WVALID + // The data transfer for the write address + write data is done, + // so we set these channels to `DontCare` DUT.S_AXI_AWVALID := X; DUT.S_AXI_WVALID := X; - - // Wait for BVALID to become 1 + DUT.S_AXI_AWADDR := X; + DUT.S_AXI_WDATA := X; + + // We use `fork` to indicate that another transaction can begin concurrently + // According to B1.1.4 of the AXI-Lite spec, a manager can send a + // new write request while awaiting a response for a previous request, + // but it is the subordinate's responsibility to acknowledge these + // requests in the order they were issued. + fork(); + + // Wait BVALID to become 1 + // Before BVALID becomes 1, we have to keep BVALID = 0 + DUT.S_AXI_BREADY := 1'b0; while !(DUT.S_AXI_BVALID == 1'b1) { step(); } // BVALID is now 1 - // Wait for some no. of cycles before BREADY becomes 1 + // Wait `n` cycles before asserting BREADY repeat n iterations { step(); // BVALID must remain stable after it becomes 1 assert_eq(DUT.S_AXI_BVALID, 1'b1); } + // Assert BREADY and check that the response is transffered DUT.S_AXI_BREADY := 1'b1; assert_eq(DUT.S_AXI_BRESP, resp); step(); -} - -#[idle] -prot idle() { - DUT.S_AXI_ARVALID := 1'b0; - DUT.S_AXI_ARADDR := X; - DUT.S_AXI_RREADY := 1'b0; + // Set BREADY back to 0 + // (transaction is over so there is no data on the response channel) + DUT.S_AXI_BREADY := 1'b0; step(); } #[idle] prot idle() { + // Reset is active-low, so we set reset = 1 here + // to indicate that the DUT is *not* reset during an `idle` transaction + DUT.S_AXI_ARESETN := 1'b1; DUT.S_AXI_AWVALID := 1'b0; DUT.S_AXI_AWADDR := X; DUT.S_AXI_WVALID := 1'b0; DUT.S_AXI_WDATA := X; step(); } - -// RREADY is asserted before RVALID -// (This is allowed in section A2.3.2.2 of the AXI spec) -prot read_v1(addr: u7, data: u32) { - DUT.S_AXI_ARVALID := 1'b1; - DUT.S_AXI_ARADDR := addr; - - // Wait for ARREADY to become 1 - while !(DUT.S_AXI_ARREADY == 1'b1) { - step(); - } - // ARREADY is now 1 - - step(); - - // While we are waiting for RREADY to become 1, - // another read address request cannot arrive - // (i.e. ARREADY has to remain 0). That is, we have to acknowledge - // the read data before another read address request can arrive. - assert_eq(DUT.S_AXI_ARREADY, 1'b0); - - // Once ARREADY is de-asserted, ARVALID is allowed to be any value - DUT.S_AXI_ARVALID := X; - - // Manager sets RREADY to 1 to begin transfer on read data channel - DUT.S_AXI_RREADY := 1'b1; - - // Wait for RVALID to become 1 - // AXI spec says that ARVALID & ARREADY must both be 1 - // before RVALID can be asserted (A2.3.2.2) - while !(DUT.S_AXI_RVALID == 1'b1) { - step(); - assert_eq(DUT.S_AXI_ARREADY, 1'b0); - } - assert_eq(DUT.S_AXI_RDATA, data); - step(); -} - -// RVALID is asserted before RREADY -// (This is allowed in section A2.3.2.2 of the AXI spec) -prot read_v2(addr: u7, data: u32, n: uint) { - DUT.S_AXI_ARVALID := 1'b1; - DUT.S_AXI_ARADDR := addr; - - // Wait for ARREADY to become 1 - while !(DUT.S_AXI_ARREADY == 1'b1) { - step(); - } - // ARREADY is now 1 - - step(); - - // Wait for RVALID to become 1 - // AXI spec says that ARVALID & ARREADY must both be 1 - // before RVALID can be asserted (A2.3.2.2) - while !(DUT.S_AXI_RVALID == 1'b1) { - step(); - } - // RVALID is now 1 - - // While we are waiting for RREADY to become 1, - // another read address request cannot arrive - // (i.e. ARREADY has to remain 0). That is, we have to acknowledge - // the read data before another read address request can arrive. - assert_eq(DUT.S_AXI_ARREADY, 1'b0); - - // Once ARREADY is de-asserted, ARVALID is allowed to be any value - DUT.S_AXI_ARVALID := X; - - // Wait until RREADY becomes 1 - repeat n iterations { - DUT.S_AXI_RREADY := 1'b0; - // Check that RVALID remains stable - assert_eq(DUT.S_AXI_RVALID, 1'b1); - step(); - } - // Check that ARREADY remains 0 (i.e. no conflicting read address request) - assert_eq(DUT.S_AXI_ARREADY, 1'b0); - - // Perform data transfer on the read data channel - DUT.S_AXI_RREADY := 1'b1; - assert_eq(DUT.S_AXI_RDATA, data); - - step(); -} diff --git a/tests/fpga-debugging/axi-lite-s1/s1_fixed.prot b/tests/fpga-debugging/axi-lite-s1/s1_fixed.prot index 2063b7e6..75ce47f6 100644 --- a/tests/fpga-debugging/axi-lite-s1/s1_fixed.prot +++ b/tests/fpga-debugging/axi-lite-s1/s1_fixed.prot @@ -1,16 +1,7 @@ -struct ReadSubordinate { - // Read address channel - in S_AXI_ARVALID: u1, - in S_AXI_ARADDR: u7, - out S_AXI_ARREADY: u1, - - // Read data channel - in S_AXI_RREADY: u1, - out S_AXI_RVALID: u1, - out S_AXI_RDATA: u32, -} - struct WriteSubordinate { + // Active-low reset + in S_AXI_ARESETN: u1, + // Write address channel in S_AXI_AWVALID: u1, in S_AXI_AWADDR: u7, @@ -27,11 +18,31 @@ struct WriteSubordinate { out S_AXI_BRESP: u2, } -// Note: this is still WIP (this is simpler than the protocol we discussed -// yesterday for ease of debugging for now) +prot reset() { + // Reset is active-low + DUT.S_AXI_ARESETN := 1'b0; + + // Set valid = 0 for the write data / write address channels + DUT.S_AXI_AWVALID := 1'b0; + DUT.S_AXI_WVALID := 1'b0; + + // Set ready = 0 for write response + DUT.S_AXI_BREADY := 1'b0; + + step(); +} + +// Write transaction where the manager waits `n` cycles before setting AWVALID = 1 +// and stalls the response channel for `n` cycles before setting BREADY = 1. +// The `resp` argument is a 2-bit pattern containing the subordinate's response +// to the write request (indicating whether the transaction succeeded). prot write(addr: u7, data: u32, resp: u2, n: uint) { + // Reset is active-low + DUT.S_AXI_ARESETN := 1'b1; + + // Wait for `n` cycles before starting write request + DUT.S_AXI_AWVALID := 1'b0; repeat n iterations { - DUT.S_AXI_AWVALID := 1'b0; step(); } DUT.S_AXI_AWVALID := 1'b1; @@ -40,137 +51,64 @@ prot write(addr: u7, data: u32, resp: u2, n: uint) { DUT.S_AXI_WVALID := 1'b1; DUT.S_AXI_WDATA := data; - // technically this should be `while !AWREADY && !WREADY { step() }` + // Technically this should be `while !AWREADY && !WREADY { step() }`, // but our DSL doesn't have `&&`. Without loss of generality, // we wait for AWREADY to become 1 while !(DUT.S_AXI_AWREADY == 1'b1) { step(); } - // Assuming AWREADY & WREADY become 1 together + // Here we're assuming AWREADY & WREADY become 1 together // (this is allowed in the AXI spec and the DUT exhibits this behavior) assert_eq(DUT.S_AXI_WREADY, 1'b1); step(); - // Remove constraints on AWVALID and WVALID + // The data transfer for the write address + write data is done, + // so we set these channels to `DontCare` DUT.S_AXI_AWVALID := X; DUT.S_AXI_WVALID := X; - - // Wait for BVALID to become 1 + DUT.S_AXI_AWADDR := X; + DUT.S_AXI_WDATA := X; + + // We use `fork` to indicate that another transaction can begin concurrently + // According to B1.1.4 of the AXI-Lite spec, a manager can send a + // new write request while awaiting a response for a previous request, + // but it is the subordinate's responsibility to acknowledge these + // requests in the order they were issued. + fork(); + + // Wait BVALID to become 1 + // Before BVALID becomes 1, we have to keep BVALID = 0 + DUT.S_AXI_BREADY := 1'b0; while !(DUT.S_AXI_BVALID == 1'b1) { step(); } // BVALID is now 1 - // Wait for some no. of cycles before BREADY becomes 1 + // Wait `n` cycles before asserting BREADY repeat n iterations { step(); // BVALID must remain stable after it becomes 1 assert_eq(DUT.S_AXI_BVALID, 1'b1); } + // Assert BREADY and check that the response is transffered DUT.S_AXI_BREADY := 1'b1; assert_eq(DUT.S_AXI_BRESP, resp); step(); -} - -#[idle] -prot idle() { - DUT.S_AXI_ARVALID := 1'b0; - DUT.S_AXI_ARADDR := X; - DUT.S_AXI_RREADY := 1'b0; + // Set BREADY back to 0 + // (transaction is over so there is no data on the response channel) + DUT.S_AXI_BREADY := 1'b0; step(); } #[idle] prot idle() { + // Reset is active-low, so we set reset = 1 here + // to indicate that the DUT is *not* reset during an `idle` transaction + DUT.S_AXI_ARESETN := 1'b1; DUT.S_AXI_AWVALID := 1'b0; DUT.S_AXI_AWADDR := X; DUT.S_AXI_WVALID := 1'b0; DUT.S_AXI_WDATA := X; step(); } - -// RREADY is asserted before RVALID -// (This is allowed in section A2.3.2.2 of the AXI spec) -prot read_v1(addr: u7, data: u32) { - DUT.S_AXI_ARVALID := 1'b1; - DUT.S_AXI_ARADDR := addr; - - // Wait for ARREADY to become 1 - while !(DUT.S_AXI_ARREADY == 1'b1) { - step(); - } - // ARREADY is now 1 - - step(); - - // While we are waiting for RREADY to become 1, - // another read address request cannot arrive - // (i.e. ARREADY has to remain 0). That is, we have to acknowledge - // the read data before another read address request can arrive. - assert_eq(DUT.S_AXI_ARREADY, 1'b0); - - // Once ARREADY is de-asserted, ARVALID is allowed to be any value - DUT.S_AXI_ARVALID := X; - - // Manager sets RREADY to 1 to begin transfer on read data channel - DUT.S_AXI_RREADY := 1'b1; - - // Wait for RVALID to become 1 - // AXI spec says that ARVALID & ARREADY must both be 1 - // before RVALID can be asserted (A2.3.2.2) - while !(DUT.S_AXI_RVALID == 1'b1) { - step(); - assert_eq(DUT.S_AXI_ARREADY, 1'b0); - } - assert_eq(DUT.S_AXI_RDATA, data); - step(); -} - -// RVALID is asserted before RREADY -// (This is allowed in section A2.3.2.2 of the AXI spec) -prot read_v2(addr: u7, data: u32, n: uint) { - DUT.S_AXI_ARVALID := 1'b1; - DUT.S_AXI_ARADDR := addr; - - // Wait for ARREADY to become 1 - while !(DUT.S_AXI_ARREADY == 1'b1) { - step(); - } - // ARREADY is now 1 - - step(); - - // Wait for RVALID to become 1 - // AXI spec says that ARVALID & ARREADY must both be 1 - // before RVALID can be asserted (A2.3.2.2) - while !(DUT.S_AXI_RVALID == 1'b1) { - step(); - } - // RVALID is now 1 - - // While we are waiting for RREADY to become 1, - // another read address request cannot arrive - // (i.e. ARREADY has to remain 0). That is, we have to acknowledge - // the read data before another read address request can arrive. - assert_eq(DUT.S_AXI_ARREADY, 1'b0); - - // Once ARREADY is de-asserted, ARVALID is allowed to be any value - DUT.S_AXI_ARVALID := X; - - // Wait until RREADY becomes 1 - repeat n iterations { - DUT.S_AXI_RREADY := 1'b0; - // Check that RVALID remains stable - assert_eq(DUT.S_AXI_RVALID, 1'b1); - step(); - } - // Check that ARREADY remains 0 (i.e. no conflicting read address request) - assert_eq(DUT.S_AXI_ARREADY, 1'b0); - - // Perform data transfer on the read data channel - DUT.S_AXI_RREADY := 1'b1; - assert_eq(DUT.S_AXI_RDATA, data); - - step(); -} From 8b7f3c7f515a4ec551c544ea9c8e5d1cbb902653 Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Sun, 5 Jul 2026 14:58:19 -0400 Subject: [PATCH 04/13] Remove unnecessary .prot file --- .../fpga-debugging/axi-lite-s1/s1_interp.prot | 121 ------------------ 1 file changed, 121 deletions(-) delete mode 100644 tests/fpga-debugging/axi-lite-s1/s1_interp.prot diff --git a/tests/fpga-debugging/axi-lite-s1/s1_interp.prot b/tests/fpga-debugging/axi-lite-s1/s1_interp.prot deleted file mode 100644 index fd060321..00000000 --- a/tests/fpga-debugging/axi-lite-s1/s1_interp.prot +++ /dev/null @@ -1,121 +0,0 @@ -// Modified version of the protocol for the `axi-lite-s1` Brave New World example. -// This file is largely similar to `s1_buggy.prot` / `s1_fixed.prot`, -// except it only contains one struct. -// The AST interpreter currently rejects .prot files containing multiple -// structs, so we keep only the `WriteSubordinate` struct in this file -// (since the bug is only related to write requests). - -struct WriteSubordinate { - // Active-low reset - in S_AXI_ARESETN: u1, - - // Write address channel - in S_AXI_AWVALID: u1, - in S_AXI_AWADDR: u7, - out S_AXI_AWREADY: u1, - - // Write data channel - in S_AXI_WVALID: u1, - in S_AXI_WDATA: u32, - out S_AXI_WREADY: u1, - - // Write response channel - in S_AXI_BREADY: u1, - out S_AXI_BVALID: u1, - out S_AXI_BRESP: u2, -} - -prot reset() { - // Reset is active-low - DUT.S_AXI_ARESETN := 1'b0; - - // Set valid = 0 for the write data / write address channels - DUT.S_AXI_AWVALID := 1'b0; - DUT.S_AXI_WVALID := 1'b0; - - // Set ready = 0 for write response - DUT.S_AXI_BREADY := 1'b0; - - step(); -} - -// Write transaction where the manager waits `n` cycles before setting AWVALID = 1 -// and stalls the response channel for `n` cycles before setting BREADY = 1. -// The `resp` argument is a 2-bit pattern containing the subordinate's response -// to the write request (indicating whether the transaction succeeded). -prot write(addr: u7, data: u32, resp: u2, n: uint) { - // Reset is active-low - DUT.S_AXI_ARESETN := 1'b1; - - // Wait for `n` cycles before starting write request - DUT.S_AXI_AWVALID := 1'b0; - repeat n iterations { - step(); - } - DUT.S_AXI_AWVALID := 1'b1; - DUT.S_AXI_AWADDR := addr; - - DUT.S_AXI_WVALID := 1'b1; - DUT.S_AXI_WDATA := data; - - // Technically this should be `while !AWREADY && !WREADY { step() }`, - // but our DSL doesn't have `&&`. Without loss of generality, - // we wait for AWREADY to become 1 - while !(DUT.S_AXI_AWREADY == 1'b1) { - step(); - } - // Here we're assuming AWREADY & WREADY become 1 together - // (this is allowed in the AXI spec and the DUT exhibits this behavior) - assert_eq(DUT.S_AXI_WREADY, 1'b1); - - step(); - - // The data transfer for the write address + write data is done, - // so we set these channels to `DontCare` - DUT.S_AXI_AWVALID := X; - DUT.S_AXI_WVALID := X; - DUT.S_AXI_AWADDR := X; - DUT.S_AXI_WDATA := X; - - // We use `fork` to indicate that another transaction can begin concurrently - // According to B1.1.4 of the AXI-Lite spec, a manager can send a - // new write request while awaiting a response for a previous request, - // but it is the subordinate's responsibility to acknowledge these - // requests in the order they were issued. - fork(); - - // Wait BVALID to become 1 - // Before BVALID becomes 1, we have to keep BVALID = 0 - DUT.S_AXI_BREADY := 1'b0; - while !(DUT.S_AXI_BVALID == 1'b1) { - step(); - } - // BVALID is now 1 - // Wait `n` cycles before asserting BREADY - repeat n iterations { - step(); - // BVALID must remain stable after it becomes 1 - assert_eq(DUT.S_AXI_BVALID, 1'b1); - } - // Assert BREADY and check that the response is transffered - DUT.S_AXI_BREADY := 1'b1; - assert_eq(DUT.S_AXI_BRESP, resp); - step(); - - // Set BREADY back to 0 - // (transaction is over so there is no data on the response channel) - DUT.S_AXI_BREADY := 1'b0; - step(); -} - -#[idle] -prot idle() { - // Reset is active-low, so we set reset = 1 here - // to indicate that the DUT is *not* reset during an `idle` transaction - DUT.S_AXI_ARESETN := 1'b1; - DUT.S_AXI_AWVALID := 1'b0; - DUT.S_AXI_AWADDR := X; - DUT.S_AXI_WVALID := 1'b0; - DUT.S_AXI_WDATA := X; - step(); -} From ca552a80cfa9bd3330aff37fa461b46f333dce6b Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Sun, 5 Jul 2026 15:05:17 -0400 Subject: [PATCH 05/13] Add .tx files --- tests/fpga-debugging/axi-lite-s1/s1_buggy.tx | 13 +++++++++++++ tests/fpga-debugging/axi-lite-s1/s1_fixed.tx | 9 +++++++++ 2 files changed, 22 insertions(+) create mode 100644 tests/fpga-debugging/axi-lite-s1/s1_buggy.tx create mode 100644 tests/fpga-debugging/axi-lite-s1/s1_fixed.tx diff --git a/tests/fpga-debugging/axi-lite-s1/s1_buggy.tx b/tests/fpga-debugging/axi-lite-s1/s1_buggy.tx new file mode 100644 index 00000000..a60a148d --- /dev/null +++ b/tests/fpga-debugging/axi-lite-s1/s1_buggy.tx @@ -0,0 +1,13 @@ +// In the first write transaction, the manager waits 4 cycles before issuing a response +// (last argument to the `write` transaction). +// The second write transaction is pipelined and begins +// when the first `write` transaction calls `fork`. +// The buggy DUT only acknowledges the first write request +// and ignores the second one. +// Our interpreter emits an error message saying +// there are conflicting assignments to `BREADY`. +trace { + reset(); + write(4, 42, 0, 4); + write(8, 7, 0, 0); +} diff --git a/tests/fpga-debugging/axi-lite-s1/s1_fixed.tx b/tests/fpga-debugging/axi-lite-s1/s1_fixed.tx new file mode 100644 index 00000000..1edf625a --- /dev/null +++ b/tests/fpga-debugging/axi-lite-s1/s1_fixed.tx @@ -0,0 +1,9 @@ +// This is the same transaction trace as s1_buggy.tx, +// but the DUT is fixed, so it doesn't accept the second +// write transaction until the first one is acknowledged. +// Our interpreter executes this list of transcations successfully. +trace { + reset(); + write(4, 42, 0, 4); + write(8, 7, 0, 0); +} From b8405038be5cced0972e03e32b0a791bc3e93812 Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Sun, 5 Jul 2026 15:09:20 -0400 Subject: [PATCH 06/13] Update Runt + add expect test outputs --- runt/interp/runt.toml | 18 ++++++++++++ runt/monitor/runt.toml | 4 +-- scripts/test_catalog.py | 29 +++++++++++++------ .../expects/s1_buggy.interp.expect | 15 ++++++++++ .../expects/s1_fixed.interp.expect | 1 + .../expects/s1_fixed.monitor.expect | 10 ++----- .../fpga-debugging/axi-lite-s1/s1_buggy.prot | 5 ++-- 7 files changed, 61 insertions(+), 21 deletions(-) create mode 100644 tests/fpga-debugging/axi-lite-s1/expects/s1_buggy.interp.expect create mode 100644 tests/fpga-debugging/axi-lite-s1/expects/s1_fixed.interp.expect diff --git a/runt/interp/runt.toml b/runt/interp/runt.toml index 23b631a7..13a0223e 100644 --- a/runt/interp/runt.toml +++ b/runt/interp/runt.toml @@ -495,6 +495,24 @@ expect_dir = "../../tests/fifo/expects" expect_name = "push_pop_loop_not_empty.interp.expect" cmd = "cd ../.. && target/debug/protocols-interp --color never --transactions tests/fifo/push_pop_loop_not_empty.tx --verilog tests/fifo/bsg_mem_1rw_sync.v tests/fifo/bsg_mem_1rw_sync_synth.v tests/fifo/bsg_circular_ptr.v tests/fifo/bsg_fifo_1rw_large.v tests/fifo/fifo_wrapper.v --protocol tests/fifo/fifo_bounded_loop.prot --module fifo_wrapper 2>&1" +[[tests]] +name = "interp.tests_fpga_debugging_axi_lite_s1_s1_buggy.s1_buggy_interp" +paths = [ + "../../tests/fpga-debugging/axi-lite-s1/s1_buggy.tx", +] +expect_dir = "../../tests/fpga-debugging/axi-lite-s1/expects" +expect_name = "s1_buggy.interp.expect" +cmd = "cd ../.. && target/debug/protocols-interp --color never --transactions tests/fpga-debugging/axi-lite-s1/s1_buggy.tx --verilog tests/fpga-debugging/axi-lite-s1/s1_buggy.v --protocol tests/fpga-debugging/axi-lite-s1/s1_buggy.prot --module xlnxdemo --max-steps 300 2>&1" + +[[tests]] +name = "interp.tests_fpga_debugging_axi_lite_s1_s1_fixed.s1_fixed_interp" +paths = [ + "../../tests/fpga-debugging/axi-lite-s1/s1_fixed.tx", +] +expect_dir = "../../tests/fpga-debugging/axi-lite-s1/expects" +expect_name = "s1_fixed.interp.expect" +cmd = "cd ../.. && target/debug/protocols-interp --color never --transactions tests/fpga-debugging/axi-lite-s1/s1_fixed.tx --verilog tests/fpga-debugging/axi-lite-s1/s1_fixed.v --protocol tests/fpga-debugging/axi-lite-s1/s1_fixed.prot --module xlnxdemo --max-steps 300 2>&1" + [[tests]] name = "interp.tests_identities_dual_identity_d0_dual_identity_d0_combdep.dual_identity_d0_combdep_interp" paths = [ diff --git a/runt/monitor/runt.toml b/runt/monitor/runt.toml index aee94652..14513f8c 100644 --- a/runt/monitor/runt.toml +++ b/runt/monitor/runt.toml @@ -1240,7 +1240,7 @@ paths = [ ] expect_dir = "../../tests/fpga-debugging/axi-lite-s1/expects" expect_name = "s1_buggy.monitor.expect" -cmd = "cd ../.. && target/debug/protocols-monitor --protocol tests/fpga-debugging/axi-lite-s1/s1_buggy.prot --wave tests/fpga-debugging/axi-lite-s1/s1_buggy_workload2.vcd --instances TOP.testbench.UUT:WriteSubordinate TOP.testbench.UUT:ReadSubordinate --sample-posedge TOP.testbench.UUT.S_AXI_ACLK --show-waveform-time --time-unit ns --include-idle 2>/dev/null" +cmd = "cd ../.. && target/debug/protocols-monitor --protocol tests/fpga-debugging/axi-lite-s1/s1_buggy.prot --wave tests/fpga-debugging/axi-lite-s1/s1_buggy_workload2.vcd --instances TOP.testbench.UUT:WriteSubordinate --sample-posedge TOP.testbench.UUT.S_AXI_ACLK --show-waveform-time --time-unit ns --include-idle 2>/dev/null" [[tests]] name = "monitor.tests_fpga_debugging_axi_lite_s1_s1_buggy_workload_1.s1_buggy_workload_1_monitor" @@ -1258,7 +1258,7 @@ paths = [ ] expect_dir = "../../tests/fpga-debugging/axi-lite-s1/expects" expect_name = "s1_fixed.monitor.expect" -cmd = "cd ../.. && target/debug/protocols-monitor --protocol tests/fpga-debugging/axi-lite-s1/s1_fixed.prot --wave tests/fpga-debugging/axi-lite-s1/s1_fixed_workload2.vcd --instances TOP.testbench.UUT:WriteSubordinate TOP.testbench.UUT:ReadSubordinate --sample-posedge TOP.testbench.UUT.S_AXI_ACLK --show-waveform-time --time-unit ns --include-idle 2>/dev/null" +cmd = "cd ../.. && target/debug/protocols-monitor --protocol tests/fpga-debugging/axi-lite-s1/s1_fixed.prot --wave tests/fpga-debugging/axi-lite-s1/s1_fixed_workload2.vcd --instances TOP.testbench.UUT:WriteSubordinate --sample-posedge TOP.testbench.UUT.S_AXI_ACLK --show-waveform-time --time-unit ns --include-idle 2>/dev/null" [[tests]] name = "monitor.tests_fpga_debugging_axi_lite_s1_s1_fixed_workload_1.s1_fixed_workload_1_monitor" diff --git a/scripts/test_catalog.py b/scripts/test_catalog.py index ff56b960..04d8af1e 100644 --- a/scripts/test_catalog.py +++ b/scripts/test_catalog.py @@ -349,6 +349,20 @@ "top": "fifo_wrapper", "expect": "pass", }, + "tests/fpga-debugging/axi-lite-s1/s1_buggy.tx": { + "protocol": "tests/fpga-debugging/axi-lite-s1/s1_buggy.prot", + "verilog": ("tests/fpga-debugging/axi-lite-s1/s1_buggy.v",), + "top": "xlnxdemo", + "max_steps": 300, + "expect": "assignment_conflict", + }, + "tests/fpga-debugging/axi-lite-s1/s1_fixed.tx": { + "protocol": "tests/fpga-debugging/axi-lite-s1/s1_fixed.prot", + "verilog": ("tests/fpga-debugging/axi-lite-s1/s1_fixed.v",), + "top": "xlnxdemo", + "max_steps": 300, + "expect": "pass", + }, "tests/identities/dual_identity_d0/dual_identity_d0_combdep.tx": { "protocol": "tests/identities/dual_identity_d0/dual_identity_d0.prot", "verilog": ("tests/identities/dual_identity_d0/dual_identity_d0.v",), @@ -660,10 +674,7 @@ "tests.fpga-debugging.axi-lite-s1.s1_buggy": { "protocol": "tests/fpga-debugging/axi-lite-s1/s1_buggy.prot", "wave": "tests/fpga-debugging/axi-lite-s1/s1_buggy_workload2.vcd", - "instances": ( - "TOP.testbench.UUT:WriteSubordinate", - "TOP.testbench.UUT:ReadSubordinate", - ), + "instances": ("TOP.testbench.UUT:WriteSubordinate",), "expect": None, "extra_args": ( "--sample-posedge", @@ -694,11 +705,11 @@ "tests.fpga-debugging.axi-lite-s1.s1_fixed": { "protocol": "tests/fpga-debugging/axi-lite-s1/s1_fixed.prot", "wave": "tests/fpga-debugging/axi-lite-s1/s1_fixed_workload2.vcd", - "instances": ( - "TOP.testbench.UUT:WriteSubordinate", - "TOP.testbench.UUT:ReadSubordinate", - ), - "expect": "pass", + "instances": ("TOP.testbench.UUT:WriteSubordinate",), + # The monitor doesn't work for this protocol due to a known bug + # (inability to handle multiple assignments to the same port within the same cycle). + # See https://github.com/cucapra/protocols/issues/214 + "expect": None, "extra_args": ( "--sample-posedge", "TOP.testbench.UUT.S_AXI_ACLK", diff --git a/tests/fpga-debugging/axi-lite-s1/expects/s1_buggy.interp.expect b/tests/fpga-debugging/axi-lite-s1/expects/s1_buggy.interp.expect new file mode 100644 index 00000000..484d6be2 --- /dev/null +++ b/tests/fpga-debugging/axi-lite-s1/expects/s1_buggy.interp.expect @@ -0,0 +1,15 @@ +error: Thread 1 (`write`) attempted conflicting assignment to 'S_AXI_BREADY': current=1, new=0 + ┌─ tests/fpga-debugging/axi-lite-s1/s1_buggy.prot:88:5 + │ +88 │ DUT.S_AXI_BREADY := 1'b0; + │ ^^^^^^^^^^^^^^^^^^^^^^^^^ Thread 1 (`write`) attempted conflicting assignment to 'S_AXI_BREADY': current=1, new=0 + +error: Thread 2 (`write`) attempted conflicting assignment to 'S_AXI_BREADY': current=0, new=1 + ┌─ tests/fpga-debugging/axi-lite-s1/s1_buggy.prot:100:5 + │ +100 │ DUT.S_AXI_BREADY := 1'b1; + │ ^^^^^^^^^^^^^^^^^^^^^^^^^ Thread 2 (`write`) attempted conflicting assignment to 'S_AXI_BREADY': current=0, new=1 + +Trace 0 execution failed. +---CODE--- +101 diff --git a/tests/fpga-debugging/axi-lite-s1/expects/s1_fixed.interp.expect b/tests/fpga-debugging/axi-lite-s1/expects/s1_fixed.interp.expect new file mode 100644 index 00000000..f5f6cb49 --- /dev/null +++ b/tests/fpga-debugging/axi-lite-s1/expects/s1_fixed.interp.expect @@ -0,0 +1 @@ +Trace 0 executed successfully! diff --git a/tests/fpga-debugging/axi-lite-s1/expects/s1_fixed.monitor.expect b/tests/fpga-debugging/axi-lite-s1/expects/s1_fixed.monitor.expect index aabbc981..6503598b 100644 --- a/tests/fpga-debugging/axi-lite-s1/expects/s1_fixed.monitor.expect +++ b/tests/fpga-debugging/axi-lite-s1/expects/s1_fixed.monitor.expect @@ -1,8 +1,2 @@ -// trace 0 -trace { - WriteSubordinate::idle(); // [time: 0ns -> 25ns] - ReadSubordinate::idle(); // [time: 0ns -> 25ns] - WriteSubordinate::write(64, 2147483648, 0, 0); // [time: 25ns -> 100ns] - ReadSubordinate::read_v2(68, 0, 1); // [time: 50ns -> 125ns] - ReadSubordinate::idle(); // [time: 125ns -> 150ns] -} +---CODE--- +1 diff --git a/tests/fpga-debugging/axi-lite-s1/s1_buggy.prot b/tests/fpga-debugging/axi-lite-s1/s1_buggy.prot index 75ce47f6..e10244d0 100644 --- a/tests/fpga-debugging/axi-lite-s1/s1_buggy.prot +++ b/tests/fpga-debugging/axi-lite-s1/s1_buggy.prot @@ -32,8 +32,9 @@ prot reset() { step(); } -// Write transaction where the manager waits `n` cycles before setting AWVALID = 1 -// and stalls the response channel for `n` cycles before setting BREADY = 1. +// Write transaction where the manager waits `n` cycles before setting AWVALID = 1. +// After the subordinate indicates `BVALID = 1`, the manager stalls the response channel +// for `n` cycles before setting BREADY = 1. // The `resp` argument is a 2-bit pattern containing the subordinate's response // to the write request (indicating whether the transaction succeeded). prot write(addr: u7, data: u32, resp: u2, n: uint) { From 9ce5b8572a682a873a6bafb9464e10b6fc894a74 Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Sun, 5 Jul 2026 15:18:09 -0400 Subject: [PATCH 07/13] Update Runt expect test output --- .../axi-lite-s1/expects/s1_buggy.interp.expect | 12 ++++++------ tests/fpga-debugging/axi-lite-s1/s1_fixed.prot | 5 +++-- 2 files changed, 9 insertions(+), 8 deletions(-) diff --git a/tests/fpga-debugging/axi-lite-s1/expects/s1_buggy.interp.expect b/tests/fpga-debugging/axi-lite-s1/expects/s1_buggy.interp.expect index 484d6be2..6bc54dd6 100644 --- a/tests/fpga-debugging/axi-lite-s1/expects/s1_buggy.interp.expect +++ b/tests/fpga-debugging/axi-lite-s1/expects/s1_buggy.interp.expect @@ -1,14 +1,14 @@ error: Thread 1 (`write`) attempted conflicting assignment to 'S_AXI_BREADY': current=1, new=0 - ┌─ tests/fpga-debugging/axi-lite-s1/s1_buggy.prot:88:5 + ┌─ tests/fpga-debugging/axi-lite-s1/s1_buggy.prot:83:5 │ -88 │ DUT.S_AXI_BREADY := 1'b0; +83 │ DUT.S_AXI_BREADY := 1'b0; │ ^^^^^^^^^^^^^^^^^^^^^^^^^ Thread 1 (`write`) attempted conflicting assignment to 'S_AXI_BREADY': current=1, new=0 error: Thread 2 (`write`) attempted conflicting assignment to 'S_AXI_BREADY': current=0, new=1 - ┌─ tests/fpga-debugging/axi-lite-s1/s1_buggy.prot:100:5 - │ -100 │ DUT.S_AXI_BREADY := 1'b1; - │ ^^^^^^^^^^^^^^^^^^^^^^^^^ Thread 2 (`write`) attempted conflicting assignment to 'S_AXI_BREADY': current=0, new=1 + ┌─ tests/fpga-debugging/axi-lite-s1/s1_buggy.prot:95:5 + │ +95 │ DUT.S_AXI_BREADY := 1'b1; + │ ^^^^^^^^^^^^^^^^^^^^^^^^^ Thread 2 (`write`) attempted conflicting assignment to 'S_AXI_BREADY': current=0, new=1 Trace 0 execution failed. ---CODE--- diff --git a/tests/fpga-debugging/axi-lite-s1/s1_fixed.prot b/tests/fpga-debugging/axi-lite-s1/s1_fixed.prot index 75ce47f6..e10244d0 100644 --- a/tests/fpga-debugging/axi-lite-s1/s1_fixed.prot +++ b/tests/fpga-debugging/axi-lite-s1/s1_fixed.prot @@ -32,8 +32,9 @@ prot reset() { step(); } -// Write transaction where the manager waits `n` cycles before setting AWVALID = 1 -// and stalls the response channel for `n` cycles before setting BREADY = 1. +// Write transaction where the manager waits `n` cycles before setting AWVALID = 1. +// After the subordinate indicates `BVALID = 1`, the manager stalls the response channel +// for `n` cycles before setting BREADY = 1. // The `resp` argument is a 2-bit pattern containing the subordinate's response // to the write request (indicating whether the transaction succeeded). prot write(addr: u7, data: u32, resp: u2, n: uint) { From bfe6f4e1f49b0078b2158a7caae1ced2fa9aa302 Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Sun, 5 Jul 2026 15:19:52 -0400 Subject: [PATCH 08/13] Run uv 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 04d8af1e..50676904 100644 --- a/scripts/test_catalog.py +++ b/scripts/test_catalog.py @@ -706,8 +706,8 @@ "protocol": "tests/fpga-debugging/axi-lite-s1/s1_fixed.prot", "wave": "tests/fpga-debugging/axi-lite-s1/s1_fixed_workload2.vcd", "instances": ("TOP.testbench.UUT:WriteSubordinate",), - # The monitor doesn't work for this protocol due to a known bug - # (inability to handle multiple assignments to the same port within the same cycle). + # The monitor doesn't work for this protocol due to a known bug + # (inability to handle multiple assignments to the same port within the same cycle). # See https://github.com/cucapra/protocols/issues/214 "expect": None, "extra_args": ( From 945ea523dc3df73800c0807404aa824e4f2c0f77 Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Sun, 5 Jul 2026 16:02:48 -0400 Subject: [PATCH 09/13] Add Runt test suite for bi --- runt/bi/runt.toml | 19 +++++++++++++++++ scripts/generate_runt_configs.py | 35 ++++++++++++++++++++++++++++++++ scripts/test_catalog.py | 23 ++++++++++++++++++++- 3 files changed, 76 insertions(+), 1 deletion(-) create mode 100644 runt/bi/runt.toml diff --git a/runt/bi/runt.toml b/runt/bi/runt.toml new file mode 100644 index 00000000..bfa4e6d3 --- /dev/null +++ b/runt/bi/runt.toml @@ -0,0 +1,19 @@ +ver = "0.4.1" + +[[tests]] +name = "bi.tests_fpga_debugging_axi_lite_s1_s1_buggy.s1_buggy_bi" +paths = [ + "../../tests/fpga-debugging/axi-lite-s1/s1_buggy.prot", +] +expect_dir = "../../tests/fpga-debugging/axi-lite-s1/expects" +expect_name = "s1_buggy.bi.expect" +cmd = "cd ../.. && target/debug/bi --protocol tests/fpga-debugging/axi-lite-s1/s1_buggy.prot --wave tests/fpga-debugging/axi-lite-s1/s1_buggy_interp.fst --instances dut:WriteSubordinate --show-steps --include-in-progress 2>/dev/null" + +[[tests]] +name = "bi.tests_fpga_debugging_axi_lite_s1_s1_fixed.s1_fixed_bi" +paths = [ + "../../tests/fpga-debugging/axi-lite-s1/s1_fixed.prot", +] +expect_dir = "../../tests/fpga-debugging/axi-lite-s1/expects" +expect_name = "s1_fixed.bi.expect" +cmd = "cd ../.. && target/debug/bi --protocol tests/fpga-debugging/axi-lite-s1/s1_fixed.prot --wave tests/fpga-debugging/axi-lite-s1/s1_fixed_interp.fst --instances dut:WriteSubordinate --show-steps 2>/dev/null" diff --git a/scripts/generate_runt_configs.py b/scripts/generate_runt_configs.py index 011e7293..d9695ea9 100644 --- a/scripts/generate_runt_configs.py +++ b/scripts/generate_runt_configs.py @@ -62,6 +62,25 @@ def load_monitor_cases() -> list[dict]: return out +def load_bi_cases() -> list[dict]: + """Same as load_monitor_cases but for the bi cases""" + out = [] + for case_id, c in test_catalog.BI_CASES.items(): + out.append( + { + "id": case_id, + "path": c["protocol"], + "wave": c.get("wave"), + "instances": c.get("instances", ()), + "max_steps": c.get("max_steps"), + "timeout_secs": c.get("timeout_secs"), + "extra_args": c.get("extra_args", ()), + "expected": c["expect"], + } + ) + return out + + # helper function to escape globs in places def runt_glob_literal(path: str) -> str: return path.replace("[", "[[]").replace("*", "[*]").replace("?", "[?]") @@ -195,6 +214,19 @@ def monitor_runt_command(case: dict) -> list[tuple[str, str]]: return [("", repo_root_command(cmd))] +# Same as `monitor_runt_command` above but for BI test cases +def bi_runt_command(case: dict) -> list[tuple[str, str]]: + cmd = [*binary_prefix("bi"), "--protocol", case["path"]] + if case["wave"]: + cmd += ["--wave", case["wave"]] + if case["instances"]: + cmd += ["--instances", *case["instances"]] + cmd += case["extra_args"] + if case["timeout_secs"] is not None: + cmd = timeout_cmd(case["timeout_secs"], cmd) + return [("", repo_root_command(cmd))] + + def waveform_runt_command(case: dict) -> list[tuple[str, str]]: ast_cmd = [ *binary_prefix("protocols-interp"), @@ -226,6 +258,7 @@ def waveform_runt_command(case: dict) -> list[tuple[str, str]]: "interp": interp_runt_command, "graph_interp": graph_interp_runt_command, "monitor": monitor_runt_command, + "bi": bi_runt_command, "waveform": waveform_runt_command, } @@ -330,11 +363,13 @@ def write_runt_toml(output_dir: Path, suites) -> None: def generate_runt_configs() -> None: tx = load_tx_cases() mon = load_monitor_cases() + bi = load_bi_cases() # Each suite maps a name to (runner, cases). interp + monitor + graph_interp # together cover every test. suite_specs = { "interp": ("interp", tx), "monitor": ("monitor", mon), + "bi": ("bi", bi), "graph_interp": ("graph_interp", graph_interp_cases(tx)), "waveform": ("waveform", waveform_cases(tx)), } diff --git a/scripts/test_catalog.py b/scripts/test_catalog.py index 50676904..ee069389 100644 --- a/scripts/test_catalog.py +++ b/scripts/test_catalog.py @@ -1,7 +1,7 @@ # Checked-in test catalog. Hand-maintained source of truth. # Consumed by scripts/generate_runt_configs.py and scripts/benchmark_monitor.py. # -# TX_CASES are keyed by their .tx path. MONITOR_CASES are keyed by a unique id +# TX_CASES are keyed by their .tx path. MONITOR_CASES & BI_CASES are both keyed by a unique id TX_CASES = { "examples/picorv32/unsigned_mul.tx": { @@ -1110,3 +1110,24 @@ def _antmicro_case(stem): for stem in ANTMICRO_TRACE_STEMS } ) + +# The filepath supplied to the `wave` field are .fst files produced by the interpreter. +BI_CASES = { + "tests.fpga-debugging.axi-lite-s1.s1_buggy.bi": { + "protocol": "tests/fpga-debugging/axi-lite-s1/s1_buggy.prot", + "wave": "tests/fpga-debugging/axi-lite-s1/s1_buggy_interp.fst", + "instances": ("dut:WriteSubordinate",), + # `--include-in-progress` makes `bi` report the two writes that + # started but whose responses never completed, surfacing the + # lost-write-response bug on the monitoring side. + "expect": None, + "extra_args": ("--show-steps", "--include-in-progress"), + }, + "tests.fpga-debugging.axi-lite-s1.s1_fixed.bi": { + "protocol": "tests/fpga-debugging/axi-lite-s1/s1_fixed.prot", + "wave": "tests/fpga-debugging/axi-lite-s1/s1_fixed_interp.fst", + "instances": ("dut:WriteSubordinate",), + "expect": None, + "extra_args": ("--show-steps",), + }, +} From 3a10f5317f6c6657aa84d91fb4518685dcfc601a Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Sun, 5 Jul 2026 16:03:06 -0400 Subject: [PATCH 10/13] Update Justfile to run Runt bi test suite --- justfile | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/justfile b/justfile index 264bdc23..ebc8eceb 100644 --- a/justfile +++ b/justfile @@ -1,8 +1,9 @@ # Runs the Runt snapshot suites that together cover every test runt: - cargo build --offline --package protocols-interp --package protocols-monitor --package graph-interp + cargo build --offline --package protocols-interp --package protocols-monitor --package graph-interp --package bi runt --max-futures 1 runt/interp runt --max-futures 1 runt/monitor + runt --max-futures 1 runt/bi runt --max-futures 1 runt/graph_interp runt --max-futures 1 runt/waveform From 36ed000c29d2d7c09e4a72a12646dbd8b9d52030 Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Sun, 5 Jul 2026 16:03:14 -0400 Subject: [PATCH 11/13] update CI --- .github/workflows/test.yml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index de6ab4ea..8a1d3111 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -36,6 +36,8 @@ jobs: run: runt runt/graph_interp - name: Run Runt tests for monitor run: runt runt/monitor + - name: Run Runt tests for bi + run: runt runt/bi test-freshness: name: Check Generated Runt Configs are Fresh From 459df74d90ff42986ed42ed409e9929d15a644d8 Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Sun, 5 Jul 2026 16:03:35 -0400 Subject: [PATCH 12/13] Add expected test output for bi --- .../axi-lite-s1/expects/s1_buggy.bi.expect | 13 ++++++ .../axi-lite-s1/expects/s1_fixed.bi.expect | 43 +++++++++++++++++++ 2 files changed, 56 insertions(+) create mode 100644 tests/fpga-debugging/axi-lite-s1/expects/s1_buggy.bi.expect create mode 100644 tests/fpga-debugging/axi-lite-s1/expects/s1_fixed.bi.expect diff --git a/tests/fpga-debugging/axi-lite-s1/expects/s1_buggy.bi.expect b/tests/fpga-debugging/axi-lite-s1/expects/s1_buggy.bi.expect new file mode 100644 index 00000000..2e3bfd1b --- /dev/null +++ b/tests/fpga-debugging/axi-lite-s1/expects/s1_buggy.bi.expect @@ -0,0 +1,13 @@ +// trace 0 +trace { + reset(); [0] + write(8, 7, X, 0); [7 .. ] + write(4, 42, X, 4); [1 .. ] +} + +// trace 1 +trace { + reset(); [0] + write(8, 7, X, 0); [7 .. ] + write(4, 42, X, 3); [2 .. ] +} diff --git a/tests/fpga-debugging/axi-lite-s1/expects/s1_fixed.bi.expect b/tests/fpga-debugging/axi-lite-s1/expects/s1_fixed.bi.expect new file mode 100644 index 00000000..d2661524 --- /dev/null +++ b/tests/fpga-debugging/axi-lite-s1/expects/s1_fixed.bi.expect @@ -0,0 +1,43 @@ +// trace 0 +trace { + reset(); [0] + write(4, 42, 0, 4); [1 .. 12] + write(8, 7, 0, 0); [7 .. 14] +} + +// trace 1 +trace { + reset(); [0] + write(4, 42, 0, 4); [1 .. 12] + write(8, 7, 0, 0); [7 .. 14] +} + +// trace 2 +trace { + reset(); [0] + write(4, 42, 0, 4); [1 .. 12] + write(8, 7, 0, 0); [7 .. 14] +} + +// trace 3 +trace { + reset(); [0] + write(4, 42, 0, 4); [1 .. 12] + write(8, 7, 0, 0); [7 .. 14] +} + +// trace 4 +trace { + reset(); [0] + write(4, 42, 0, 4); [1 .. 12] + write(8, 7, 0, 0); [7 .. 14] +} + +// trace 5 +trace { + reset(); [0] + write(4, 42, 0, 4); [1 .. 12] + write(8, 7, 0, 0); [7 .. 14] +} +---CODE--- +1 From 79820a6494938920324bc79cb9f55b58498bac7f Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Sun, 5 Jul 2026 16:03:44 -0400 Subject: [PATCH 13/13] Add waveforms produced by interpreter --- .../axi-lite-s1/s1_buggy_interp.fst | Bin 0 -> 2289 bytes .../axi-lite-s1/s1_fixed_interp.fst | Bin 0 -> 2318 bytes 2 files changed, 0 insertions(+), 0 deletions(-) create mode 100644 tests/fpga-debugging/axi-lite-s1/s1_buggy_interp.fst create mode 100644 tests/fpga-debugging/axi-lite-s1/s1_fixed_interp.fst diff --git a/tests/fpga-debugging/axi-lite-s1/s1_buggy_interp.fst b/tests/fpga-debugging/axi-lite-s1/s1_buggy_interp.fst new file mode 100644 index 0000000000000000000000000000000000000000..c46cd3afa7f369f132e005836f6e0e036943b55f GIT binary patch literal 2289 zcmeHHOK%cU6#njIV7MdDmzwf0!LTZcNul`Yg4jVYAvP8V6o`uvWkN7Yn_*}{-E>`D zs4JIUxp3t|HYWOK)UEml)H4r=c45+;F`VQ(-#yX^=nCVyDbhX2W9;kQ-p;_%SNGuy zV>v^}64t_4$i2g1YuMFWW~<#cUotx6sl7QI-W^#6Rke-bIhg$iySiy~dUiGMK?*~O zLrK^Nk<#E#Aw|HS*?#$a4=b4q5kxN%E|IVvf!Ibg`^rHqn}%?g6X|yrEkxI7n;@P* zJcf7#F+y;NJDqhT@zdwMpqm~~A0v~Qk1?6RI7>Q^Skg9GcIa;|=yvme_PS0;cnfu` zjFtTAAC{pgld=7=j0z?-R7?##!KTT^u^P^jXA_uBU^an&bprVuIFREp{)s1eP@2bS zDS$;NA;d_3zx0joe%*S@S8iAP{LS|d&nX*eiJa_Y27&=7c3FrdN%95!JTClP4*D;1 W5fUdhNVaW>ety^77?aO?%D({T8fbq2 literal 0 HcmV?d00001 diff --git a/tests/fpga-debugging/axi-lite-s1/s1_fixed_interp.fst b/tests/fpga-debugging/axi-lite-s1/s1_fixed_interp.fst new file mode 100644 index 0000000000000000000000000000000000000000..2f07ed9548dbc164570aaf02307c2ddaca170cc8 GIT binary patch literal 2318 zcmeHJO=}ZT6g}_dbtW^DkG9s(rV&Q6YCvex_|Zk76B8j=Y@9^XP%y@32oX)oBxzIa zrYjfKg^CMzcICpA3$qdQN9a!w!Ik<4)H|6ZXct0vBDrwxdH3A8mp7Nk;{iQmS(k@C zST9Z;sPD&?hl;yk{dnmJGvq2Qd$ZAQ>doC|%et%A8!gM;vMusQdiy52;t31CCj~~-GvEEg?>eBol7N;m4cl@!83I;V)Obz;iLxaSz8je05O<**E(FFe02`nW+ z*J_f7`6nLXUNP?b$fpq!A%RI0a3 K7~JgIApQj*CvT_# literal 0 HcmV?d00001