URL
https://opencores.org/ocsvn/wb2axip/wb2axip/trunk
Subversion Repositories wb2axip
[/] [wb2axip/] [trunk/] [bench/] [formal/] [faxi_slave.v] - Rev 16
Compare with Previous | Blame | View Log
//////////////////////////////////////////////////////////////////////////////// // // Filename: faxi_slave.v (Formal properties of an AXI slave) // // Project: Pipelined Wishbone to AXI converter // // Purpose: This file contains a set of formal properties which can be // used to formally verify that a core truly follows the full // AXI4 specification. // // Creator: Dan Gisselquist, Ph.D. // Gisselquist Technology, LLC // //////////////////////////////////////////////////////////////////////////////// // // Copyright (C) 2017-2019, Gisselquist Technology, LLC // // This file is part of the pipelined Wishbone to AXI converter project, a // project that contains multiple bus bridging designs and formal bus property // sets. // // The bus bridge designs and property sets are free RTL designs: you can // redistribute them and/or modify any of them under the terms of the GNU // Lesser General Public License as published by the Free Software Foundation, // either version 3 of the License, or (at your option) any later version. // // The bus bridge designs and property sets are distributed in the hope that // they will be useful, but WITHOUT ANY WARRANTY; without even the implied // warranty of MERCHANTIBILITY or FITNESS FOR A PARTICULAR PURPOSE. See the // GNU Lesser General Public License for more details. // // You should have received a copy of the GNU Lesser General Public License // along with these designs. (It's in the $(ROOT)/doc directory. Run make // with no target there if the PDF file isn't present.) If not, see // <http://www.gnu.org/licenses/> for a copy. // // License: LGPL, v3, as defined and found on www.gnu.org, // http://www.gnu.org/licenses/lgpl.html // //////////////////////////////////////////////////////////////////////////////// // // `default_nettype none // module faxi_slave #( parameter C_AXI_ID_WIDTH = 3, // The AXI id width used for R&W // This is an int between 1-16 parameter C_AXI_DATA_WIDTH = 128,// Width of the AXI R&W data parameter C_AXI_ADDR_WIDTH = 28, // AXI Address width (log wordsize) localparam DW = C_AXI_DATA_WIDTH, localparam AW = C_AXI_ADDR_WIDTH, parameter [0:0] F_OPT_BURSTS = 1'b1, // Check burst lengths parameter [7:0] F_AXI_MAXBURST = 8'hff,// Maximum burst length, minus 1 parameter F_LGDEPTH = 10, parameter F_LGFIFO = 3, parameter [(C_AXI_ID_WIDTH-1):0] F_AXI_MAXSTALL = 3, parameter [(C_AXI_ID_WIDTH-1):0] F_AXI_MAXDELAY = 3 ) ( input wire i_clk, // System clock input wire i_axi_reset_n, // AXI write address channel signals input wire i_axi_awready,//Slave is ready to accept // input wire [C_AXI_ID_WIDTH-1:0] i_axi_awid, // Write ID input wire [AW-1:0] i_axi_awaddr, // Write address input wire [7:0] i_axi_awlen, // Write Burst Length input wire [2:0] i_axi_awsize, // Write Burst size input wire [1:0] i_axi_awburst, // Write Burst type input wire [0:0] i_axi_awlock, // Write lock type input wire [3:0] i_axi_awcache, // Write Cache type input wire [2:0] i_axi_awprot, // Write Protection type input wire [3:0] i_axi_awqos, // Write Quality of Svc input wire i_axi_awvalid, // Write address valid // AXI write data channel signals input wire i_axi_wready, // Write data ready input wire [DW-1:0] i_axi_wdata, // Write data input wire [DW/8-1:0] i_axi_wstrb, // Write strobes input wire i_axi_wlast, // Last write transaction input wire i_axi_wvalid, // Write valid // AXI write response channel signals // input wire [C_AXI_ID_WIDTH-1:0] i_axi_bid, // Response ID input wire [1:0] i_axi_bresp, // Write response input wire i_axi_bvalid, // Write reponse valid input wire i_axi_bready, // Response ready // AXI read address channel signals input wire i_axi_arready, // Read address ready // input wire [C_AXI_ID_WIDTH-1:0] i_axi_arid, // Read ID input wire [AW-1:0] i_axi_araddr, // Read address input wire [7:0] i_axi_arlen, // Read Burst Length input wire [2:0] i_axi_arsize, // Read Burst size input wire [1:0] i_axi_arburst, // Read Burst type input wire [0:0] i_axi_arlock, // Read lock type input wire [3:0] i_axi_arcache, // Read Cache type input wire [2:0] i_axi_arprot, // Read Protection type input wire [3:0] i_axi_arqos, // Read Protection type input wire i_axi_arvalid, // Read address valid // AXI read data channel signals // input wire [C_AXI_ID_WIDTH-1:0] i_axi_rid, // Response ID input wire [1:0] i_axi_rresp, // Read response input wire i_axi_rvalid, // Read reponse valid input wire [DW-1:0] i_axi_rdata, // Read data input wire i_axi_rlast, // Read last input wire i_axi_rready, // Read Response ready // output reg [F_LGDEPTH-1:0] f_axi_rd_nbursts, output reg [F_LGDEPTH-1:0] f_axi_rd_outstanding, output reg [F_LGDEPTH-1:0] f_axi_wr_nbursts, output reg [F_LGDEPTH-1:0] f_axi_awr_outstanding, output reg [F_LGDEPTH-1:0] f_axi_awr_nbursts, // Address writes without write valids // // output reg [(9-1):0] f_axi_wr_pending, // // RD_COUNT: increment on read w/o last, cleared on read w/ last output reg [(9-1):0] f_axi_rd_count, output reg [(72-1):0] f_axi_rdfifo ); reg [(9-1):0] f_axi_wr_count; //***************************************************************************** // Parameter declarations //***************************************************************************** localparam LG_AXI_DW = ( C_AXI_DATA_WIDTH == 8) ? 3 : ((C_AXI_DATA_WIDTH == 16) ? 4 : ((C_AXI_DATA_WIDTH == 32) ? 5 : ((C_AXI_DATA_WIDTH == 64) ? 6 : ((C_AXI_DATA_WIDTH == 128) ? 7 : 8)))); localparam LG_WB_DW = ( DW == 8) ? 3 : ((DW == 16) ? 4 : ((DW == 32) ? 5 : ((DW == 64) ? 6 : ((DW == 128) ? 7 : 8)))); localparam LGFIFOLN = C_AXI_ID_WIDTH; localparam FIFOLN = (1<<LGFIFOLN); localparam F_AXI_MAXWAIT = F_AXI_MAXSTALL; //***************************************************************************** // Internal register and wire declarations //***************************************************************************** // wire w_fifo_full; wire axi_rd_ack, axi_wr_ack, axi_ard_req, axi_awr_req, axi_wr_req, axi_rd_err, axi_wr_err; // assign axi_ard_req = (i_axi_arvalid)&&(i_axi_arready); assign axi_awr_req = (i_axi_awvalid)&&(i_axi_awready); assign axi_wr_req = (i_axi_wvalid )&&(i_axi_wready); // assign axi_rd_ack = (i_axi_rvalid)&&(i_axi_rready); assign axi_wr_ack = (i_axi_bvalid)&&(i_axi_bready); assign axi_rd_err = (axi_rd_ack)&&(i_axi_rresp[1]); assign axi_wr_err = (axi_wr_ack)&&(i_axi_bresp[1]); `define SLAVE_ASSUME assume `define SLAVE_ASSERT assert // // Setup // reg f_past_valid; integer k; initial f_past_valid = 1'b0; always @(posedge i_clk) f_past_valid <= 1'b1; always @(*) if (!f_past_valid) assume(!i_axi_reset_n); // WAS AN ASSERT //////////////////////////////////////////////////////////////////////// // // // Reset properties // // //////////////////////////////////////////////////////////////////////// localparam [0:0] F_OPT_ASSUME_RESET = 1'b1; generate if (F_OPT_ASSUME_RESET) begin : ASSUME_INITIAL_RESET always @(*) if (!f_past_valid) assume(!i_axi_reset_n); end else begin : ASSERT_INITIAL_RESET always @(*) if (!f_past_valid) assert(!i_axi_reset_n); end endgenerate // // If asserted, the reset must be asserted for a minimum of 16 clocks reg [3:0] f_reset_length; initial f_reset_length = 0; always @(posedge i_clk) if (i_axi_reset_n) f_reset_length <= 0; else if (!(&f_reset_length)) f_reset_length <= f_reset_length + 1'b1; always @(posedge i_clk) if ((f_past_valid)&&(!$past(i_axi_reset_n))&&(!$past(&f_reset_length))) `SLAVE_ASSUME(!i_axi_reset_n); generate if (F_OPT_ASSUME_RESET) begin : ASSUME_RESET always @(posedge i_clk) if ((f_past_valid)&&(!$past(i_axi_reset_n))&&(!$past(&f_reset_length))) assume(!i_axi_reset_n); always @(*) if ((f_reset_length > 0)&&(f_reset_length < 4'hf)) assume(!i_axi_reset_n); end else begin : ASSERT_RESET always @(posedge i_clk) if ((f_past_valid)&&(!$past(i_axi_reset_n))&&(!$past(&f_reset_length))) assert(!i_axi_reset_n); always @(*) if ((f_reset_length > 0)&&(f_reset_length < 4'hf)) assert(!i_axi_reset_n); end endgenerate always @(posedge i_clk) if ((!f_past_valid)||(!$past(i_axi_reset_n))) begin `SLAVE_ASSUME(!i_axi_arvalid); `SLAVE_ASSUME(!i_axi_awvalid); `SLAVE_ASSUME(!i_axi_wvalid); // `SLAVE_ASSERT(!i_axi_bvalid); `SLAVE_ASSERT(!i_axi_rvalid); end //////////////////////////////////////////////////////////////////////// // // // Stability properties--what happens if valid and not ready // // //////////////////////////////////////////////////////////////////////// // Assume any response from the bus will not change prior to that // response being accepted always @(posedge i_clk) if ((f_past_valid)&&($past(i_axi_reset_n))) begin // Write address channel if ((f_past_valid)&&($past(i_axi_awvalid))&&(!$past(i_axi_awready))) begin `SLAVE_ASSUME(i_axi_awvalid); `SLAVE_ASSUME(i_axi_awaddr == $past(i_axi_awaddr)); // `SLAVE_ASSUME($stable(i_axi_awid)); `SLAVE_ASSUME($stable(i_axi_awlen)); `SLAVE_ASSUME($stable(i_axi_awsize)); `SLAVE_ASSUME($stable(i_axi_awburst)); `SLAVE_ASSUME($stable(i_axi_awlock)); `SLAVE_ASSUME($stable(i_axi_awcache)); `SLAVE_ASSUME($stable(i_axi_awprot)); `SLAVE_ASSUME($stable(i_axi_awqos)); end // Write data channel if ((f_past_valid)&&($past(i_axi_wvalid))&&(!$past(i_axi_wready))) begin `SLAVE_ASSUME(i_axi_wvalid); `SLAVE_ASSUME($stable(i_axi_wstrb)); `SLAVE_ASSUME($stable(i_axi_wdata)); `SLAVE_ASSUME($stable(i_axi_wlast)); end // Incoming Read address channel if ((f_past_valid)&&($past(i_axi_arvalid))&&(!$past(i_axi_arready))) begin `SLAVE_ASSUME(i_axi_arvalid); // `SLAVE_ASSUME($stable(i_axi_arid)); `SLAVE_ASSUME($stable(i_axi_araddr)); `SLAVE_ASSUME($stable(i_axi_arlen)); `SLAVE_ASSUME($stable(i_axi_arsize)); `SLAVE_ASSUME($stable(i_axi_arburst)); `SLAVE_ASSUME($stable(i_axi_arlock)); `SLAVE_ASSUME($stable(i_axi_arcache)); `SLAVE_ASSUME($stable(i_axi_arprot)); `SLAVE_ASSUME($stable(i_axi_arqos)); end // Assume any response from the bus will not change prior to that // response being accepted if ((f_past_valid)&&($past(i_axi_rvalid))&&(!$past(i_axi_rready))) begin `SLAVE_ASSERT(i_axi_rvalid); // `SLAVE_ASSERT($stable(i_axi_rid)); `SLAVE_ASSERT($stable(i_axi_rresp)); `SLAVE_ASSERT($stable(i_axi_rdata)); `SLAVE_ASSERT($stable(i_axi_rlast)); end if ((f_past_valid)&&($past(i_axi_bvalid))&&(!$past(i_axi_bready))) begin `SLAVE_ASSERT(i_axi_bvalid); /// `SLAVE_ASSERT($stable(i_axi_bid)); `SLAVE_ASSERT($stable(i_axi_bresp)); end end // Nothing should be returned or requested on the first clock initial `SLAVE_ASSUME(!i_axi_arvalid); initial `SLAVE_ASSUME(!i_axi_awvalid); initial `SLAVE_ASSUME(!i_axi_wvalid); // initial `SLAVE_ASSERT(!i_axi_bvalid); initial `SLAVE_ASSERT(!i_axi_rvalid); //////////////////////////////////////////////////////////////////////// // // // Insist upon a maximum delay before a request is accepted // // //////////////////////////////////////////////////////////////////////// generate if (F_AXI_MAXWAIT > 0) begin : CHECK_STALL_COUNT // // AXI write address channel // // reg [(F_LGDEPTH-1):0] f_axi_awstall, f_axi_wstall, f_axi_arstall, f_axi_bstall, f_axi_rstall; initial f_axi_awstall = 0; always @(posedge i_clk) if ((!i_axi_reset_n)||(!i_axi_awvalid)||(i_axi_awready)) f_axi_awstall <= 0; else if ((!i_axi_bvalid)||(i_axi_bready)) f_axi_awstall <= f_axi_awstall + 1'b1; always @(*) `SLAVE_ASSERT(f_axi_awstall < F_AXI_MAXWAIT); // // AXI write data channel // // // AXI explicitly allows write bursts with zero strobes. This is part // of how a transaction is aborted (if at all). initial f_axi_wstall = 0; always @(posedge i_clk) if ((!i_axi_reset_n)||(!i_axi_wvalid)||(i_axi_wready)) f_axi_wstall <= 0; else if ((!i_axi_bvalid)||(i_axi_bready)) f_axi_wstall <= f_axi_wstall + 1'b1; always @(*) `SLAVE_ASSERT(f_axi_wstall < F_AXI_MAXWAIT); // // AXI read address channel // // initial f_axi_arstall = 0; always @(posedge i_clk) if ((!i_axi_reset_n)||(!i_axi_arvalid)||(i_axi_arready)) f_axi_arstall <= 0; else if ((!i_axi_rvalid)||(i_axi_rready)) f_axi_arstall <= f_axi_arstall + 1'b1; always @(*) `SLAVE_ASSERT(f_axi_arstall < F_AXI_MAXWAIT); // AXI write response channel initial f_axi_bstall = 0; always @(posedge i_clk) if ((!i_axi_reset_n)||(!i_axi_bvalid)||(i_axi_bready)) f_axi_bstall <= 0; else f_axi_bstall <= f_axi_bstall + 1'b1; always @(*) `SLAVE_ASSUME(f_axi_bstall < F_AXI_MAXWAIT); // AXI read response channel initial f_axi_rstall = 0; always @(posedge i_clk) if ((!i_axi_reset_n)||(!i_axi_rvalid)||(i_axi_rready)) f_axi_rstall <= 0; else f_axi_rstall <= f_axi_rstall + 1'b1; always @(*) `SLAVE_ASSUME(f_axi_rstall < F_AXI_MAXWAIT); end endgenerate //////////////////////////////////////////////////////////////////////// // // // Count outstanding transactions. With these measures, we count // once per any burst. // // //////////////////////////////////////////////////////////////////////// initial f_axi_awr_outstanding = 0; always @(posedge i_clk) if (!i_axi_reset_n) f_axi_awr_outstanding <= 0; else case({ (axi_awr_req), (axi_wr_req) }) 2'b10: f_axi_awr_outstanding <= f_axi_awr_outstanding + i_axi_awlen-1; 2'b01: f_axi_awr_outstanding <= f_axi_awr_outstanding - 1'b1; 2'b11: f_axi_awr_outstanding <= f_axi_awr_outstanding + i_axi_awlen; // +1 -1 default: begin end endcase initial f_axi_awr_nbursts = 0; always @(posedge i_clk) if (!i_axi_reset_n) f_axi_awr_nbursts <= 0; else case({ (axi_awr_req), (axi_wr_ack) }) 2'b10: f_axi_awr_nbursts <= f_axi_awr_nbursts + 1'b1; 2'b01: f_axi_awr_nbursts <= f_axi_awr_nbursts - 1'b1; default: begin end endcase initial f_axi_wr_nbursts = 0; always @(posedge i_clk) if (!i_axi_reset_n) f_axi_wr_nbursts <= 0; else case({ (axi_wr_req)&&(i_axi_wlast), (axi_wr_ack) }) 2'b01: f_axi_wr_nbursts <= f_axi_wr_nbursts - 1'b1; 2'b10: f_axi_wr_nbursts <= f_axi_wr_nbursts + 1'b1; default: begin end endcase initial f_axi_rd_nbursts = 0; always @(posedge i_clk) if (!i_axi_reset_n) f_axi_rd_nbursts <= 0; else case({ (axi_ard_req), (axi_rd_ack)&&(i_axi_rlast) }) 2'b01: f_axi_rd_nbursts <= f_axi_rd_nbursts - 1'b1; 2'b10: f_axi_rd_nbursts <= f_axi_rd_nbursts + 1'b1; endcase initial f_axi_rd_outstanding = 0; always @(posedge i_clk) if (!i_axi_reset_n) f_axi_rd_outstanding <= 0; else case({ (axi_ard_req), (axi_rd_ack) }) 2'b01: f_axi_rd_outstanding <= f_axi_rd_outstanding - 1'b1; 2'b10: f_axi_rd_outstanding <= f_axi_rd_outstanding + i_axi_arlen+1; 2'b11: f_axi_rd_outstanding <= f_axi_rd_outstanding + i_axi_arlen; endcase // Do not let the number of outstanding requests overflow always @(posedge i_clk) `SLAVE_ASSERT(f_axi_awr_outstanding < {(F_LGDEPTH){1'b1}}); always @(posedge i_clk) `SLAVE_ASSERT(f_axi_rd_outstanding < {(F_LGDEPTH){1'b1}}); always @(posedge i_clk) `SLAVE_ASSERT(f_axi_awr_nbursts < {(F_LGDEPTH){1'b1}}); always @(posedge i_clk) `SLAVE_ASSERT(f_axi_wr_nbursts < {(F_LGDEPTH){1'b1}}); always @(posedge i_clk) `SLAVE_ASSERT(f_axi_rd_nbursts < {(F_LGDEPTH){1'b1}}); // Cannot have outstanding values if there aren't any outstanding // bursts always @(posedge i_clk) if (f_axi_awr_outstanding > 0) `SLAVE_ASSERT(f_axi_awr_nbursts > 0); // else if (f_axi_awr_outstanding == 0) // Doesn't apply. Might have awr_outstanding == 0 and // awr_nbursts>0 always @(posedge i_clk) if (f_axi_rd_outstanding > 0) `SLAVE_ASSERT(f_axi_rd_nbursts > 0); else `SLAVE_ASSERT(f_axi_rd_nbursts == 0); always @(posedge i_clk) `SLAVE_ASSERT(f_axi_rd_nbursts <= f_axi_rd_outstanding); //////////////////////////////////////////////////////////////////////// // // // Insist that all responses are returned in less than a maximum delay // In this case, we count responses within a burst, rather than entire // bursts. // // //////////////////////////////////////////////////////////////////////// generate if (F_AXI_MAXDELAY > 0) begin : CHECK_MAX_DELAY reg [(C_AXI_ID_WIDTH):0] f_axi_wr_ack_delay, f_axi_awr_ack_delay, f_axi_rd_ack_delay; initial f_axi_rd_ack_delay = 0; always @(posedge i_clk) if ((!i_axi_reset_n)||(i_axi_rvalid)||(f_axi_rd_outstanding==0)) f_axi_rd_ack_delay <= 0; else f_axi_rd_ack_delay <= f_axi_rd_ack_delay + 1'b1; initial f_axi_wr_ack_delay = 0; always @(posedge i_clk) if ((!i_axi_reset_n)||((i_axi_wvalid)&&(!i_axi_wlast)) ||(i_axi_bvalid)||(f_axi_awr_outstanding==0)) f_axi_wr_ack_delay <= 0; else f_axi_wr_ack_delay <= f_axi_wr_ack_delay + 1'b1; initial f_axi_awr_ack_delay = 0; always @(posedge i_clk) if ((!i_axi_reset_n)||(i_axi_bvalid)||(i_axi_wvalid) ||(f_axi_awr_nbursts == 0) ||(f_axi_wr_nbursts == 0)) f_axi_awr_ack_delay <= 0; else f_axi_awr_ack_delay <= f_axi_awr_ack_delay + 1'b1; always @(*) `SLAVE_ASSERT(f_axi_rd_ack_delay < F_AXI_MAXDELAY); always @(*) `SLAVE_ASSERT(f_axi_wr_ack_delay < F_AXI_MAXDELAY); always @(posedge i_clk) `SLAVE_ASSERT(f_axi_awr_ack_delay < F_AXI_MAXDELAY); end endgenerate //////////////////////////////////////////////////////////////////////// // // // Assume acknowledgements must follow requests // // The outstanding count is a count of bursts, but the acknowledgements // we are looking for are individual. Hence, there should be no // individual acknowledgements coming back if there's no outstanding // burst. // // //////////////////////////////////////////////////////////////////////// // // AXI write response channel // always @(posedge i_clk) if (i_axi_bvalid) begin `SLAVE_ASSERT(f_axi_awr_nbursts > 0); `SLAVE_ASSERT(f_axi_wr_nbursts > 0); end // // AXI read data channel signals // always @(posedge i_clk) if (i_axi_rvalid) begin `SLAVE_ASSERT(f_axi_rd_outstanding > 0); `SLAVE_ASSERT(f_axi_rd_nbursts > 0); if (!i_axi_rlast) `SLAVE_ASSERT(f_axi_rd_outstanding > 1); end //////////////////////////////////////////////////////////////////////// // // // //////////////////////////////////////////////////////////////////////// generate if (!F_OPT_BURSTS) begin always @(posedge i_clk) if (i_axi_awvalid) `SLAVE_ASSUME(i_axi_awlen == 0); always @(posedge i_clk) if (i_axi_wvalid) `SLAVE_ASSUME(i_axi_wlast); always @(posedge i_clk) if (i_axi_arvalid) `SLAVE_ASSUME(i_axi_arlen == 0); always @(*) `SLAVE_ASSERT(f_axi_rd_nbursts == f_axi_rd_outstanding); end endgenerate reg [7:0] wrfifo [0:((1<<F_LGDEPTH)-1)]; reg [7:0] rdfifo [0:((1<<F_LGDEPTH)-1)]; reg [F_LGDEPTH-1:0] rd_rdaddr, wr_rdaddr, rd_wraddr, wr_wraddr; reg [7:0] rdfifo_data, wrfifo_data; reg [F_LGDEPTH-1:0] rdfifo_outstanding; wire [7:0] this_wlen; wire [F_LGDEPTH-1:0] wrfifo_fill, rdfifo_fill; /* always @(posedge i_clk) if (!i_axi_reset_n) begin f_axi_wburst_fifo <= 0; end else case({ axi_awr_req , axi_wr_req, i_axi_wrlast }) 3'b010: f_axi_wburst_fifo[7:0] <= f_axi_wburst_fifo[7:0]-1; 3'b011: begin `SLAVE_ASSUME(f_axi_wburst_fifo[7:0] == 0); f_axi_wburst_fifo <= { 8'h0, f_axi_wburst_fifo[63:8] }; end 3'b100: `SLAVE_ASSUME(f_axi_awr_nbursts < 8); f_axi_wburst_fifo <= f_axi_wburst_fifo | ((i_axi_awlen)<<(f_axi_awr_nbursts * 8)); 3'b11: f_axi_wburst_fifo <= { 8'h0, f_axi_wburst_fifo[63:8] } | ((i_axi_awlen)<<((f_axi_awr_nbursts-1) * 8)); default: endcase */ // // Count the number of write elements received since the last wlast initial f_axi_wr_count = 0; always @(posedge i_clk) if (!i_axi_reset_n) f_axi_wr_count <= 0; else if (axi_wr_req) begin if (i_axi_wlast) f_axi_wr_count <= 1'b0; else f_axi_wr_count <= f_axi_wr_count + 1'b1; end // // Write information to the write FIFO initial wr_wraddr = 0; always @(posedge i_clk) if (!i_axi_reset_n) wr_wraddr <= 0; else if (axi_awr_req) wr_wraddr <= wr_wraddr + 1'b1; always @(posedge i_clk) if (axi_awr_req) wrfifo[wr_wraddr] <= { i_axi_awlen }; // // Read information from the write queue always @(*) wrfifo_data = wrfifo[wr_rdaddr]; assign this_wlen = wrfifo_data; always @(*) if ((i_axi_wvalid)&&(i_axi_wlast)&&(f_axi_awr_nbursts>0)) `SLAVE_ASSUME(i_axi_wlast == (this_wlen == f_axi_wr_count)); // Advance the read pointer for the write FIFO initial wr_rdaddr = 0; always @(posedge i_clk) if (!i_axi_reset_n) wr_rdaddr <= 0; else if ((axi_wr_req)&&(i_axi_wlast)) wr_rdaddr <= wr_rdaddr + 1'b1; assign wrfifo_fill = wr_wraddr - wr_rdaddr; //////////////////////////////////////////////////////////////////////// // // Read FIFO // parameter NRDFIFO = 8; parameter WRDFIFO = 9; initial f_axi_rd_count = 0; always @(posedge i_clk) if (!i_axi_reset_n) f_axi_rd_count <= 0; else if (axi_rd_ack) begin if (i_axi_rlast) f_axi_rd_count <= 1'b0; else f_axi_rd_count <= f_axi_rd_count + 1'b1; end always @(*) `SLAVE_ASSUME(f_axi_rd_nbursts <= NRDFIFO); /* always @(*) if (i_axi_rvalid) begin if (i_axi_rlast) `SLAVE_ASSERT(f_axi_rdfifo[WRDFIFO-1:0] == f_axi_rd_count); else `SLAVE_ASSERT(f_axi_rdfifo[WRDFIFO-1:0] < f_axi_rd_count); end always @(posedge i_clk) if (!i_axi_reset_n) f_axi_rdfifo <= 0; else casez({ axi_ard_req, axi_rd_ack, i_axi_rlast }) 3'b10?: f_axi_rdfifo[ f_axi_rd_nbursts*WRDFIFO +: WRDFIFO] <= { 1'b0, i_axi_arlen }; // 3'b010: f_axi_rdfifo[ 8:0] <= f_axi_rdfifo[8:0] - 1'b1; 3'b011: f_axi_rdfifo <= { {(WRDFIFO){1'b0}}, f_axi_rdfifo[NRDFIFO*WRDFIFO-1:WRDFIFO] }; 3'b111: begin f_axi_rdfifo <= { {(WRDFIFO){1'b0}}, f_axi_rdfifo[NRDFIFO*WRDFIFO-1:WRDFIFO] }; f_axi_rdfifo[ (f_axi_rd_nbursts-1)*WRDFIFO +: WRDFIFO] <= { 1'b0, i_axi_arlen }; end default: begin end endcase always @(*) if (f_axi_rd_nbursts < NRDFIFO) assert(f_axi_rdfifo[NRDFIFO * WRDFIFO-1: f_axi_rd_nbursts*WRDFIFO] == 0); always @(*) begin rdfifo_outstanding = 0; for(k = 0; k < NRDFIFO; k=k+1) begin if (k < f_axi_rd_nbursts) begin rdfifo_outstanding = rdfifo_outstanding + f_axi_rdfifo[k * WRDFIFO +: WRDFIFO] + 1; end assert(f_axi_rdfifo[k*WRDFIFO+(WRDFIFO-1)] == 1'b0); end end always @(posedge i_clk) assert(rdfifo_outstanding - f_axi_rd_count == f_axi_rd_outstanding); */ always @(*) f_axi_rdfifo = 0; endmodule