From 220e66614faf861436255822f9ef00ceb0c128dc Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Wed, 18 Feb 2026 10:39:39 -0500 Subject: [PATCH 01/11] Add axi-stream-s2 files for interpreter --- .../fpga-debugging/axi-stream-s2/s2_buggy.out | 0 .../axi-stream-s2/s2_buggy.prot | 111 +++++++++ .../fpga-debugging/axi-stream-s2/s2_buggy.v | 231 +++++++++++++++++ .../fpga-debugging/axi-stream-s2/s2_fixed.out | 0 .../axi-stream-s2/s2_fixed.prot | 113 +++++++++ .../fpga-debugging/axi-stream-s2/s2_fixed.v | 232 ++++++++++++++++++ 6 files changed, 687 insertions(+) create mode 100644 protocols/tests/fpga-debugging/axi-stream-s2/s2_buggy.out create mode 100644 protocols/tests/fpga-debugging/axi-stream-s2/s2_buggy.prot create mode 100644 protocols/tests/fpga-debugging/axi-stream-s2/s2_buggy.v create mode 100644 protocols/tests/fpga-debugging/axi-stream-s2/s2_fixed.out create mode 100644 protocols/tests/fpga-debugging/axi-stream-s2/s2_fixed.prot create mode 100644 protocols/tests/fpga-debugging/axi-stream-s2/s2_fixed.v diff --git a/protocols/tests/fpga-debugging/axi-stream-s2/s2_buggy.out b/protocols/tests/fpga-debugging/axi-stream-s2/s2_buggy.out new file mode 100644 index 00000000..e69de29b diff --git a/protocols/tests/fpga-debugging/axi-stream-s2/s2_buggy.prot b/protocols/tests/fpga-debugging/axi-stream-s2/s2_buggy.prot new file mode 100644 index 00000000..a1648cf1 --- /dev/null +++ b/protocols/tests/fpga-debugging/axi-stream-s2/s2_buggy.prot @@ -0,0 +1,111 @@ +// ARGS: --wave fpga-debugging/axi-stream-s2/s2_buggy.fst --instances TOP.testbench.UUT.axi_stream_check:AXISManager --sample-posedge TOP.testbench.UUT.axi_stream_check.i_aclk --show-waveform-time --time-unit ns + +// Source (manager) that outputs a sequence of 8 words +struct AXISManager { + // Control signals + in i_aresetn: u1, // Active-low reset + + // AXI-Stream manager outputs (from DUT perspective) + out i_tvalid: u1, // manager has valid data + out i_tdata: u32, // Data payload + out i_tstrb: u4, // Byte strobe (always 0xF) + out i_tlast: u1, // Last word in packet + + // AXI-Stream sub-ordinate input + in i_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.i_aresetn := 1'b0; // Assert reset (active-low) + DUT.i_tready := 1'b0; + step(); +} + +// RECV: Receive one data word from the AXI-Stream manager +// Data transfer occurs when i_tvalid and i_tready are both 1 +// Only matches when data is immediately available (i_tvalid = 1) +// +// Output Arguments: +// data - Expected payload from manager +prot recv( + out data: u32, +) { + DUT.i_aresetn := 1'b1; // Keep out of reset + DUT.i_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.i_tvalid, 1'b1); + + // Verify output data + assert_eq(DUT.i_tdata, data); + + // One cycle for the transfer to complete + step(); +} + +// RECV_LAST: Receive the last data word (with i_tlast asserted) +// This verifies both the data and that i_tlast is properly set +// Only matches when data is immediately available (i_tvalid = 1) +// +// Output Arguments: +// data - Expected payload from manager (should be the last word) +prot recv_last( + out data: u32, +) { + DUT.i_aresetn := 1'b1; // Keep out of reset + DUT.i_tready := 1'b1; // Signal ready to receive + + // Only matches when data is available + assert_eq(DUT.i_tvalid, 1'b1); + + // Verify output data and i_tlast + assert_eq(DUT.i_tdata, data); + assert_eq(DUT.i_tlast, 1'b1); + + // One cycle for the transfer to complete + step(); +} + +// STALL: Assert backpressure (i_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 i_tvalid=1 (i.e. there is some valid data and it's available to stall) +prot stall(out data: u32, out last: u1) { + DUT.i_aresetn := 1'b1; // Keep out of reset + DUT.i_tready := 1'b0; // Apply backpressure + + // Stall only applies when manager has valid data + // If i_tvalid=0, this fails and we instead have an `idle` transaction + assert_eq(DUT.i_tvalid, 1'b1); + + // Capture output values before the stall cycle + assert_eq(DUT.i_tdata, data); + assert_eq(DUT.i_tlast, last); + + step(); + + // Verify outputs remained stable during the stall + assert_eq(DUT.i_tdata, data); + assert_eq(DUT.i_tlast, last); +} + +// 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.i_aresetn := 1'b1; // Keep out of reset + DUT.i_tready := 1'b1; + + // Only matches when no data is available + assert_eq(DUT.i_tvalid, 1'b0); + step(); +} + +// IDLE: No transaction - i_tready is deasserted +#[idle] +prot idle() { + DUT.i_aresetn := 1'b1; // Keep out of reset + DUT.i_tready := 1'b0; + step(); +} diff --git a/protocols/tests/fpga-debugging/axi-stream-s2/s2_buggy.v b/protocols/tests/fpga-debugging/axi-stream-s2/s2_buggy.v new file mode 100644 index 00000000..b95a2254 --- /dev/null +++ b/protocols/tests/fpga-debugging/axi-stream-s2/s2_buggy.v @@ -0,0 +1,231 @@ +//////////////////////////////////////////////////////////////////////////////// +// +// Filename: xlnxstream_2018_3 +// +// Project: WB2AXIPSP: bus bridges and other odds and ends +// +// Purpose: To test the formal tools on an AXI stream master core that is +// "known" to work. This core was generated via the IP packager +// in Vivado 2018.3. Sadly, it's broken in a couple of ways, one which +// is prominently the TLAST signal which may be set even through the +// channel is stalled. Feel free to try it out. +// +// This core will fail a verification check. +// +// Creator: Vivado, 2018.3 +// +//////////////////////////////////////////////////////////////////////////////// +// +// +`default_nettype none +// +`timescale 1 ns / 1 ps + +module xlnxstream_2018_3 # + ( + // Users to add parameters here + + // User parameters ends + // Do not modify the parameters beyond this line + + // Width of S_AXIS address bus. The slave accepts the read and write addresses of width C_M_AXIS_TDATA_WIDTH. + parameter integer C_M_AXIS_TDATA_WIDTH = 32, + // Start count is the number of clock cycles the master will wait before initiating/issuing any transaction. + parameter integer C_M_START_COUNT = 32 + ) + ( + // Users to add ports here + + // User ports ends + // Do not modify the ports beyond this line + + // Global ports + input wire M_AXIS_ACLK, + // + input wire M_AXIS_ARESETN, + // Master Stream Ports. TVALID indicates that the master + // is driving a valid transfer, A transfer takes place + // when both TVALID and TREADY are asserted. + output wire M_AXIS_TVALID, + // TDATA is the primary payload that is used to provide the + // data that is passing across the interface from the master. + output wire [C_M_AXIS_TDATA_WIDTH-1 : 0] M_AXIS_TDATA, + // TSTRB is the byte qualifier that indicates whether the + // content of the associated byte of TDATA is processed as a + // data byte or a position byte. + output wire [(C_M_AXIS_TDATA_WIDTH/8)-1 : 0] M_AXIS_TSTRB, + // TLAST indicates the boundary of a packet. + output wire M_AXIS_TLAST, + // TREADY indicates that the slave can accept a transfer in + // the current cycle. + input wire M_AXIS_TREADY + ); + // Total number of output data + localparam NUMBER_OF_OUTPUT_WORDS = 8; + + // WAIT_COUNT_BITS is the width of the wait counter. + localparam integer WAIT_COUNT_BITS = $clog2(C_M_START_COUNT); + + // bit_num gives the minimum number of bits needed to address 'depth' + // size of FIFO. + localparam bit_num = $clog2(NUMBER_OF_OUTPUT_WORDS + 1); + + // Define the states of state machine + // The control state machine oversees the writing of input streaming + // data to the FIFO, and outputs the streaming data from the FIFO + parameter [1:0] IDLE = 2'b00, // This is the initial/idle state + + INIT_COUNTER = 2'b01, // This state initializes the counter, + // once the counter reaches + // C_M_START_COUNT count, the state + // machine changes state to SEND_STREAM + SEND_STREAM = 2'b10; // In this state the + // stream data is output through M_AXIS_TDATA + // State variable + reg [1:0] mst_exec_state; + // Example design FIFO read pointer + reg [bit_num-1:0] read_pointer; + + // AXI Stream internal signals + // wait counter. The master waits for the user defined number of + // clock cycles before initiating a transfer. + reg [WAIT_COUNT_BITS-1 : 0] count; + //streaming data valid + wire axis_tvalid; + //streaming data valid delayed by one clock cycle + reg axis_tvalid_delay; + //Last of the streaming data + wire axis_tlast; + //Last of the streaming data delayed by one clock cycle + reg axis_tlast_delay; + //FIFO implementation signals + reg [C_M_AXIS_TDATA_WIDTH-1 : 0] stream_data_out; + wire tx_en; + //The master has issued all the streaming data stored in FIFO + reg tx_done; + + + // I/O Connections assignments + + assign M_AXIS_TVALID = axis_tvalid_delay; + assign M_AXIS_TDATA = stream_data_out; + assign M_AXIS_TLAST = axis_tlast_delay; + assign M_AXIS_TSTRB = {(C_M_AXIS_TDATA_WIDTH/8){1'b1}}; + + + // Control state machine implementation + always @(posedge M_AXIS_ACLK) + if (!M_AXIS_ARESETN) + // Synchronous reset (active low) + begin + mst_exec_state <= IDLE; + count <= 0; + end else case (mst_exec_state) + IDLE: + // The slave starts accepting tdata when + // there tvalid is asserted to mark the + // presence of valid streaming data + //if ( count == 0 ) + // begin + mst_exec_state <= INIT_COUNTER; + // end + //else + // begin + // mst_exec_state <= IDLE; + // end + + INIT_COUNTER: + // The slave starts accepting tdata when + // there tvalid is asserted to mark the + // presence of valid streaming data + if ( count == C_M_START_COUNT - 1 ) + mst_exec_state <= SEND_STREAM; + else begin + count <= count + 1; + mst_exec_state <= INIT_COUNTER; + end + + SEND_STREAM: + // The example design streaming master functionality starts when + // the master drives output tdata from the FIFO and the slave + // has finished storing the S_AXIS_TDATA + if (tx_done) + mst_exec_state <= IDLE; + else + mst_exec_state <= SEND_STREAM; + endcase + + + //tvalid generation + //axis_tvalid is asserted when the control state machine's state + // is SEND_STREAM and number of output streaming data is less than + // the NUMBER_OF_OUTPUT_WORDS. + assign axis_tvalid = ((mst_exec_state == SEND_STREAM) && (read_pointer < NUMBER_OF_OUTPUT_WORDS)); + + // AXI tlast generation + // axis_tlast is asserted number of output streaming data + // is NUMBER_OF_OUTPUT_WORDS-1 (0 to NUMBER_OF_OUTPUT_WORDS-1) + assign axis_tlast = (read_pointer == NUMBER_OF_OUTPUT_WORDS-1); + + + // Delay the axis_tvalid and axis_tlast signal by one clock cycle + // to match the latency of M_AXIS_TDATA + always @(posedge M_AXIS_ACLK) + if (!M_AXIS_ARESETN) + begin + axis_tvalid_delay <= 1'b0; + axis_tlast_delay <= 1'b0; + end else begin + axis_tvalid_delay <= axis_tvalid; + axis_tlast_delay <= axis_tlast; + end + + + //read_pointer pointer + always@(posedge M_AXIS_ACLK) + if(!M_AXIS_ARESETN) + begin + read_pointer <= 0; + tx_done <= 1'b0; + end else if (read_pointer <= NUMBER_OF_OUTPUT_WORDS-1) + begin + if (tx_en) + // read pointer is incremented after every read from the FIFO + // when FIFO read signal is enabled. + begin + read_pointer <= read_pointer + 1; + tx_done <= 1'b0; + end + end else if (read_pointer == NUMBER_OF_OUTPUT_WORDS) + begin + // tx_done is asserted when NUMBER_OF_OUTPUT_WORDS numbers + // of streaming data has been out. + tx_done <= 1'b1; + end + + + //FIFO read enable generation + assign tx_en = M_AXIS_TREADY && axis_tvalid; + + // Streaming output data is read from FIFO + always @( posedge M_AXIS_ACLK ) + if(!M_AXIS_ARESETN) + stream_data_out <= 1; + else if (tx_en)// && M_AXIS_TSTRB[byte_index] + stream_data_out <= read_pointer + 32'b1; + + //////////////////////////////////////////////////////////////////////// + // + // Add user logic here + // + // The below initial lines, and FORMAL section following, were not in + // Xilinx's original demo example. + // + // This initial logic is used to keep the formal proof consistent + // below. It's not strictly needed, neither was it part of Xilinx's + // original example demo. + initial count = 0; + initial mst_exec_state = IDLE; + initial read_pointer = 0; + initial tx_done = 0; +endmodule diff --git a/protocols/tests/fpga-debugging/axi-stream-s2/s2_fixed.out b/protocols/tests/fpga-debugging/axi-stream-s2/s2_fixed.out new file mode 100644 index 00000000..e69de29b diff --git a/protocols/tests/fpga-debugging/axi-stream-s2/s2_fixed.prot b/protocols/tests/fpga-debugging/axi-stream-s2/s2_fixed.prot new file mode 100644 index 00000000..afb0eccc --- /dev/null +++ b/protocols/tests/fpga-debugging/axi-stream-s2/s2_fixed.prot @@ -0,0 +1,113 @@ +// ARGS: --wave fpga-debugging/axi-stream-s2/s2_fixed.fst --instances TOP.testbench.UUT.axi_stream_check:AXISManager --sample-posedge TOP.testbench.UUT.axi_stream_check.i_aclk --show-waveform-time --time-unit ns + + +// Source (manager) that outputs a sequence of 8 words +struct AXISManager { + // Control signals + in i_aresetn: u1, // Active-low reset + + // AXI-Stream manager outputs (from DUT perspective) + out i_tvalid: u1, // manager has valid data + out i_tdata: u32, // Data payload + out i_tstrb: u4, // Byte strobe (always 0xF) + out i_tlast: u1, // Last word in packet + + // AXI-Stream sub-ordinate input + in i_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.i_aresetn := 1'b0; // Assert reset (active-low) + DUT.i_tready := 1'b0; + step(); +} + +// RECV: Receive one data word from the AXI-Stream manager +// Data transfer occurs when i_tvalid and i_tready are both 1 +// Only matches when data is immediately available (i_tvalid = 1) +// +// Output Arguments: +// data - Expected payload from manager +prot recv( + out data: u32, +) { + DUT.i_aresetn := 1'b1; // Keep out of reset + DUT.i_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.i_tvalid, 1'b1); + + // Verify output data + assert_eq(DUT.i_tdata, data); + + // One cycle for the transfer to complete + step(); +} + +// RECV_LAST: Receive the last data word (with i_tlast asserted) +// This verifies both the data and that i_tlast is properly set +// Only matches when data is immediately available (i_tvalid = 1) +// +// Output Arguments: +// data - Expected payload from manager (should be the last word) +prot recv_last( + out data: u32, +) { + DUT.i_aresetn := 1'b1; // Keep out of reset + DUT.i_tready := 1'b1; // Signal ready to receive + + // Only matches when data is available + assert_eq(DUT.i_tvalid, 1'b1); + + // Verify output data and i_tlast + assert_eq(DUT.i_tdata, data); + assert_eq(DUT.i_tlast, 1'b1); + + // One cycle for the transfer to complete + step(); +} + +// STALL: Assert backpressure (i_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 i_tvalid=1 (i.e. there is some valid data and it's available to stall) +prot stall(out data: u32, out last: u1) { + DUT.i_aresetn := 1'b1; // Keep out of reset + DUT.i_tready := 1'b0; // Apply backpressure + + // Stall only applies when manager has valid data + // If i_tvalid=0, this fails and we instead have an `idle` transaction + assert_eq(DUT.i_tvalid, 1'b1); + + // Capture output values before the stall cycle + assert_eq(DUT.i_tdata, data); + assert_eq(DUT.i_tlast, last); + + step(); + + // Verify outputs remained stable during the stall + assert_eq(DUT.i_tdata, data); + assert_eq(DUT.i_tlast, last); +} + +// 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.i_aresetn := 1'b1; // Keep out of reset + DUT.i_tready := 1'b1; + + // Only matches when no data is available + assert_eq(DUT.i_tvalid, 1'b0); + + step(); +} + +// IDLE: No transaction - i_tready is deasserted +#[idle] +prot idle() { + DUT.i_aresetn := 1'b1; // Keep out of reset + DUT.i_tready := 1'b0; + step(); +} diff --git a/protocols/tests/fpga-debugging/axi-stream-s2/s2_fixed.v b/protocols/tests/fpga-debugging/axi-stream-s2/s2_fixed.v new file mode 100644 index 00000000..51f02441 --- /dev/null +++ b/protocols/tests/fpga-debugging/axi-stream-s2/s2_fixed.v @@ -0,0 +1,232 @@ +//////////////////////////////////////////////////////////////////////////////// +// +// Filename: xlnxstream_2018_3 +// +// Project: WB2AXIPSP: bus bridges and other odds and ends +// +// Purpose: To test the formal tools on an AXI stream master core that is +// "known" to work. This core was generated via the IP packager +// in Vivado 2018.3. Sadly, it's broken in a couple of ways, one which +// is prominently the TLAST signal which may be set even through the +// channel is stalled. Feel free to try it out. +// +// This core will fail a verification check. +// +// Creator: Vivado, 2018.3 +// +//////////////////////////////////////////////////////////////////////////////// +// +// +`default_nettype none +// +`timescale 1 ns / 1 ps + +module xlnxstream_2018_3 # + ( + // Users to add parameters here + + // User parameters ends + // Do not modify the parameters beyond this line + + // Width of S_AXIS address bus. The slave accepts the read and write addresses of width C_M_AXIS_TDATA_WIDTH. + parameter integer C_M_AXIS_TDATA_WIDTH = 32, + // Start count is the number of clock cycles the master will wait before initiating/issuing any transaction. + parameter integer C_M_START_COUNT = 32 + ) + ( + // Users to add ports here + + // User ports ends + // Do not modify the ports beyond this line + + // Global ports + input wire M_AXIS_ACLK, + // + input wire M_AXIS_ARESETN, + // Master Stream Ports. TVALID indicates that the master + // is driving a valid transfer, A transfer takes place + // when both TVALID and TREADY are asserted. + output wire M_AXIS_TVALID, + // TDATA is the primary payload that is used to provide the + // data that is passing across the interface from the master. + output wire [C_M_AXIS_TDATA_WIDTH-1 : 0] M_AXIS_TDATA, + // TSTRB is the byte qualifier that indicates whether the + // content of the associated byte of TDATA is processed as a + // data byte or a position byte. + output wire [(C_M_AXIS_TDATA_WIDTH/8)-1 : 0] M_AXIS_TSTRB, + // TLAST indicates the boundary of a packet. + output wire M_AXIS_TLAST, + // TREADY indicates that the slave can accept a transfer in + // the current cycle. + input wire M_AXIS_TREADY + ); + // Total number of output data + localparam NUMBER_OF_OUTPUT_WORDS = 8; + + // WAIT_COUNT_BITS is the width of the wait counter. + localparam integer WAIT_COUNT_BITS = $clog2(C_M_START_COUNT); + + // bit_num gives the minimum number of bits needed to address 'depth' + // size of FIFO. + localparam bit_num = $clog2(NUMBER_OF_OUTPUT_WORDS + 1); + + // Define the states of state machine + // The control state machine oversees the writing of input streaming + // data to the FIFO, and outputs the streaming data from the FIFO + parameter [1:0] IDLE = 2'b00, // This is the initial/idle state + + INIT_COUNTER = 2'b01, // This state initializes the counter, + // once the counter reaches + // C_M_START_COUNT count, the state + // machine changes state to SEND_STREAM + SEND_STREAM = 2'b10; // In this state the + // stream data is output through M_AXIS_TDATA + // State variable + reg [1:0] mst_exec_state; + // Example design FIFO read pointer + reg [bit_num-1:0] read_pointer; + + // AXI Stream internal signals + // wait counter. The master waits for the user defined number of + // clock cycles before initiating a transfer. + reg [WAIT_COUNT_BITS-1 : 0] count; + //streaming data valid + wire axis_tvalid; + //streaming data valid delayed by one clock cycle + reg axis_tvalid_delay; + //Last of the streaming data + wire axis_tlast; + //Last of the streaming data delayed by one clock cycle + reg axis_tlast_delay; + //FIFO implementation signals + reg [C_M_AXIS_TDATA_WIDTH-1 : 0] stream_data_out; + wire tx_en; + //The master has issued all the streaming data stored in FIFO + reg tx_done; + + + // I/O Connections assignments + + assign M_AXIS_TVALID = axis_tvalid_delay; + assign M_AXIS_TDATA = stream_data_out; + assign M_AXIS_TLAST = axis_tlast_delay; + assign M_AXIS_TSTRB = {(C_M_AXIS_TDATA_WIDTH/8){1'b1}}; + + + // Control state machine implementation + always @(posedge M_AXIS_ACLK) + if (!M_AXIS_ARESETN) + // Synchronous reset (active low) + begin + mst_exec_state <= IDLE; + count <= 0; + end else case (mst_exec_state) + IDLE: + // The slave starts accepting tdata when + // there tvalid is asserted to mark the + // presence of valid streaming data + //if ( count == 0 ) + // begin + mst_exec_state <= INIT_COUNTER; + // end + //else + // begin + // mst_exec_state <= IDLE; + // end + + INIT_COUNTER: + // The slave starts accepting tdata when + // there tvalid is asserted to mark the + // presence of valid streaming data + if ( count == C_M_START_COUNT - 1 ) + mst_exec_state <= SEND_STREAM; + else begin + count <= count + 1; + mst_exec_state <= INIT_COUNTER; + end + + SEND_STREAM: + // The example design streaming master functionality starts when + // the master drives output tdata from the FIFO and the slave + // has finished storing the S_AXIS_TDATA + if (tx_done) + mst_exec_state <= IDLE; + else + mst_exec_state <= SEND_STREAM; + endcase + + + //tvalid generation + //axis_tvalid is asserted when the control state machine's state + // is SEND_STREAM and number of output streaming data is less than + // the NUMBER_OF_OUTPUT_WORDS. + assign axis_tvalid = ((mst_exec_state == SEND_STREAM) && (read_pointer < NUMBER_OF_OUTPUT_WORDS)); + + // AXI tlast generation + // axis_tlast is asserted number of output streaming data + // is NUMBER_OF_OUTPUT_WORDS-1 (0 to NUMBER_OF_OUTPUT_WORDS-1) + assign axis_tlast = (read_pointer == NUMBER_OF_OUTPUT_WORDS-1); + + + // Delay the axis_tvalid and axis_tlast signal by one clock cycle + // to match the latency of M_AXIS_TDATA + always @(posedge M_AXIS_ACLK) + if (!M_AXIS_ARESETN) + begin + axis_tvalid_delay <= 1'b0; + axis_tlast_delay <= 1'b0; + end else begin + axis_tvalid_delay <= axis_tvalid; + if (!axis_tvalid_delay || M_AXIS_TREADY) + axis_tlast_delay <= axis_tlast; + end + + + //read_pointer pointer + always@(posedge M_AXIS_ACLK) + if(!M_AXIS_ARESETN) + begin + read_pointer <= 0; + tx_done <= 1'b0; + end else if (read_pointer <= NUMBER_OF_OUTPUT_WORDS-1) + begin + if (tx_en) + // read pointer is incremented after every read from the FIFO + // when FIFO read signal is enabled. + begin + read_pointer <= read_pointer + 1; + tx_done <= 1'b0; + end + end else if (read_pointer == NUMBER_OF_OUTPUT_WORDS) + begin + // tx_done is asserted when NUMBER_OF_OUTPUT_WORDS numbers + // of streaming data has been out. + tx_done <= 1'b1; + end + + + //FIFO read enable generation + assign tx_en = M_AXIS_TREADY && axis_tvalid; + + // Streaming output data is read from FIFO + always @( posedge M_AXIS_ACLK ) + if(!M_AXIS_ARESETN) + stream_data_out <= 1; + else if (tx_en)// && M_AXIS_TSTRB[byte_index] + stream_data_out <= read_pointer + 32'b1; + + //////////////////////////////////////////////////////////////////////// + // + // Add user logic here + // + // The below initial lines, and FORMAL section following, were not in + // Xilinx's original demo example. + // + // This initial logic is used to keep the formal proof consistent + // below. It's not strictly needed, neither was it part of Xilinx's + // original example demo. + initial count = 0; + initial mst_exec_state = IDLE; + initial read_pointer = 0; + initial tx_done = 0; +endmodule From 6b156adab1ee62c5dc2de1444fe1eb7f120faf7c Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Wed, 18 Feb 2026 10:48:57 -0500 Subject: [PATCH 02/11] Add .tx files --- protocols/s2_buggy.tx | 38 ++++++++++++++++++++++++++++++++++++++ protocols/s2_fixed.tx | 39 +++++++++++++++++++++++++++++++++++++++ 2 files changed, 77 insertions(+) create mode 100644 protocols/s2_buggy.tx create mode 100644 protocols/s2_fixed.tx diff --git a/protocols/s2_buggy.tx b/protocols/s2_buggy.tx new file mode 100644 index 00000000..40a7ea8e --- /dev/null +++ b/protocols/s2_buggy.tx @@ -0,0 +1,38 @@ +// trace 0 +trace { + reset(); // [time: 0ns -> 12.5ns] + wait_for_data(); // [time: 337.5ns -> 362.5ns] + wait_for_data(); // [time: 387.5ns -> 412.5ns] + wait_for_data(); // [time: 512.5ns -> 537.5ns] + wait_for_data(); // [time: 537.5ns -> 562.5ns] + wait_for_data(); // [time: 612.5ns -> 637.5ns] + wait_for_data(); // [time: 787.5ns -> 812.5ns] + wait_for_data(); // [time: 837.5ns -> 862.5ns] + recv(1); // [time: 862.5ns -> 887.5ns] + recv(2); // [time: 887.5ns -> 912.5ns] + recv(3); // [time: 912.5ns -> 937.5ns] + recv(4); // [time: 937.5ns -> 962.5ns] + recv(5); // [time: 962.5ns -> 987.5ns] + recv(6); // [time: 987.5ns -> 1012.5ns] + stall(7, 0); // [time: 1012.5ns -> 1037.5ns] + stall(7, 1); // [time: 1037.5ns -> 1050ns] +} + +// trace 1 +trace { + reset(); // [time: 0ns -> 12.5ns] + wait_for_data(); // [time: 337.5ns -> 362.5ns] + wait_for_data(); // [time: 387.5ns -> 412.5ns] + wait_for_data(); // [time: 512.5ns -> 537.5ns] + wait_for_data(); // [time: 537.5ns -> 562.5ns] + wait_for_data(); // [time: 612.5ns -> 637.5ns] + wait_for_data(); // [time: 787.5ns -> 812.5ns] + wait_for_data(); // [time: 837.5ns -> 862.5ns] + recv(1); // [time: 862.5ns -> 887.5ns] + recv(2); // [time: 887.5ns -> 912.5ns] + recv(3); // [time: 912.5ns -> 937.5ns] + recv(4); // [time: 937.5ns -> 962.5ns] + recv(5); // [time: 962.5ns -> 987.5ns] + recv(6); // [time: 987.5ns -> 1012.5ns] + stall(7, 1); // [time: 1037.5ns -> 1050ns] +} diff --git a/protocols/s2_fixed.tx b/protocols/s2_fixed.tx new file mode 100644 index 00000000..ecb7f33b --- /dev/null +++ b/protocols/s2_fixed.tx @@ -0,0 +1,39 @@ +// Same as s2_buggy.tx for now +// trace 0 +trace { + reset(); // [time: 0ns -> 12.5ns] + wait_for_data(); // [time: 337.5ns -> 362.5ns] + wait_for_data(); // [time: 387.5ns -> 412.5ns] + wait_for_data(); // [time: 512.5ns -> 537.5ns] + wait_for_data(); // [time: 537.5ns -> 562.5ns] + wait_for_data(); // [time: 612.5ns -> 637.5ns] + wait_for_data(); // [time: 787.5ns -> 812.5ns] + wait_for_data(); // [time: 837.5ns -> 862.5ns] + recv(1); // [time: 862.5ns -> 887.5ns] + recv(2); // [time: 887.5ns -> 912.5ns] + recv(3); // [time: 912.5ns -> 937.5ns] + recv(4); // [time: 937.5ns -> 962.5ns] + recv(5); // [time: 962.5ns -> 987.5ns] + recv(6); // [time: 987.5ns -> 1012.5ns] + stall(7, 0); // [time: 1012.5ns -> 1037.5ns] + stall(7, 1); // [time: 1037.5ns -> 1050ns] +} + +// trace 1 +trace { + reset(); // [time: 0ns -> 12.5ns] + wait_for_data(); // [time: 337.5ns -> 362.5ns] + wait_for_data(); // [time: 387.5ns -> 412.5ns] + wait_for_data(); // [time: 512.5ns -> 537.5ns] + wait_for_data(); // [time: 537.5ns -> 562.5ns] + wait_for_data(); // [time: 612.5ns -> 637.5ns] + wait_for_data(); // [time: 787.5ns -> 812.5ns] + wait_for_data(); // [time: 837.5ns -> 862.5ns] + recv(1); // [time: 862.5ns -> 887.5ns] + recv(2); // [time: 887.5ns -> 912.5ns] + recv(3); // [time: 912.5ns -> 937.5ns] + recv(4); // [time: 937.5ns -> 962.5ns] + recv(5); // [time: 962.5ns -> 987.5ns] + recv(6); // [time: 987.5ns -> 1012.5ns] + stall(7, 1); // [time: 1037.5ns -> 1050ns] +} From 1a2bff0710d4019867b4c0b21e0a55293b680fa6 Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Wed, 18 Feb 2026 10:50:48 -0500 Subject: [PATCH 03/11] Move .tx files --- protocols/{ => tests/fpga-debugging/axi-stream-s2}/s2_buggy.tx | 0 protocols/{ => tests/fpga-debugging/axi-stream-s2}/s2_fixed.tx | 0 2 files changed, 0 insertions(+), 0 deletions(-) rename protocols/{ => tests/fpga-debugging/axi-stream-s2}/s2_buggy.tx (100%) rename protocols/{ => tests/fpga-debugging/axi-stream-s2}/s2_fixed.tx (100%) diff --git a/protocols/s2_buggy.tx b/protocols/tests/fpga-debugging/axi-stream-s2/s2_buggy.tx similarity index 100% rename from protocols/s2_buggy.tx rename to protocols/tests/fpga-debugging/axi-stream-s2/s2_buggy.tx diff --git a/protocols/s2_fixed.tx b/protocols/tests/fpga-debugging/axi-stream-s2/s2_fixed.tx similarity index 100% rename from protocols/s2_fixed.tx rename to protocols/tests/fpga-debugging/axi-stream-s2/s2_fixed.tx From 7819192f1bf4a495091d21086d5cb2dced83570a Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Wed, 18 Feb 2026 11:12:34 -0500 Subject: [PATCH 04/11] Ignore dotfiles in gitignore --- .gitignore | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/.gitignore b/.gitignore index aa7fd4bb..c521c699 100644 --- a/.gitignore +++ b/.gitignore @@ -13,3 +13,11 @@ monitor/tests/axi_output.txt *.csv # Allow benchmark results to be committed for CI regression testing !benchmark_results/*.csv +# Ignore all dotfiles and dotdirectories +.* +# But include the .github directory (CI files) +!.github/ +!.github/**/* +# And also include .gitignore + .python-version +!.gitignore +!.python-version From 738b4418cfa8db9e282ead72e29a6102dea17d22 Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Wed, 18 Feb 2026 11:12:39 -0500 Subject: [PATCH 05/11] Add Verilog wrapper file --- .../axi-stream-s2/faxis_master.v | 235 ++++++++++++++++++ .../fpga-debugging/axi-stream-s2/s2_buggy.tx | 1 + .../fpga-debugging/axi-stream-s2/s2_fixed.tx | 3 +- 3 files changed, 238 insertions(+), 1 deletion(-) create mode 100644 protocols/tests/fpga-debugging/axi-stream-s2/faxis_master.v diff --git a/protocols/tests/fpga-debugging/axi-stream-s2/faxis_master.v b/protocols/tests/fpga-debugging/axi-stream-s2/faxis_master.v new file mode 100644 index 00000000..06a1853a --- /dev/null +++ b/protocols/tests/fpga-debugging/axi-stream-s2/faxis_master.v @@ -0,0 +1,235 @@ +//////////////////////////////////////////////////////////////////////////////// +// +// Filename: faxis_master.v +// +// Project: WB2AXIPSP: bus bridges and other odds and ends +// +// Purpose: Formal properties for verifying the proper functionality of an +// AXI Stream master. +// +// Creator: Dan Gisselquist, Ph.D. +// Gisselquist Technology, LLC +// +//////////////////////////////////////////////////////////////////////////////// +// +// Copyright (C) 2019-2020, Gisselquist Technology, LLC +// +// This file is part of the WB2AXIP project. +// +// The WB2AXIP project contains free software and gateware, licensed under the +// Apache License, Version 2.0 (the "License"). You may not use this project, +// or this file, except in compliance with the License. You may obtain a copy +// of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, WITHOUT +// WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the +// License for the specific language governing permissions and limitations +// under the License. +// +//////////////////////////////////////////////////////////////////////////////// +// +// +`default_nettype none +// +module faxis_master #( + parameter F_MAX_PACKET = 0, + parameter F_MIN_PACKET = 0, + parameter F_MAX_STALL = 0, + parameter C_S_AXI_DATA_WIDTH = 32, + parameter C_S_AXI_ID_WIDTH = 1, + parameter C_S_AXI_ADDR_WIDTH = 1, + parameter C_S_AXI_USER_WIDTH = 1, + parameter [0:0] OPT_ASYNC_RESET = 1'b0, + // + // F_LGDEPTH is the number of bits necessary to represent a packets + // length + parameter F_LGDEPTH = 32, + // + localparam AW = C_S_AXI_ADDR_WIDTH, + localparam DW = C_S_AXI_DATA_WIDTH, + localparam IDW = C_S_AXI_ID_WIDTH, + localparam UW = C_S_AXI_USER_WIDTH + // + ) ( + // + input wire i_aclk, i_aresetn, + input wire i_tvalid, + input wire i_tready, + input wire [DW-1:0] i_tdata, + input wire [DW/8-1:0] i_tstrb, + input wire [DW/8-1:0] i_tkeep, + input wire i_tlast, + input wire [(IDW>0?IDW:1)-1:0] i_tid, + input wire [(AW>0?AW:1)-1:0] i_tdest, + input wire [(UW>0?UW:1)-1:0] i_tuser, + // + output reg [F_LGDEPTH-1:0] f_bytecount, + (* anyconst *) output reg [AW+IDW-1:0] f_routecheck + ); + +`define SLAVE_ASSUME assert +`ifndef VERILATOR + `define SLAVE_ASSERT assume +`else + function void empty(input int i); + endfunction + `define SLAVE_ASSERT empty +`endif + + localparam F_STALLBITS = (F_MAX_STALL <= 1) + ? 1 : $clog2(F_MAX_STALL+2); + reg f_past_valid; + reg [F_LGDEPTH-1:0] f_vbytes; + reg [F_STALLBITS-1:0] f_stall_count; + integer iB; + genvar k; + + // + // f_past_valid is used to make certain that temporal assertions + // depending upon past values depend upon *valid* past values. + // It is true for all clocks other than the first clock. + initial f_past_valid = 1'b0; + always @(posedge i_aclk) + f_past_valid <= 1'b1; + + // + // Reset should always be active (low) initially + always @(posedge i_aclk) + if (!f_past_valid) + `SLAVE_ASSUME(!i_aresetn); + + // + // During and following a reset, TVALID should be deasserted + always @(posedge i_aclk) + if ((!f_past_valid)||(!i_aresetn && OPT_ASYNC_RESET)||($past(!i_aresetn))) + `SLAVE_ASSUME(!i_tvalid); + + // + // If TVALID but not TREADY, then the master isn't allowed to change + // anything until the slave asserts TREADY. + always @(posedge i_aclk) + if ((f_past_valid)&&($past(i_aresetn))&&(!OPT_ASYNC_RESET || i_aresetn) + &&($past(i_tvalid))&&(!$past(i_tready))) + begin + `SLAVE_ASSUME(i_tvalid); + `SLAVE_ASSUME($stable(i_tstrb)); + `SLAVE_ASSUME($stable(i_tkeep)); + `SLAVE_ASSUME($stable(i_tlast)); + `SLAVE_ASSUME($stable(i_tid)); + `SLAVE_ASSUME($stable(i_tdest)); + `SLAVE_ASSUME($stable(i_tuser)); + end + + generate for(k=0; k 0) + begin : MAX_PACKET + + always @(*) + `SLAVE_ASSUME(f_bytecount + f_vbytes <= F_MAX_PACKET); + + end endgenerate + + // + // F_MIN_PACKET + // + // An optoinal check, forcing a minimum packet length + generate if (F_MIN_PACKET > 0) + begin : MIN_PACKET + + always @(*) + if (i_tvalid && i_tlast) + `SLAVE_ASSUME(f_bytecount + f_vbytes >= F_MIN_PACKET); + + end endgenerate + + // + // F_MAX_STALL + // + // Another optional check, this time insisting that the READY flag can + // only be low for up to F_MAX_STALL clocks. + // + generate if (F_MAX_STALL > 0) + begin : MAX_STALL_CHECK + + always @(*) + `SLAVE_ASSERT(f_stall_count < F_MAX_STALL); + + end endgenerate +endmodule +`undef SLAVE_ASSUME +`undef SLAVE_ASSERT diff --git a/protocols/tests/fpga-debugging/axi-stream-s2/s2_buggy.tx b/protocols/tests/fpga-debugging/axi-stream-s2/s2_buggy.tx index 40a7ea8e..eb6eef33 100644 --- a/protocols/tests/fpga-debugging/axi-stream-s2/s2_buggy.tx +++ b/protocols/tests/fpga-debugging/axi-stream-s2/s2_buggy.tx @@ -1,3 +1,4 @@ +// ARGS: --verilog fpga-debugging/axi-stream-s2/s2_buggy.v fpga-debugging/axi-stream-s2/faxis_master.v --protocol fpga-debugging/axi-stream-s2/s2_buggy.prot --module faxis_master // trace 0 trace { reset(); // [time: 0ns -> 12.5ns] diff --git a/protocols/tests/fpga-debugging/axi-stream-s2/s2_fixed.tx b/protocols/tests/fpga-debugging/axi-stream-s2/s2_fixed.tx index ecb7f33b..5af86396 100644 --- a/protocols/tests/fpga-debugging/axi-stream-s2/s2_fixed.tx +++ b/protocols/tests/fpga-debugging/axi-stream-s2/s2_fixed.tx @@ -1,4 +1,5 @@ -// Same as s2_buggy.tx for now +// ARGS: --verilog fpga-debugging/axi-stream-s2/s2_fixed.v fpga-debugging/axi-stream-s2/faxis_master.v --protocol fpga-debugging/axi-stream-s2/s2_fixed.prot --module faxis_master +// These traces are the same as s2_buggy.tx for now // trace 0 trace { reset(); // [time: 0ns -> 12.5ns] From 09daadbee67ea462305774c222d4580f3cfbd3cf Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Wed, 18 Feb 2026 11:33:53 -0500 Subject: [PATCH 06/11] Add missing step() to end of stall transaction for monitor files --- .../fpga-debugging/axi-stream-s2/s2_buggy.out | 22 +---------------- .../axi-stream-s2/s2_buggy.prot | 2 ++ .../fpga-debugging/axi-stream-s2/s2_fixed.out | 24 +------------------ .../axi-stream-s2/s2_fixed.prot | 2 ++ 4 files changed, 6 insertions(+), 44 deletions(-) diff --git a/monitor/tests/fpga-debugging/axi-stream-s2/s2_buggy.out b/monitor/tests/fpga-debugging/axi-stream-s2/s2_buggy.out index 40a7ea8e..343c9ed9 100644 --- a/monitor/tests/fpga-debugging/axi-stream-s2/s2_buggy.out +++ b/monitor/tests/fpga-debugging/axi-stream-s2/s2_buggy.out @@ -14,25 +14,5 @@ trace { recv(4); // [time: 937.5ns -> 962.5ns] recv(5); // [time: 962.5ns -> 987.5ns] recv(6); // [time: 987.5ns -> 1012.5ns] - stall(7, 0); // [time: 1012.5ns -> 1037.5ns] - stall(7, 1); // [time: 1037.5ns -> 1050ns] -} - -// trace 1 -trace { - reset(); // [time: 0ns -> 12.5ns] - wait_for_data(); // [time: 337.5ns -> 362.5ns] - wait_for_data(); // [time: 387.5ns -> 412.5ns] - wait_for_data(); // [time: 512.5ns -> 537.5ns] - wait_for_data(); // [time: 537.5ns -> 562.5ns] - wait_for_data(); // [time: 612.5ns -> 637.5ns] - wait_for_data(); // [time: 787.5ns -> 812.5ns] - wait_for_data(); // [time: 837.5ns -> 862.5ns] - recv(1); // [time: 862.5ns -> 887.5ns] - recv(2); // [time: 887.5ns -> 912.5ns] - recv(3); // [time: 912.5ns -> 937.5ns] - recv(4); // [time: 937.5ns -> 962.5ns] - recv(5); // [time: 962.5ns -> 987.5ns] - recv(6); // [time: 987.5ns -> 1012.5ns] - stall(7, 1); // [time: 1037.5ns -> 1050ns] + stall(7, 0); // [time: 1012.5ns -> 1050ns] } diff --git a/monitor/tests/fpga-debugging/axi-stream-s2/s2_buggy.prot b/monitor/tests/fpga-debugging/axi-stream-s2/s2_buggy.prot index a1648cf1..0f0c81d8 100644 --- a/monitor/tests/fpga-debugging/axi-stream-s2/s2_buggy.prot +++ b/monitor/tests/fpga-debugging/axi-stream-s2/s2_buggy.prot @@ -89,6 +89,8 @@ prot stall(out data: u32, out last: u1) { // Verify outputs remained stable during the stall assert_eq(DUT.i_tdata, data); assert_eq(DUT.i_tlast, last); + + step(); } // WAIT_FOR_DATA: Receiver is ready but no data is available diff --git a/monitor/tests/fpga-debugging/axi-stream-s2/s2_fixed.out b/monitor/tests/fpga-debugging/axi-stream-s2/s2_fixed.out index 8ad4900a..190a394f 100644 --- a/monitor/tests/fpga-debugging/axi-stream-s2/s2_fixed.out +++ b/monitor/tests/fpga-debugging/axi-stream-s2/s2_fixed.out @@ -14,34 +14,12 @@ trace { recv(4); // [time: 937.5ns -> 962.5ns] recv(5); // [time: 962.5ns -> 987.5ns] recv(6); // [time: 987.5ns -> 1012.5ns] - stall(7, 0); // [time: 1012.5ns -> 1037.5ns] - stall(7, 0); // [time: 1037.5ns -> 1062.5ns] + stall(7, 0); // [time: 1012.5ns -> 1062.5ns] reset(); // [time: 1062.5ns -> 1087.5ns] reset(); // [time: 1087.5ns -> 1100ns] } // trace 1 -trace { - reset(); // [time: 0ns -> 12.5ns] - wait_for_data(); // [time: 337.5ns -> 362.5ns] - wait_for_data(); // [time: 387.5ns -> 412.5ns] - wait_for_data(); // [time: 512.5ns -> 537.5ns] - wait_for_data(); // [time: 537.5ns -> 562.5ns] - wait_for_data(); // [time: 612.5ns -> 637.5ns] - wait_for_data(); // [time: 787.5ns -> 812.5ns] - wait_for_data(); // [time: 837.5ns -> 862.5ns] - recv(1); // [time: 862.5ns -> 887.5ns] - recv(2); // [time: 887.5ns -> 912.5ns] - recv(3); // [time: 912.5ns -> 937.5ns] - recv(4); // [time: 937.5ns -> 962.5ns] - recv(5); // [time: 962.5ns -> 987.5ns] - recv(6); // [time: 987.5ns -> 1012.5ns] - stall(7, 0); // [time: 1012.5ns -> 1037.5ns] - reset(); // [time: 1062.5ns -> 1087.5ns] - reset(); // [time: 1087.5ns -> 1100ns] -} - -// trace 2 trace { reset(); // [time: 0ns -> 12.5ns] wait_for_data(); // [time: 337.5ns -> 362.5ns] diff --git a/monitor/tests/fpga-debugging/axi-stream-s2/s2_fixed.prot b/monitor/tests/fpga-debugging/axi-stream-s2/s2_fixed.prot index afb0eccc..50a2b1d2 100644 --- a/monitor/tests/fpga-debugging/axi-stream-s2/s2_fixed.prot +++ b/monitor/tests/fpga-debugging/axi-stream-s2/s2_fixed.prot @@ -90,6 +90,8 @@ prot stall(out data: u32, out last: u1) { // Verify outputs remained stable during the stall assert_eq(DUT.i_tdata, data); assert_eq(DUT.i_tlast, last); + + step(); } // WAIT_FOR_DATA: Receiver is ready but no data is available From f1faef5957bdb579cb5904d7045da975ed306da8 Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Wed, 18 Feb 2026 11:36:50 -0500 Subject: [PATCH 07/11] Update input traces for interpreter --- .../axi-stream-s2/s2_buggy.prot | 80 ++++++++++--------- .../fpga-debugging/axi-stream-s2/s2_buggy.tx | 63 ++++++++++++++- .../axi-stream-s2/s2_fixed.prot | 80 ++++++++++--------- .../fpga-debugging/axi-stream-s2/s2_fixed.tx | 68 ++++++++++++++-- 4 files changed, 204 insertions(+), 87 deletions(-) diff --git a/protocols/tests/fpga-debugging/axi-stream-s2/s2_buggy.prot b/protocols/tests/fpga-debugging/axi-stream-s2/s2_buggy.prot index a1648cf1..5f13da22 100644 --- a/protocols/tests/fpga-debugging/axi-stream-s2/s2_buggy.prot +++ b/protocols/tests/fpga-debugging/axi-stream-s2/s2_buggy.prot @@ -3,109 +3,111 @@ // Source (manager) that outputs a sequence of 8 words struct AXISManager { // Control signals - in i_aresetn: u1, // Active-low reset + in M_AXIS_ARESETN: u1, // Active-low reset // AXI-Stream manager outputs (from DUT perspective) - out i_tvalid: u1, // manager has valid data - out i_tdata: u32, // Data payload - out i_tstrb: u4, // Byte strobe (always 0xF) - out i_tlast: u1, // Last word in packet + out M_AXIS_TVALID: u1, // manager has valid data + out M_AXIS_TDATA: u32, // Data payload + out M_AXIS_TSTRB: u4, // Byte strobe (always 0xF) + out M_AXIS_TLAST: u1, // Last word in packet // AXI-Stream sub-ordinate input - in i_tready: u1, // Downstream ready to accept + in M_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.i_aresetn := 1'b0; // Assert reset (active-low) - DUT.i_tready := 1'b0; + DUT.M_AXIS_ARESETN := 1'b0; // Assert reset (active-low) + DUT.M_AXIS_TREADY := 1'b0; step(); } // RECV: Receive one data word from the AXI-Stream manager -// Data transfer occurs when i_tvalid and i_tready are both 1 -// Only matches when data is immediately available (i_tvalid = 1) +// Data transfer occurs when M_AXIS_TVALID and M_AXIS_TREADY are both 1 +// Only matches when data is immediately available (M_AXIS_TVALID = 1) // // Output Arguments: // data - Expected payload from manager prot recv( out data: u32, ) { - DUT.i_aresetn := 1'b1; // Keep out of reset - DUT.i_tready := 1'b1; // Signal ready to receive + DUT.M_AXIS_ARESETN := 1'b1; // Keep out of reset + DUT.M_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.i_tvalid, 1'b1); + assert_eq(DUT.M_AXIS_TVALID, 1'b1); // Verify output data - assert_eq(DUT.i_tdata, data); + assert_eq(DUT.M_AXIS_TDATA, data); // One cycle for the transfer to complete step(); } -// RECV_LAST: Receive the last data word (with i_tlast asserted) -// This verifies both the data and that i_tlast is properly set -// Only matches when data is immediately available (i_tvalid = 1) +// RECV_LAST: Receive the last data word (with M_AXIS_TLAST asserted) +// This verifies both the data and that M_AXIS_TLAST is properly set +// Only matches when data is immediately available (M_AXIS_TVALID = 1) // // Output Arguments: // data - Expected payload from manager (should be the last word) prot recv_last( out data: u32, ) { - DUT.i_aresetn := 1'b1; // Keep out of reset - DUT.i_tready := 1'b1; // Signal ready to receive + DUT.M_AXIS_ARESETN := 1'b1; // Keep out of reset + DUT.M_AXIS_TREADY := 1'b1; // Signal ready to receive // Only matches when data is available - assert_eq(DUT.i_tvalid, 1'b1); + assert_eq(DUT.M_AXIS_TVALID, 1'b1); - // Verify output data and i_tlast - assert_eq(DUT.i_tdata, data); - assert_eq(DUT.i_tlast, 1'b1); + // Verify output data and M_AXIS_TLAST + assert_eq(DUT.M_AXIS_TDATA, data); + assert_eq(DUT.M_AXIS_TLAST, 1'b1); // One cycle for the transfer to complete step(); } -// STALL: Assert backpressure (i_tready=0) while manager has valid data +// STALL: Assert backpressure (M_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 i_tvalid=1 (i.e. there is some valid data and it's available to stall) +// Only matches when the waveform contains M_AXIS_TVALID=1 (i.e. there is some valid data and it's available to stall) prot stall(out data: u32, out last: u1) { - DUT.i_aresetn := 1'b1; // Keep out of reset - DUT.i_tready := 1'b0; // Apply backpressure + DUT.M_AXIS_ARESETN := 1'b1; // Keep out of reset + DUT.M_AXIS_TREADY := 1'b0; // Apply backpressure // Stall only applies when manager has valid data - // If i_tvalid=0, this fails and we instead have an `idle` transaction - assert_eq(DUT.i_tvalid, 1'b1); + // If M_AXIS_TVALID=0, this fails and we instead have an `idle` transaction + assert_eq(DUT.M_AXIS_TVALID, 1'b1); // Capture output values before the stall cycle - assert_eq(DUT.i_tdata, data); - assert_eq(DUT.i_tlast, last); + assert_eq(DUT.M_AXIS_TDATA, data); + assert_eq(DUT.M_AXIS_TLAST, last); step(); // Verify outputs remained stable during the stall - assert_eq(DUT.i_tdata, data); - assert_eq(DUT.i_tlast, last); + assert_eq(DUT.M_AXIS_TDATA, data); + assert_eq(DUT.M_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.i_aresetn := 1'b1; // Keep out of reset - DUT.i_tready := 1'b1; + DUT.M_AXIS_ARESETN := 1'b1; // Keep out of reset + DUT.M_AXIS_TREADY := 1'b1; // Only matches when no data is available - assert_eq(DUT.i_tvalid, 1'b0); + assert_eq(DUT.M_AXIS_TVALID, 1'b0); step(); } -// IDLE: No transaction - i_tready is deasserted +// IDLE: No transaction - M_AXIS_TREADY is deasserted #[idle] prot idle() { - DUT.i_aresetn := 1'b1; // Keep out of reset - DUT.i_tready := 1'b0; + DUT.M_AXIS_ARESETN := 1'b1; // Keep out of reset + DUT.M_AXIS_TREADY := 1'b0; step(); } diff --git a/protocols/tests/fpga-debugging/axi-stream-s2/s2_buggy.tx b/protocols/tests/fpga-debugging/axi-stream-s2/s2_buggy.tx index eb6eef33..5e6ebf20 100644 --- a/protocols/tests/fpga-debugging/axi-stream-s2/s2_buggy.tx +++ b/protocols/tests/fpga-debugging/axi-stream-s2/s2_buggy.tx @@ -1,13 +1,41 @@ -// ARGS: --verilog fpga-debugging/axi-stream-s2/s2_buggy.v fpga-debugging/axi-stream-s2/faxis_master.v --protocol fpga-debugging/axi-stream-s2/s2_buggy.prot --module faxis_master +// ARGS: --verilog fpga-debugging/axi-stream-s2/s2_buggy.v fpga-debugging/axi-stream-s2/faxis_master.v --protocol fpga-debugging/axi-stream-s2/s2_buggy.prot --module xlnxstream_2018_3 + // trace 0 trace { reset(); // [time: 0ns -> 12.5ns] + idle(); // [time: 12.5ns -> 37.5ns] + idle(); // [time: 37.5ns -> 62.5ns] + idle(); // [time: 62.5ns -> 87.5ns] + idle(); // [time: 87.5ns -> 112.5ns] + idle(); // [time: 112.5ns -> 137.5ns] + idle(); // [time: 137.5ns -> 162.5ns] + idle(); // [time: 162.5ns -> 187.5ns] + idle(); // [time: 187.5ns -> 212.5ns] + idle(); // [time: 212.5ns -> 237.5ns] + idle(); // [time: 237.5ns -> 262.5ns] + idle(); // [time: 262.5ns -> 287.5ns] + idle(); // [time: 287.5ns -> 312.5ns] + idle(); // [time: 312.5ns -> 337.5ns] wait_for_data(); // [time: 337.5ns -> 362.5ns] + idle(); // [time: 362.5ns -> 387.5ns] wait_for_data(); // [time: 387.5ns -> 412.5ns] + idle(); // [time: 412.5ns -> 437.5ns] + idle(); // [time: 437.5ns -> 462.5ns] + idle(); // [time: 462.5ns -> 487.5ns] + idle(); // [time: 487.5ns -> 512.5ns] wait_for_data(); // [time: 512.5ns -> 537.5ns] wait_for_data(); // [time: 537.5ns -> 562.5ns] + idle(); // [time: 562.5ns -> 587.5ns] + idle(); // [time: 587.5ns -> 612.5ns] wait_for_data(); // [time: 612.5ns -> 637.5ns] + idle(); // [time: 637.5ns -> 662.5ns] + idle(); // [time: 662.5ns -> 687.5ns] + idle(); // [time: 687.5ns -> 712.5ns] + idle(); // [time: 712.5ns -> 737.5ns] + idle(); // [time: 737.5ns -> 762.5ns] + idle(); // [time: 762.5ns -> 787.5ns] wait_for_data(); // [time: 787.5ns -> 812.5ns] + idle(); // [time: 812.5ns -> 837.5ns] wait_for_data(); // [time: 837.5ns -> 862.5ns] recv(1); // [time: 862.5ns -> 887.5ns] recv(2); // [time: 887.5ns -> 912.5ns] @@ -15,19 +43,45 @@ trace { recv(4); // [time: 937.5ns -> 962.5ns] recv(5); // [time: 962.5ns -> 987.5ns] recv(6); // [time: 987.5ns -> 1012.5ns] - stall(7, 0); // [time: 1012.5ns -> 1037.5ns] - stall(7, 1); // [time: 1037.5ns -> 1050ns] + stall(7, 0); // [time: 1012.5ns -> 1050ns] } // trace 1 trace { reset(); // [time: 0ns -> 12.5ns] + idle(); // [time: 12.5ns -> 37.5ns] + idle(); // [time: 37.5ns -> 62.5ns] + idle(); // [time: 62.5ns -> 87.5ns] + idle(); // [time: 87.5ns -> 112.5ns] + idle(); // [time: 112.5ns -> 137.5ns] + idle(); // [time: 137.5ns -> 162.5ns] + idle(); // [time: 162.5ns -> 187.5ns] + idle(); // [time: 187.5ns -> 212.5ns] + idle(); // [time: 212.5ns -> 237.5ns] + idle(); // [time: 237.5ns -> 262.5ns] + idle(); // [time: 262.5ns -> 287.5ns] + idle(); // [time: 287.5ns -> 312.5ns] + idle(); // [time: 312.5ns -> 337.5ns] wait_for_data(); // [time: 337.5ns -> 362.5ns] + idle(); // [time: 362.5ns -> 387.5ns] wait_for_data(); // [time: 387.5ns -> 412.5ns] + idle(); // [time: 412.5ns -> 437.5ns] + idle(); // [time: 437.5ns -> 462.5ns] + idle(); // [time: 462.5ns -> 487.5ns] + idle(); // [time: 487.5ns -> 512.5ns] wait_for_data(); // [time: 512.5ns -> 537.5ns] wait_for_data(); // [time: 537.5ns -> 562.5ns] + idle(); // [time: 562.5ns -> 587.5ns] + idle(); // [time: 587.5ns -> 612.5ns] wait_for_data(); // [time: 612.5ns -> 637.5ns] + idle(); // [time: 637.5ns -> 662.5ns] + idle(); // [time: 662.5ns -> 687.5ns] + idle(); // [time: 687.5ns -> 712.5ns] + idle(); // [time: 712.5ns -> 737.5ns] + idle(); // [time: 737.5ns -> 762.5ns] + idle(); // [time: 762.5ns -> 787.5ns] wait_for_data(); // [time: 787.5ns -> 812.5ns] + idle(); // [time: 812.5ns -> 837.5ns] wait_for_data(); // [time: 837.5ns -> 862.5ns] recv(1); // [time: 862.5ns -> 887.5ns] recv(2); // [time: 887.5ns -> 912.5ns] @@ -35,5 +89,6 @@ trace { recv(4); // [time: 937.5ns -> 962.5ns] recv(5); // [time: 962.5ns -> 987.5ns] recv(6); // [time: 987.5ns -> 1012.5ns] - stall(7, 1); // [time: 1037.5ns -> 1050ns] + idle(); // [time: 1012.5ns -> 1037.5ns] + idle(); // [time: 1037.5ns -> 1050ns] } diff --git a/protocols/tests/fpga-debugging/axi-stream-s2/s2_fixed.prot b/protocols/tests/fpga-debugging/axi-stream-s2/s2_fixed.prot index afb0eccc..46411502 100644 --- a/protocols/tests/fpga-debugging/axi-stream-s2/s2_fixed.prot +++ b/protocols/tests/fpga-debugging/axi-stream-s2/s2_fixed.prot @@ -4,110 +4,112 @@ // Source (manager) that outputs a sequence of 8 words struct AXISManager { // Control signals - in i_aresetn: u1, // Active-low reset + in M_AXIS_ARESETN: u1, // Active-low reset // AXI-Stream manager outputs (from DUT perspective) - out i_tvalid: u1, // manager has valid data - out i_tdata: u32, // Data payload - out i_tstrb: u4, // Byte strobe (always 0xF) - out i_tlast: u1, // Last word in packet + out M_AXIS_TVALID: u1, // manager has valid data + out M_AXIS_TDATA: u32, // Data payload + out M_AXIS_TSTRB: u4, // Byte strobe (always 0xF) + out M_AXIS_TLAST: u1, // Last word in packet // AXI-Stream sub-ordinate input - in i_tready: u1, // Downstream ready to accept + in M_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.i_aresetn := 1'b0; // Assert reset (active-low) - DUT.i_tready := 1'b0; + DUT.M_AXIS_ARESETN := 1'b0; // Assert reset (active-low) + DUT.M_AXIS_TREADY := 1'b0; step(); } // RECV: Receive one data word from the AXI-Stream manager -// Data transfer occurs when i_tvalid and i_tready are both 1 -// Only matches when data is immediately available (i_tvalid = 1) +// Data transfer occurs when M_AXIS_TVALID and M_AXIS_TREADY are both 1 +// Only matches when data is immediately available (M_AXIS_TVALID = 1) // // Output Arguments: // data - Expected payload from manager prot recv( out data: u32, ) { - DUT.i_aresetn := 1'b1; // Keep out of reset - DUT.i_tready := 1'b1; // Signal ready to receive + DUT.M_AXIS_ARESETN := 1'b1; // Keep out of reset + DUT.M_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.i_tvalid, 1'b1); + assert_eq(DUT.M_AXIS_TVALID, 1'b1); // Verify output data - assert_eq(DUT.i_tdata, data); + assert_eq(DUT.M_AXIS_TDATA, data); // One cycle for the transfer to complete step(); } -// RECV_LAST: Receive the last data word (with i_tlast asserted) -// This verifies both the data and that i_tlast is properly set -// Only matches when data is immediately available (i_tvalid = 1) +// RECV_LAST: Receive the last data word (with M_AXIS_TLAST asserted) +// This verifies both the data and that M_AXIS_TLAST is properly set +// Only matches when data is immediately available (M_AXIS_TVALID = 1) // // Output Arguments: // data - Expected payload from manager (should be the last word) prot recv_last( out data: u32, ) { - DUT.i_aresetn := 1'b1; // Keep out of reset - DUT.i_tready := 1'b1; // Signal ready to receive + DUT.M_AXIS_ARESETN := 1'b1; // Keep out of reset + DUT.M_AXIS_TREADY := 1'b1; // Signal ready to receive // Only matches when data is available - assert_eq(DUT.i_tvalid, 1'b1); + assert_eq(DUT.M_AXIS_TVALID, 1'b1); - // Verify output data and i_tlast - assert_eq(DUT.i_tdata, data); - assert_eq(DUT.i_tlast, 1'b1); + // Verify output data and M_AXIS_TLAST + assert_eq(DUT.M_AXIS_TDATA, data); + assert_eq(DUT.M_AXIS_TLAST, 1'b1); // One cycle for the transfer to complete step(); } -// STALL: Assert backpressure (i_tready=0) while manager has valid data +// STALL: Assert backpressure (M_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 i_tvalid=1 (i.e. there is some valid data and it's available to stall) +// Only matches when the waveform contains M_AXIS_TVALID=1 (i.e. there is some valid data and it's available to stall) prot stall(out data: u32, out last: u1) { - DUT.i_aresetn := 1'b1; // Keep out of reset - DUT.i_tready := 1'b0; // Apply backpressure + DUT.M_AXIS_ARESETN := 1'b1; // Keep out of reset + DUT.M_AXIS_TREADY := 1'b0; // Apply backpressure // Stall only applies when manager has valid data - // If i_tvalid=0, this fails and we instead have an `idle` transaction - assert_eq(DUT.i_tvalid, 1'b1); + // If M_AXIS_TVALID=0, this fails and we instead have an `idle` transaction + assert_eq(DUT.M_AXIS_TVALID, 1'b1); // Capture output values before the stall cycle - assert_eq(DUT.i_tdata, data); - assert_eq(DUT.i_tlast, last); + assert_eq(DUT.M_AXIS_TDATA, data); + assert_eq(DUT.M_AXIS_TLAST, last); step(); // Verify outputs remained stable during the stall - assert_eq(DUT.i_tdata, data); - assert_eq(DUT.i_tlast, last); + assert_eq(DUT.M_AXIS_TDATA, data); + assert_eq(DUT.M_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.i_aresetn := 1'b1; // Keep out of reset - DUT.i_tready := 1'b1; + DUT.M_AXIS_ARESETN := 1'b1; // Keep out of reset + DUT.M_AXIS_TREADY := 1'b1; // Only matches when no data is available - assert_eq(DUT.i_tvalid, 1'b0); + assert_eq(DUT.M_AXIS_TVALID, 1'b0); step(); } -// IDLE: No transaction - i_tready is deasserted +// IDLE: No transaction - M_AXIS_TREADY is deasserted #[idle] prot idle() { - DUT.i_aresetn := 1'b1; // Keep out of reset - DUT.i_tready := 1'b0; + DUT.M_AXIS_ARESETN := 1'b1; // Keep out of reset + DUT.M_AXIS_TREADY := 1'b0; step(); } diff --git a/protocols/tests/fpga-debugging/axi-stream-s2/s2_fixed.tx b/protocols/tests/fpga-debugging/axi-stream-s2/s2_fixed.tx index 5af86396..f4f06b4b 100644 --- a/protocols/tests/fpga-debugging/axi-stream-s2/s2_fixed.tx +++ b/protocols/tests/fpga-debugging/axi-stream-s2/s2_fixed.tx @@ -1,14 +1,41 @@ -// ARGS: --verilog fpga-debugging/axi-stream-s2/s2_fixed.v fpga-debugging/axi-stream-s2/faxis_master.v --protocol fpga-debugging/axi-stream-s2/s2_fixed.prot --module faxis_master -// These traces are the same as s2_buggy.tx for now +// ARGS: --verilog fpga-debugging/axi-stream-s2/s2_fixed.v fpga-debugging/axi-stream-s2/faxis_master.v --protocol fpga-debugging/axi-stream-s2/s2_fixed.prot --module xlnxstream_2018_3 + // trace 0 trace { reset(); // [time: 0ns -> 12.5ns] + idle(); // [time: 12.5ns -> 37.5ns] + idle(); // [time: 37.5ns -> 62.5ns] + idle(); // [time: 62.5ns -> 87.5ns] + idle(); // [time: 87.5ns -> 112.5ns] + idle(); // [time: 112.5ns -> 137.5ns] + idle(); // [time: 137.5ns -> 162.5ns] + idle(); // [time: 162.5ns -> 187.5ns] + idle(); // [time: 187.5ns -> 212.5ns] + idle(); // [time: 212.5ns -> 237.5ns] + idle(); // [time: 237.5ns -> 262.5ns] + idle(); // [time: 262.5ns -> 287.5ns] + idle(); // [time: 287.5ns -> 312.5ns] + idle(); // [time: 312.5ns -> 337.5ns] wait_for_data(); // [time: 337.5ns -> 362.5ns] + idle(); // [time: 362.5ns -> 387.5ns] wait_for_data(); // [time: 387.5ns -> 412.5ns] + idle(); // [time: 412.5ns -> 437.5ns] + idle(); // [time: 437.5ns -> 462.5ns] + idle(); // [time: 462.5ns -> 487.5ns] + idle(); // [time: 487.5ns -> 512.5ns] wait_for_data(); // [time: 512.5ns -> 537.5ns] wait_for_data(); // [time: 537.5ns -> 562.5ns] + idle(); // [time: 562.5ns -> 587.5ns] + idle(); // [time: 587.5ns -> 612.5ns] wait_for_data(); // [time: 612.5ns -> 637.5ns] + idle(); // [time: 637.5ns -> 662.5ns] + idle(); // [time: 662.5ns -> 687.5ns] + idle(); // [time: 687.5ns -> 712.5ns] + idle(); // [time: 712.5ns -> 737.5ns] + idle(); // [time: 737.5ns -> 762.5ns] + idle(); // [time: 762.5ns -> 787.5ns] wait_for_data(); // [time: 787.5ns -> 812.5ns] + idle(); // [time: 812.5ns -> 837.5ns] wait_for_data(); // [time: 837.5ns -> 862.5ns] recv(1); // [time: 862.5ns -> 887.5ns] recv(2); // [time: 887.5ns -> 912.5ns] @@ -16,19 +43,47 @@ trace { recv(4); // [time: 937.5ns -> 962.5ns] recv(5); // [time: 962.5ns -> 987.5ns] recv(6); // [time: 987.5ns -> 1012.5ns] - stall(7, 0); // [time: 1012.5ns -> 1037.5ns] - stall(7, 1); // [time: 1037.5ns -> 1050ns] + stall(7, 0); // [time: 1012.5ns -> 1062.5ns] + reset(); // [time: 1062.5ns -> 1087.5ns] + reset(); // [time: 1087.5ns -> 1100ns] } // trace 1 trace { reset(); // [time: 0ns -> 12.5ns] + idle(); // [time: 12.5ns -> 37.5ns] + idle(); // [time: 37.5ns -> 62.5ns] + idle(); // [time: 62.5ns -> 87.5ns] + idle(); // [time: 87.5ns -> 112.5ns] + idle(); // [time: 112.5ns -> 137.5ns] + idle(); // [time: 137.5ns -> 162.5ns] + idle(); // [time: 162.5ns -> 187.5ns] + idle(); // [time: 187.5ns -> 212.5ns] + idle(); // [time: 212.5ns -> 237.5ns] + idle(); // [time: 237.5ns -> 262.5ns] + idle(); // [time: 262.5ns -> 287.5ns] + idle(); // [time: 287.5ns -> 312.5ns] + idle(); // [time: 312.5ns -> 337.5ns] wait_for_data(); // [time: 337.5ns -> 362.5ns] + idle(); // [time: 362.5ns -> 387.5ns] wait_for_data(); // [time: 387.5ns -> 412.5ns] + idle(); // [time: 412.5ns -> 437.5ns] + idle(); // [time: 437.5ns -> 462.5ns] + idle(); // [time: 462.5ns -> 487.5ns] + idle(); // [time: 487.5ns -> 512.5ns] wait_for_data(); // [time: 512.5ns -> 537.5ns] wait_for_data(); // [time: 537.5ns -> 562.5ns] + idle(); // [time: 562.5ns -> 587.5ns] + idle(); // [time: 587.5ns -> 612.5ns] wait_for_data(); // [time: 612.5ns -> 637.5ns] + idle(); // [time: 637.5ns -> 662.5ns] + idle(); // [time: 662.5ns -> 687.5ns] + idle(); // [time: 687.5ns -> 712.5ns] + idle(); // [time: 712.5ns -> 737.5ns] + idle(); // [time: 737.5ns -> 762.5ns] + idle(); // [time: 762.5ns -> 787.5ns] wait_for_data(); // [time: 787.5ns -> 812.5ns] + idle(); // [time: 812.5ns -> 837.5ns] wait_for_data(); // [time: 837.5ns -> 862.5ns] recv(1); // [time: 862.5ns -> 887.5ns] recv(2); // [time: 887.5ns -> 912.5ns] @@ -36,5 +91,8 @@ trace { recv(4); // [time: 937.5ns -> 962.5ns] recv(5); // [time: 962.5ns -> 987.5ns] recv(6); // [time: 987.5ns -> 1012.5ns] - stall(7, 1); // [time: 1037.5ns -> 1050ns] + idle(); // [time: 1012.5ns -> 1037.5ns] + idle(); // [time: 1037.5ns -> 1062.5ns] + reset(); // [time: 1062.5ns -> 1087.5ns] + reset(); // [time: 1087.5ns -> 1100ns] } From 7fc73670fddf72fe931e0af1c8fd0144a3385496 Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Wed, 18 Feb 2026 11:43:58 -0500 Subject: [PATCH 08/11] Update Turnt output --- .../tests/fpga-debugging/axi-stream-s2/s2_buggy.out | 11 +++++++++++ .../tests/fpga-debugging/axi-stream-s2/s2_buggy.tx | 1 + .../tests/fpga-debugging/axi-stream-s2/s2_fixed.out | 5 +++++ 3 files changed, 17 insertions(+) diff --git a/protocols/tests/fpga-debugging/axi-stream-s2/s2_buggy.out b/protocols/tests/fpga-debugging/axi-stream-s2/s2_buggy.out index e69de29b..a39f87b6 100644 --- a/protocols/tests/fpga-debugging/axi-stream-s2/s2_buggy.out +++ b/protocols/tests/fpga-debugging/axi-stream-s2/s2_buggy.out @@ -0,0 +1,11 @@ +error: The two expressions did not evaluate to the same value + ┌─ fpga-debugging/axi-stream-s2/s2_buggy.prot:91:15 + │ +91 │ assert_eq(DUT.M_AXIS_TLAST, last); + │ ^^^^^^^^^^^^^^^^^^^^^^ LHS Value: 1, RHS Value: 0 + +Trace 0 execution failed. + +--- + +Trace 1 executed successfully! diff --git a/protocols/tests/fpga-debugging/axi-stream-s2/s2_buggy.tx b/protocols/tests/fpga-debugging/axi-stream-s2/s2_buggy.tx index 5e6ebf20..438631d5 100644 --- a/protocols/tests/fpga-debugging/axi-stream-s2/s2_buggy.tx +++ b/protocols/tests/fpga-debugging/axi-stream-s2/s2_buggy.tx @@ -1,4 +1,5 @@ // ARGS: --verilog fpga-debugging/axi-stream-s2/s2_buggy.v fpga-debugging/axi-stream-s2/faxis_master.v --protocol fpga-debugging/axi-stream-s2/s2_buggy.prot --module xlnxstream_2018_3 +// RETURN: 101 // trace 0 trace { diff --git a/protocols/tests/fpga-debugging/axi-stream-s2/s2_fixed.out b/protocols/tests/fpga-debugging/axi-stream-s2/s2_fixed.out index e69de29b..451d2597 100644 --- a/protocols/tests/fpga-debugging/axi-stream-s2/s2_fixed.out +++ b/protocols/tests/fpga-debugging/axi-stream-s2/s2_fixed.out @@ -0,0 +1,5 @@ +Trace 0 executed successfully! + +--- + +Trace 1 executed successfully! From 673de685974e14e0c66691d801721271e5455556 Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Wed, 18 Feb 2026 16:55:36 -0500 Subject: [PATCH 09/11] Rename monitor version of s2_buggy.prot to be same as interp version --- .../axi-stream-s2/s2_buggy.prot | 80 +++++++++---------- 1 file changed, 40 insertions(+), 40 deletions(-) diff --git a/monitor/tests/fpga-debugging/axi-stream-s2/s2_buggy.prot b/monitor/tests/fpga-debugging/axi-stream-s2/s2_buggy.prot index 0f0c81d8..730b553a 100644 --- a/monitor/tests/fpga-debugging/axi-stream-s2/s2_buggy.prot +++ b/monitor/tests/fpga-debugging/axi-stream-s2/s2_buggy.prot @@ -1,94 +1,94 @@ -// ARGS: --wave fpga-debugging/axi-stream-s2/s2_buggy.fst --instances TOP.testbench.UUT.axi_stream_check:AXISManager --sample-posedge TOP.testbench.UUT.axi_stream_check.i_aclk --show-waveform-time --time-unit ns +// ARGS: --wave fpga-debugging/axi-stream-s2/s2_buggy.fst --instances TOP.testbench.UUT:AXISManager --sample-posedge TOP.testbench.UUT.M_AXIS_ACLK --show-waveform-time --time-unit ns // Source (manager) that outputs a sequence of 8 words struct AXISManager { // Control signals - in i_aresetn: u1, // Active-low reset + in M_AXIS_ARESETN: u1, // Active-low reset // AXI-Stream manager outputs (from DUT perspective) - out i_tvalid: u1, // manager has valid data - out i_tdata: u32, // Data payload - out i_tstrb: u4, // Byte strobe (always 0xF) - out i_tlast: u1, // Last word in packet + out M_AXIS_TVALID: u1, // manager has valid data + out M_AXIS_TDATA: u32, // Data payload + out M_AXIS_TSTRB: u4, // Byte strobe (always 0xF) + out M_AXIS_TLAST: u1, // Last word in packet // AXI-Stream sub-ordinate input - in i_tready: u1, // Downstream ready to accept + in M_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.i_aresetn := 1'b0; // Assert reset (active-low) - DUT.i_tready := 1'b0; + DUT.M_AXIS_ARESETN := 1'b0; // Assert reset (active-low) + DUT.M_AXIS_TREADY := 1'b0; step(); } // RECV: Receive one data word from the AXI-Stream manager -// Data transfer occurs when i_tvalid and i_tready are both 1 -// Only matches when data is immediately available (i_tvalid = 1) +// Data transfer occurs when M_AXIS_TVALID and M_AXIS_TREADY are both 1 +// Only matches when data is immediately available (M_AXIS_TVALID = 1) // // Output Arguments: // data - Expected payload from manager prot recv( out data: u32, ) { - DUT.i_aresetn := 1'b1; // Keep out of reset - DUT.i_tready := 1'b1; // Signal ready to receive + DUT.M_AXIS_ARESETN := 1'b1; // Keep out of reset + DUT.M_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.i_tvalid, 1'b1); + assert_eq(DUT.M_AXIS_TVALID, 1'b1); // Verify output data - assert_eq(DUT.i_tdata, data); + assert_eq(DUT.M_AXIS_TDATA, data); // One cycle for the transfer to complete step(); } -// RECV_LAST: Receive the last data word (with i_tlast asserted) -// This verifies both the data and that i_tlast is properly set -// Only matches when data is immediately available (i_tvalid = 1) +// RECV_LAST: Receive the last data word (with M_AXIS_TLAST asserted) +// This verifies both the data and that M_AXIS_TLAST is properly set +// Only matches when data is immediately available (M_AXIS_TVALID = 1) // // Output Arguments: // data - Expected payload from manager (should be the last word) prot recv_last( out data: u32, ) { - DUT.i_aresetn := 1'b1; // Keep out of reset - DUT.i_tready := 1'b1; // Signal ready to receive + DUT.M_AXIS_ARESETN := 1'b1; // Keep out of reset + DUT.M_AXIS_TREADY := 1'b1; // Signal ready to receive // Only matches when data is available - assert_eq(DUT.i_tvalid, 1'b1); + assert_eq(DUT.M_AXIS_TVALID, 1'b1); - // Verify output data and i_tlast - assert_eq(DUT.i_tdata, data); - assert_eq(DUT.i_tlast, 1'b1); + // Verify output data and M_AXIS_TLAST + assert_eq(DUT.M_AXIS_TDATA, data); + assert_eq(DUT.M_AXIS_TLAST, 1'b1); // One cycle for the transfer to complete step(); } -// STALL: Assert backpressure (i_tready=0) while manager has valid data +// STALL: Assert backpressure (M_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 i_tvalid=1 (i.e. there is some valid data and it's available to stall) +// Only matches when the waveform contains M_AXIS_TVALID=1 (i.e. there is some valid data and it's available to stall) prot stall(out data: u32, out last: u1) { - DUT.i_aresetn := 1'b1; // Keep out of reset - DUT.i_tready := 1'b0; // Apply backpressure + DUT.M_AXIS_ARESETN := 1'b1; // Keep out of reset + DUT.M_AXIS_TREADY := 1'b0; // Apply backpressure // Stall only applies when manager has valid data - // If i_tvalid=0, this fails and we instead have an `idle` transaction - assert_eq(DUT.i_tvalid, 1'b1); + // If M_AXIS_TVALID=0, this fails and we instead have an `idle` transaction + assert_eq(DUT.M_AXIS_TVALID, 1'b1); // Capture output values before the stall cycle - assert_eq(DUT.i_tdata, data); - assert_eq(DUT.i_tlast, last); + assert_eq(DUT.M_AXIS_TDATA, data); + assert_eq(DUT.M_AXIS_TLAST, last); step(); // Verify outputs remained stable during the stall - assert_eq(DUT.i_tdata, data); - assert_eq(DUT.i_tlast, last); + assert_eq(DUT.M_AXIS_TDATA, data); + assert_eq(DUT.M_AXIS_TLAST, last); step(); } @@ -96,18 +96,18 @@ prot stall(out data: u32, out last: u1) { // 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.i_aresetn := 1'b1; // Keep out of reset - DUT.i_tready := 1'b1; + DUT.M_AXIS_ARESETN := 1'b1; // Keep out of reset + DUT.M_AXIS_TREADY := 1'b1; // Only matches when no data is available - assert_eq(DUT.i_tvalid, 1'b0); + assert_eq(DUT.M_AXIS_TVALID, 1'b0); step(); } -// IDLE: No transaction - i_tready is deasserted +// IDLE: No transaction - M_AXIS_TREADY is deasserted #[idle] prot idle() { - DUT.i_aresetn := 1'b1; // Keep out of reset - DUT.i_tready := 1'b0; + DUT.M_AXIS_ARESETN := 1'b1; // Keep out of reset + DUT.M_AXIS_TREADY := 1'b0; step(); } From 2901ae1423a920611141057989a1a1ec61ee3cb0 Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Wed, 18 Feb 2026 16:56:33 -0500 Subject: [PATCH 10/11] Rename monitor version of s2_fixed.prot to be same as interp version --- .../axi-stream-s2/s2_fixed.prot | 82 +++++++++---------- 1 file changed, 40 insertions(+), 42 deletions(-) diff --git a/monitor/tests/fpga-debugging/axi-stream-s2/s2_fixed.prot b/monitor/tests/fpga-debugging/axi-stream-s2/s2_fixed.prot index 50a2b1d2..51d564c0 100644 --- a/monitor/tests/fpga-debugging/axi-stream-s2/s2_fixed.prot +++ b/monitor/tests/fpga-debugging/axi-stream-s2/s2_fixed.prot @@ -1,95 +1,94 @@ -// ARGS: --wave fpga-debugging/axi-stream-s2/s2_fixed.fst --instances TOP.testbench.UUT.axi_stream_check:AXISManager --sample-posedge TOP.testbench.UUT.axi_stream_check.i_aclk --show-waveform-time --time-unit ns - +// ARGS: --wave 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 // Source (manager) that outputs a sequence of 8 words struct AXISManager { // Control signals - in i_aresetn: u1, // Active-low reset + in M_AXIS_ARESETN: u1, // Active-low reset // AXI-Stream manager outputs (from DUT perspective) - out i_tvalid: u1, // manager has valid data - out i_tdata: u32, // Data payload - out i_tstrb: u4, // Byte strobe (always 0xF) - out i_tlast: u1, // Last word in packet + out M_AXIS_TVALID: u1, // manager has valid data + out M_AXIS_TDATA: u32, // Data payload + out M_AXIS_TSTRB: u4, // Byte strobe (always 0xF) + out M_AXIS_TLAST: u1, // Last word in packet // AXI-Stream sub-ordinate input - in i_tready: u1, // Downstream ready to accept + in M_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.i_aresetn := 1'b0; // Assert reset (active-low) - DUT.i_tready := 1'b0; + DUT.M_AXIS_ARESETN := 1'b0; // Assert reset (active-low) + DUT.M_AXIS_TREADY := 1'b0; step(); } // RECV: Receive one data word from the AXI-Stream manager -// Data transfer occurs when i_tvalid and i_tready are both 1 -// Only matches when data is immediately available (i_tvalid = 1) +// Data transfer occurs when M_AXIS_TVALID and M_AXIS_TREADY are both 1 +// Only matches when data is immediately available (M_AXIS_TVALID = 1) // // Output Arguments: // data - Expected payload from manager prot recv( out data: u32, ) { - DUT.i_aresetn := 1'b1; // Keep out of reset - DUT.i_tready := 1'b1; // Signal ready to receive + DUT.M_AXIS_ARESETN := 1'b1; // Keep out of reset + DUT.M_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.i_tvalid, 1'b1); + assert_eq(DUT.M_AXIS_TVALID, 1'b1); // Verify output data - assert_eq(DUT.i_tdata, data); + assert_eq(DUT.M_AXIS_TDATA, data); // One cycle for the transfer to complete step(); } -// RECV_LAST: Receive the last data word (with i_tlast asserted) -// This verifies both the data and that i_tlast is properly set -// Only matches when data is immediately available (i_tvalid = 1) +// RECV_LAST: Receive the last data word (with M_AXIS_TLAST asserted) +// This verifies both the data and that M_AXIS_TLAST is properly set +// Only matches when data is immediately available (M_AXIS_TVALID = 1) // // Output Arguments: // data - Expected payload from manager (should be the last word) prot recv_last( out data: u32, ) { - DUT.i_aresetn := 1'b1; // Keep out of reset - DUT.i_tready := 1'b1; // Signal ready to receive + DUT.M_AXIS_ARESETN := 1'b1; // Keep out of reset + DUT.M_AXIS_TREADY := 1'b1; // Signal ready to receive // Only matches when data is available - assert_eq(DUT.i_tvalid, 1'b1); + assert_eq(DUT.M_AXIS_TVALID, 1'b1); - // Verify output data and i_tlast - assert_eq(DUT.i_tdata, data); - assert_eq(DUT.i_tlast, 1'b1); + // Verify output data and M_AXIS_TLAST + assert_eq(DUT.M_AXIS_TDATA, data); + assert_eq(DUT.M_AXIS_TLAST, 1'b1); // One cycle for the transfer to complete step(); } -// STALL: Assert backpressure (i_tready=0) while manager has valid data +// STALL: Assert backpressure (M_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 i_tvalid=1 (i.e. there is some valid data and it's available to stall) +// Only matches when the waveform contains M_AXIS_TVALID=1 (i.e. there is some valid data and it's available to stall) prot stall(out data: u32, out last: u1) { - DUT.i_aresetn := 1'b1; // Keep out of reset - DUT.i_tready := 1'b0; // Apply backpressure + DUT.M_AXIS_ARESETN := 1'b1; // Keep out of reset + DUT.M_AXIS_TREADY := 1'b0; // Apply backpressure // Stall only applies when manager has valid data - // If i_tvalid=0, this fails and we instead have an `idle` transaction - assert_eq(DUT.i_tvalid, 1'b1); + // If M_AXIS_TVALID=0, this fails and we instead have an `idle` transaction + assert_eq(DUT.M_AXIS_TVALID, 1'b1); // Capture output values before the stall cycle - assert_eq(DUT.i_tdata, data); - assert_eq(DUT.i_tlast, last); + assert_eq(DUT.M_AXIS_TDATA, data); + assert_eq(DUT.M_AXIS_TLAST, last); step(); // Verify outputs remained stable during the stall - assert_eq(DUT.i_tdata, data); - assert_eq(DUT.i_tlast, last); + assert_eq(DUT.M_AXIS_TDATA, data); + assert_eq(DUT.M_AXIS_TLAST, last); step(); } @@ -97,19 +96,18 @@ prot stall(out data: u32, out last: u1) { // 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.i_aresetn := 1'b1; // Keep out of reset - DUT.i_tready := 1'b1; + DUT.M_AXIS_ARESETN := 1'b1; // Keep out of reset + DUT.M_AXIS_TREADY := 1'b1; // Only matches when no data is available - assert_eq(DUT.i_tvalid, 1'b0); - + assert_eq(DUT.M_AXIS_TVALID, 1'b0); step(); } -// IDLE: No transaction - i_tready is deasserted +// IDLE: No transaction - M_AXIS_TREADY is deasserted #[idle] prot idle() { - DUT.i_aresetn := 1'b1; // Keep out of reset - DUT.i_tready := 1'b0; + DUT.M_AXIS_ARESETN := 1'b1; // Keep out of reset + DUT.M_AXIS_TREADY := 1'b0; step(); } From fc7526e881e4785c202ece38f348bb7bcf2569a2 Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Wed, 18 Feb 2026 16:58:48 -0500 Subject: [PATCH 11/11] remove extraneous Turnt comment from interp files --- protocols/tests/fpga-debugging/axi-stream-s2/s2_buggy.prot | 2 -- protocols/tests/fpga-debugging/axi-stream-s2/s2_fixed.prot | 3 --- 2 files changed, 5 deletions(-) diff --git a/protocols/tests/fpga-debugging/axi-stream-s2/s2_buggy.prot b/protocols/tests/fpga-debugging/axi-stream-s2/s2_buggy.prot index 5f13da22..c4582f60 100644 --- a/protocols/tests/fpga-debugging/axi-stream-s2/s2_buggy.prot +++ b/protocols/tests/fpga-debugging/axi-stream-s2/s2_buggy.prot @@ -1,5 +1,3 @@ -// ARGS: --wave fpga-debugging/axi-stream-s2/s2_buggy.fst --instances TOP.testbench.UUT.axi_stream_check:AXISManager --sample-posedge TOP.testbench.UUT.axi_stream_check.i_aclk --show-waveform-time --time-unit ns - // Source (manager) that outputs a sequence of 8 words struct AXISManager { // Control signals diff --git a/protocols/tests/fpga-debugging/axi-stream-s2/s2_fixed.prot b/protocols/tests/fpga-debugging/axi-stream-s2/s2_fixed.prot index 46411502..7cbd0935 100644 --- a/protocols/tests/fpga-debugging/axi-stream-s2/s2_fixed.prot +++ b/protocols/tests/fpga-debugging/axi-stream-s2/s2_fixed.prot @@ -1,6 +1,3 @@ -// ARGS: --wave fpga-debugging/axi-stream-s2/s2_fixed.fst --instances TOP.testbench.UUT.axi_stream_check:AXISManager --sample-posedge TOP.testbench.UUT.axi_stream_check.i_aclk --show-waveform-time --time-unit ns - - // Source (manager) that outputs a sequence of 8 words struct AXISManager { // Control signals