URL
https://opencores.org/ocsvn/wb2axip/wb2axip/trunk
Subversion Repositories wb2axip
[/] [wb2axip/] [trunk/] [bench/] [formal/] [faxi_master.v] - Rev 12
Go to most recent revision | Compare with Previous | Blame | View Log
//////////////////////////////////////////////////////////////////////////////// // // Filename: faxi_master.v (Formal properties of an AXI master) // // Project: Pipelined Wishbone to AXI converter // // Purpose: // // Creator: Dan Gisselquist, Ph.D. // Gisselquist Technology, LLC // //////////////////////////////////////////////////////////////////////////////// // // Copyright (C) 2017, Gisselquist Technology, LLC // // This program is free software (firmware): you can redistribute it and/or // modify it under the terms of the GNU General Public License as published // by the Free Software Foundation, either version 3 of the License, or (at // your option) any later version. // // This program is distributed in the hope that it will be useful, but WITHOUT // ANY WARRANTY; without even the implied warranty of MERCHANTIBILITY or // FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License // for more details. // // You should have received a copy of the GNU General Public License along // with this program. (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: GPL, v3, as defined and found on www.gnu.org, // http://www.gnu.org/licenses/gpl.html // // //////////////////////////////////////////////////////////////////////////////// // // `default_nettype none // module faxi_master #( 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 [(C_AXI_ID_WIDTH-1):0] F_AXI_MAXSTALL = 3, parameter [(C_AXI_ID_WIDTH-1):0] F_AXI_MAXDELAY = 3, parameter [0:0] F_STRICT_ORDER = 0, // Reorder, or not? 0 -> Reorder parameter [0:0] F_CONSECUTIVE_IDS= 0, // 0=ID's must be consecutive parameter [0:0] F_OPT_BURSTS = 1'b1, // Check burst lengths parameter [0:0] F_CHECK_IDS = 1'b1 // Check ID's upon issue&return ) ( input i_clk, // System clock input i_axi_reset_n, // AXI write address channel signals input 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 [(C_AXI_ID_WIDTH-1):0] f_axi_rd_outstanding, output reg [(C_AXI_ID_WIDTH-1):0] f_axi_wr_outstanding, output reg [(C_AXI_ID_WIDTH-1):0] f_axi_awr_outstanding, output reg [((1<<C_AXI_ID_WIDTH)-1):0] f_axi_rd_id_outstanding, output reg [((1<<C_AXI_ID_WIDTH)-1):0] f_axi_awr_id_outstanding, output reg [((1<<C_AXI_ID_WIDTH)-1):0] f_axi_wr_id_outstanding ); reg [((1<<C_AXI_ID_WIDTH)-1):0] f_axi_wr_id_complete; //***************************************************************************** // 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); //***************************************************************************** // Internal register and wire declarations //***************************************************************************** // Things we're not changing ... always @(*) begin assert(i_axi_awlen == 8'h0); // Burst length is one assert(i_axi_awsize == 3'b101); // maximum bytes per burst is 32 assert(i_axi_awburst == 2'b01); // Incrementing address (ignored) assert(i_axi_arburst == 2'b01); // Incrementing address (ignored) assert(i_axi_awlock == 1'b0); // Normal signaling assert(i_axi_arlock == 1'b0); // Normal signaling assert(i_axi_awcache == 4'h2); // Normal: no cache, no buffer assert(i_axi_arcache == 4'h2); // Normal: no cache, no buffer assert(i_axi_awprot == 3'b010);// Unpriviledged, unsecure, data access assert(i_axi_arprot == 3'b010);// Unpriviledged, unsecure, data access assert(i_axi_awqos == 4'h0); // Lowest quality of service (unused) assert(i_axi_arqos == 4'h0); // Lowest quality of service (unused) end // 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]); // // 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) assert(!i_axi_reset_n); // // All signals must be synchronous with the clock // always @($global_clock) if (f_past_valid) begin // Assume our inputs will only change on the positive edge // of the clock if (!$rose(i_clk)) begin // AXI inputs assume($stable(i_axi_awready)); assume($stable(i_axi_wready)); // assume($stable(i_axi_bid)); assume($stable(i_axi_bresp)); assume($stable(i_axi_bvalid)); assume($stable(i_axi_arready)); // assume($stable(i_axi_rid)); assume($stable(i_axi_rresp)); assume($stable(i_axi_rvalid)); assume($stable(i_axi_rdata)); assume($stable(i_axi_rlast)); // // AXI outputs // assert($stable(i_axi_awvalid)); assert($stable(i_axi_awid)); assert($stable(i_axi_awlen)); assert($stable(i_axi_awsize)); assert($stable(i_axi_awlock)); assert($stable(i_axi_awcache)); assert($stable(i_axi_awprot)); assert($stable(i_axi_awqos)); // assert($stable(i_axi_wvalid)); assert($stable(i_axi_wdata)); assert($stable(i_axi_wstrb)); assert($stable(i_axi_wlast)); // assert($stable(i_axi_arvalid)); assert($stable(i_axi_arid)); assert($stable(i_axi_arlen)); assert($stable(i_axi_arsize)); assert($stable(i_axi_arburst)); assert($stable(i_axi_arlock)); assert($stable(i_axi_arprot)); assert($stable(i_axi_arqos)); // assert($stable(i_axi_bready)); // assert($stable(i_axi_rready)); // // Formal outputs // assert($stable(f_axi_rd_outstanding)); assert($stable(f_axi_wr_outstanding)); assert($stable(f_axi_awr_outstanding)); end end //////////////////////////////////////////////////// // // // Reset properties // // //////////////////////////////////////////////////// always @(posedge i_clk) if ((f_past_valid)&&(!$past(i_axi_reset_n))) begin assert(!i_axi_arvalid); assert(!i_axi_awvalid); assert(!i_axi_wvalid); assume(!i_axi_bvalid); assume(!i_axi_rvalid); end //////////////////////////////////////////////////// // // // Stability assumptions, AXI inputs/responses // // //////////////////////////////////////////////////// // Assume any response from the bus will not change prior to that // response being accepted always @(posedge i_clk) if (f_past_valid) begin if ((f_past_valid)&&($past(i_axi_rvalid))&&(!$past(i_axi_rready))) begin assume(i_axi_rid == $past(i_axi_rid)); assume(i_axi_rresp == $past(i_axi_rresp)); assume(i_axi_rdata == $past(i_axi_rdata)); assume(i_axi_rlast == $past(i_axi_rlast)); end if ((f_past_valid)&&($past(i_axi_bvalid))&&(!$past(i_axi_bready))) begin assume(i_axi_bid == $past(i_axi_bid)); assume(i_axi_bresp == $past(i_axi_bresp)); end end // Nothing should be returning a result on the first clock initial assume(!i_axi_bvalid); initial assume(!i_axi_rvalid); // initial assert(!i_axi_arvalid); initial assert(!i_axi_awvalid); initial assert(!i_axi_wvalid); ////////////////////////////////////////////// // // // Stability assumptions, AXI outputs/requests // // ////////////////////////////////////////////// // Read address chanel always @(posedge i_clk) if ((f_past_valid)&&($past(i_axi_arvalid))&&(!$past(i_axi_arready))) begin assert(i_axi_arvalid); assert($stable(i_axi_arid)); assert($stable(i_axi_araddr)); assert($stable(i_axi_arlen)); assert($stable(i_axi_arsize)); assert($stable(i_axi_arburst)); assert($stable(i_axi_arlock)); assert($stable(i_axi_arcache)); assert($stable(i_axi_arprot)); assert($stable(i_axi_arqos)); assert($stable(i_axi_arvalid)); end // If valid, but not ready, on any channel is true, nothing changes // until valid && ready always @(posedge i_clk) if ((f_past_valid)&&($past(i_axi_awvalid))&&(!$past(i_axi_awready))) begin assert($stable(i_axi_awid)); assert($stable(i_axi_awaddr)); assert($stable(i_axi_awlen)); assert($stable(i_axi_awsize)); assert($stable(i_axi_awburst)); assert($stable(i_axi_awlock)); assert($stable(i_axi_awcache)); assert($stable(i_axi_awprot)); assert($stable(i_axi_awqos)); assert($stable(i_axi_awvalid)); end always @(posedge i_clk) if ((f_past_valid)&&($past(i_axi_wvalid))&&(!$past(i_axi_wready))) begin // AXI write data channel signals assert($stable(i_axi_wdata)); assert($stable(i_axi_wstrb)); assert($stable(i_axi_wlast)); assert($stable(i_axi_wvalid)); end // // /////////////////////////////////////////////////////////////////// // // // Insist upon a maximum delay before a request is accepted // // /////////////////////////////////////////////////////////////////// // // AXI write address channel // // reg [(C_AXI_ID_WIDTH):0] f_axi_awstall; 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 f_axi_awstall <= f_axi_awstall + 1'b1; always @(*) assume((F_AXI_MAXSTALL==0)||(f_axi_awstall < F_AXI_MAXSTALL)); // // AXI write data channel // // // AXI explicitly allows write bursts with zero strobes. This is part // of how a transaction is aborted (if at all). //always @(*) if (i_axi_wvalid) assert(|i_axi_wstrb); reg [(C_AXI_ID_WIDTH):0] f_axi_wstall; 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 f_axi_wstall <= f_axi_wstall + 1'b1; always @(*) assume((F_AXI_MAXSTALL==0)||(f_axi_wstall < F_AXI_MAXSTALL)); // // AXI read address channel // // reg [(C_AXI_ID_WIDTH):0] f_axi_arstall; 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 f_axi_arstall <= f_axi_arstall + 1'b1; always @(*) assume((F_AXI_MAXSTALL==0)||(f_axi_arstall < F_AXI_MAXSTALL)); //////////////////////////////////////////////////////////////////////// // // // Count outstanding transactions // // //////////////////////////////////////////////////////////////////////// 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_ack) }) 2'b10: f_axi_awr_outstanding <= f_axi_awr_outstanding + 1'b1; 2'b01: f_axi_awr_outstanding <= f_axi_awr_outstanding - 1'b1; default: begin end endcase initial f_axi_wr_outstanding = 0; always @(posedge i_clk) if (!i_axi_reset_n) f_axi_wr_outstanding <= 0; else case({ (axi_wr_req)&&(i_axi_wlast), (axi_wr_ack) }) 2'b01: f_axi_wr_outstanding <= f_axi_wr_outstanding - 1'b1; 2'b10: f_axi_wr_outstanding <= f_axi_wr_outstanding + 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)&&(i_axi_rlast) }) 2'b01: f_axi_rd_outstanding <= f_axi_rd_outstanding - 1'b1; 2'b10: f_axi_rd_outstanding <= f_axi_rd_outstanding + 1'b1; endcase // Do not let the number of outstanding requests overflow always @(posedge i_clk) assert(f_axi_wr_outstanding < {(C_AXI_ID_WIDTH){1'b1}}); always @(posedge i_clk) assert(f_axi_awr_outstanding < {(C_AXI_ID_WIDTH){1'b1}}); always @(posedge i_clk) assert(f_axi_rd_outstanding < {(C_AXI_ID_WIDTH){1'b1}}); //////////////////////////////////////////////////////////////////////// // // // 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. // // //////////////////////////////////////////////////////////////////////// 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)||(axi_rd_ack)) f_axi_rd_ack_delay <= 0; else if (f_axi_rd_outstanding > 0) 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)||(axi_wr_ack)) f_axi_wr_ack_delay <= 0; else if (f_axi_wr_outstanding > 0) 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)||(axi_wr_ack)) f_axi_awr_ack_delay <= 0; else if (f_axi_awr_outstanding > 0) f_axi_awr_ack_delay <= f_axi_awr_ack_delay + 1'b1; always @(posedge i_clk) assume((F_AXI_MAXDELAY==0)||(f_axi_rd_ack_delay < F_AXI_MAXDELAY)); always @(posedge i_clk) assume((F_AXI_MAXDELAY==0)||(f_axi_wr_ack_delay < F_AXI_MAXDELAY)); always @(posedge i_clk) assume((F_AXI_MAXDELAY==0)||(f_axi_awr_ack_delay < F_AXI_MAXDELAY)); //////////////////////////////////////////////////////////////////////// // // // Assume all 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 ((!axi_awr_req)&&(axi_wr_ack)) assume(f_axi_awr_outstanding > 0); always @(posedge i_clk) if ((!axi_wr_req)&&(axi_wr_ack)) assume(f_axi_wr_outstanding > 0); // // AXI read data channel signals // initial f_axi_rd_outstanding = 0; always @(posedge i_clk) if ((!axi_ard_req)&&(axi_rd_ack)) assume(f_axi_rd_outstanding > 0); /////////////////////////////////////////////////////////////////// // // // Manage the ID buffer. Basic rules apply such as you can't // make a request of an already requested ID # before that ID // is returned, etc. // // Elements in this buffer reference transactions--possibly burst // transactions and not necessarily the individual values. // // /////////////////////////////////////////////////////////////////// // Now, let's look into that FIFO. Without it, we know nothing about // the ID's initial f_axi_rd_id_outstanding = 0; initial f_axi_wr_id_outstanding = 0; initial f_axi_awr_id_outstanding = 0; initial f_axi_wr_id_complete = 0; always @(posedge i_clk) if (!i_axi_reset_n) begin f_axi_rd_id_outstanding <= 0; f_axi_wr_id_outstanding <= 0; f_axi_wr_id_complete <= 0; f_axi_awr_id_outstanding <= 0; end else begin // When issuing a write if (axi_awr_req) begin if ((F_CONSECUTIVE_IDS)&&(F_CHECK_IDS)) assert(f_axi_awr_id_outstanding[i_axi_awid+1'b1] == 1'b0); assert((!F_CHECK_IDS) ||(f_axi_awr_id_outstanding[i_axi_awid] == 1'b0)); assert((!F_CHECK_IDS) ||(f_axi_wr_id_complete[i_axi_awid] == 1'b0)); f_axi_awr_id_outstanding[i_axi_awid] <= 1'b1; f_axi_wr_id_complete[i_axi_awid] <= 1'b0; end if (axi_wr_req) begin if ((F_CONSECUTIVE_IDS)&&(F_CHECK_IDS)) assert(f_axi_wr_id_outstanding[i_axi_awid+1'b1] == 1'b0); assert((!F_CHECK_IDS) ||(f_axi_wr_id_outstanding[i_axi_awid] == 1'b0)); f_axi_wr_id_outstanding[i_axi_awid] <= 1'b1; if (i_axi_wlast) begin assume(f_axi_wr_id_complete[i_axi_awid] == 1'b0); f_axi_wr_id_complete[i_axi_awid] <= 1'b1; end end // When issuing a read if (axi_ard_req) begin if ((F_CONSECUTIVE_IDS)&&(F_CHECK_IDS)) assert(f_axi_rd_id_outstanding[i_axi_arid+1'b1] == 1'b0); assert((!F_CHECK_IDS) ||(f_axi_rd_id_outstanding[i_axi_arid] == 1'b0)); f_axi_rd_id_outstanding[i_axi_arid] <= 1'b1; end // When a write is acknowledged if (axi_wr_ack) begin if (F_CHECK_IDS) begin assume(f_axi_awr_id_outstanding[i_axi_bid]); assume(f_axi_wr_id_outstanding[i_axi_bid]); assume((!F_STRICT_ORDER)||(!F_CONSECUTIVE_IDS) ||(!f_axi_wr_id_outstanding[i_axi_bid-1'b1])); assume((!F_STRICT_ORDER)||(!F_CONSECUTIVE_IDS) ||(!f_axi_awr_id_outstanding[i_axi_bid-1'b1])); assume(f_axi_wr_id_complete[i_axi_bid]); end f_axi_awr_id_outstanding[i_axi_bid] <= 1'b0; f_axi_wr_id_outstanding[i_axi_bid] <= 1'b0; f_axi_wr_id_complete[i_axi_bid] <= 1'b0; end // When a read is acknowledged if (axi_rd_ack) begin if (F_CHECK_IDS) begin assume(f_axi_rd_id_outstanding[i_axi_rid]); assume((!F_STRICT_ORDER)||(!F_CONSECUTIVE_IDS) ||(!f_axi_rd_id_outstanding[i_axi_rid-1'b1])); end if (i_axi_rlast) f_axi_rd_id_outstanding[i_axi_rid] <= 1'b0; end end reg [LGFIFOLN:0] f_axi_rd_id_outstanding_count, f_axi_awr_id_outstanding_count, f_axi_wr_id_outstanding_count; initial f_axi_rd_id_outstanding_count = 0; initial f_axi_awr_id_outstanding_count = 0; initial f_axi_wr_id_outstanding_count = 0; always @(*) begin // f_axi_rd_id_outstanding_count = 0; for(k=0; k< FIFOLN; k=k+1) if (f_axi_rd_id_outstanding[k]) f_axi_rd_id_outstanding_count = f_axi_rd_id_outstanding_count +1; // f_axi_wr_id_outstanding_count = 0; for(k=0; k< FIFOLN; k=k+1) if (f_axi_wr_id_outstanding[k]) f_axi_wr_id_outstanding_count = f_axi_wr_id_outstanding_count +1; f_axi_awr_id_outstanding_count = 0; for(k=0; k< FIFOLN; k=k+1) if (f_axi_awr_id_outstanding[k]) f_axi_awr_id_outstanding_count = f_axi_awr_id_outstanding_count +1; end always @(*) assert((!F_CHECK_IDS)||(f_axi_awr_outstanding== f_axi_awr_id_outstanding_count)); always @(*) assert((!F_CHECK_IDS)||(f_axi_wr_outstanding == f_axi_wr_id_outstanding_count)); always @(*) assert((!F_CHECK_IDS)||(f_axi_rd_outstanding == f_axi_rd_id_outstanding_count)); always @(*) assume( ((f_axi_wr_id_complete)&(~f_axi_awr_id_outstanding)) == 0); generate if (F_OPT_BURSTS) begin reg [(8-1):0] f_rd_pending [0:(FIFOLN-1)]; reg [(8-1):0] f_wr_pending, f_rd_count, f_wr_count; reg r_last_rd_id_valid, r_last_wr_id_valid; reg [(C_AXI_ID_WIDTH-1):0] r_last_wr_id, r_last_rd_id; initial r_last_wr_id_valid = 1'b0; initial r_last_rd_id_valid = 1'b0; always @(posedge i_clk) if (!i_axi_reset_n) begin r_last_wr_id_valid <= 1'b0; r_last_rd_id_valid <= 1'b0; f_wr_count <= 0; f_rd_count <= 0; end else begin if (axi_awr_req) begin f_wr_pending <= i_axi_awlen+9'h1; assert(f_wr_pending == 0); r_last_wr_id_valid <= 1'b1; end if (axi_ard_req) f_rd_pending[i_axi_arid] <= i_axi_arlen+9'h1; if ((axi_wr_req)&&(i_axi_wlast)) begin f_wr_count <= 0; r_last_wr_id_valid <= 1'b0; assert( // Either this is the last // of a series of requests we've // been waiting for, (f_wr_pending == f_wr_count - 9'h1) // *or* the only value // associated with an as yet // to be counted request ||((axi_awr_req)&&(i_axi_awlen == 0))); end else if (axi_wr_req) f_wr_count <= f_wr_count + 1'b1; if (axi_rd_ack) begin if (i_axi_rlast) r_last_rd_id_valid <= 1'b0; else r_last_rd_id_valid <= 1'b1; r_last_rd_id <= i_axi_rid; if ((axi_rd_ack)&&(r_last_rd_id_valid)) assume(i_axi_rid == r_last_rd_id); end if ((axi_rd_ack)&&(i_axi_rlast)) assert(f_rd_count == f_rd_pending[i_axi_rid]-9'h1); if ((axi_rd_ack)&&(i_axi_rlast)) f_rd_count <= 0; else if (axi_rd_ack) f_rd_count <= f_rd_count + 1'b1; end end else begin always @(*) begin // Since we aren't allowing bursts, *every* // write data and read data must always be the last // value assert((i_axi_wlast)||(!i_axi_wvalid)); assume((i_axi_rlast)||(!i_axi_rvalid)); assert((!i_axi_arvalid)||(i_axi_arlen==0)); assert((!i_axi_awvalid)||(i_axi_awlen==0)); end always @(posedge i_clk) if (i_axi_awvalid) assert(i_axi_awlen == 0); always @(posedge i_clk) if (i_axi_arvalid) assert(i_axi_arlen == 0); always @(posedge i_clk) if (i_axi_wvalid) assert(i_axi_wlast); always @(posedge i_clk) if (i_axi_rvalid) assume(i_axi_rlast); end endgenerate `endif endmodule
Go to most recent revision | Compare with Previous | Blame | View Log