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 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..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,111 +1,113 @@ -// 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(); } // 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/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..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,113 +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 - +// 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(); } // 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/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.out b/protocols/tests/fpga-debugging/axi-stream-s2/s2_buggy.out new file mode 100644 index 00000000..a39f87b6 --- /dev/null +++ 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.prot b/protocols/tests/fpga-debugging/axi-stream-s2/s2_buggy.prot new file mode 100644 index 00000000..c4582f60 --- /dev/null +++ b/protocols/tests/fpga-debugging/axi-stream-s2/s2_buggy.prot @@ -0,0 +1,111 @@ +// Source (manager) that outputs a sequence of 8 words +struct AXISManager { + // Control signals + in M_AXIS_ARESETN: u1, // Active-low reset + + // AXI-Stream manager outputs (from DUT perspective) + 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 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.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 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.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.M_AXIS_TVALID, 1'b1); + + // Verify output data + assert_eq(DUT.M_AXIS_TDATA, data); + + // One cycle for the transfer to complete + step(); +} + +// 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.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.M_AXIS_TVALID, 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 (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 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.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 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.M_AXIS_TDATA, data); + assert_eq(DUT.M_AXIS_TLAST, last); + + step(); + + // Verify outputs remained stable during the stall + 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.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.M_AXIS_TVALID, 1'b0); + step(); +} + +// IDLE: No transaction - M_AXIS_TREADY is deasserted +#[idle] +prot idle() { + 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 new file mode 100644 index 00000000..438631d5 --- /dev/null +++ b/protocols/tests/fpga-debugging/axi-stream-s2/s2_buggy.tx @@ -0,0 +1,95 @@ +// 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 { + 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] + 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 -> 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] + 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] + idle(); // [time: 1012.5ns -> 1037.5ns] + idle(); // [time: 1037.5ns -> 1050ns] +} 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..451d2597 --- /dev/null +++ b/protocols/tests/fpga-debugging/axi-stream-s2/s2_fixed.out @@ -0,0 +1,5 @@ +Trace 0 executed successfully! + +--- + +Trace 1 executed successfully! 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..7cbd0935 --- /dev/null +++ b/protocols/tests/fpga-debugging/axi-stream-s2/s2_fixed.prot @@ -0,0 +1,112 @@ +// Source (manager) that outputs a sequence of 8 words +struct AXISManager { + // Control signals + in M_AXIS_ARESETN: u1, // Active-low reset + + // AXI-Stream manager outputs (from DUT perspective) + 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 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.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 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.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.M_AXIS_TVALID, 1'b1); + + // Verify output data + assert_eq(DUT.M_AXIS_TDATA, data); + + // One cycle for the transfer to complete + step(); +} + +// 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.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.M_AXIS_TVALID, 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 (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 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.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 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.M_AXIS_TDATA, data); + assert_eq(DUT.M_AXIS_TLAST, last); + + step(); + + // Verify outputs remained stable during the stall + 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.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.M_AXIS_TVALID, 1'b0); + + step(); +} + +// IDLE: No transaction - M_AXIS_TREADY is deasserted +#[idle] +prot idle() { + 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 new file mode 100644 index 00000000..f4f06b4b --- /dev/null +++ b/protocols/tests/fpga-debugging/axi-stream-s2/s2_fixed.tx @@ -0,0 +1,98 @@ +// 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] + 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 -> 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] + 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] + idle(); // [time: 1012.5ns -> 1037.5ns] + idle(); // [time: 1037.5ns -> 1062.5ns] + reset(); // [time: 1062.5ns -> 1087.5ns] + reset(); // [time: 1087.5ns -> 1100ns] +} 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