| //////////////////////////////////////////////////////////////////////////////// |
| // |
| // Filename: wbm2axisp.v (Wishbone master to AXI slave, pipelined) |
| // {{{ |
| // Project: WB2AXIPSP: bus bridges and other odds and ends |
| // |
| // Purpose: The B4 Wishbone SPEC allows transactions at a speed as fast as |
| // one per clock. The AXI bus allows transactions at a speed of |
| // one read and one write transaction per clock. These capabilities work |
| // by allowing requests to take place prior to responses, such that the |
| // requests might go out at once per clock and take several clocks, and |
| // the responses may start coming back several clocks later. In other |
| // words, both protocols allow multiple transactions to be "in flight" at |
| // the same time. Current wishbone to AXI converters, however, handle only |
| // one transaction at a time: initiating the transaction, and then waiting |
| // for the transaction to complete before initiating the next. |
| // |
| // The purpose of this core is to maintain the speed of both buses, while |
| // transiting from the Wishbone (as master) to the AXI bus (as slave) and |
| // back again. |
| // |
| // Creator: Dan Gisselquist, Ph.D. |
| // Gisselquist Technology, LLC |
| // |
| //////////////////////////////////////////////////////////////////////////////// |
| // }}} |
| // Copyright (C) 2016-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 wbm2axisp #( |
| // {{{ |
| parameter C_AXI_DATA_WIDTH = 128,// Width of the AXI R&W data |
| parameter C_AXI_ADDR_WIDTH = 28, // AXI Address width (log wordsize) |
| parameter C_AXI_ID_WIDTH = 1, |
| parameter DW = 32, // Wishbone data width |
| parameter AW = 26, // Wishbone address width (log wordsize) |
| parameter [C_AXI_ID_WIDTH-1:0] AXI_WRITE_ID = 1'b0, |
| parameter [C_AXI_ID_WIDTH-1:0] AXI_READ_ID = 1'b1, |
| // |
| // OPT_LITTLE_ENDIAN controls which word has the greatest address |
| // when the bus size is adjusted. If OPT_LITTLE_ENDIAN is true, |
| // the biggest address is in the most significant word(s), otherwise |
| // the least significant word(s). This parameter is ignored if |
| // C_AXI_DATA_WIDTH == DW. |
| parameter [0:0] OPT_LITTLE_ENDIAN = 1'b1, |
| parameter LGFIFO = 6 |
| // }}} |
| ) ( |
| // {{{ |
| input wire i_clk, // System clock |
| input wire i_reset,// Reset signal,drives AXI rst |
| |
| // AXI write address channel signals |
| output reg o_axi_awvalid, // Write address valid |
| input wire i_axi_awready, // Slave is ready to accept |
| output wire [C_AXI_ID_WIDTH-1:0] o_axi_awid, // Write ID |
| output reg [C_AXI_ADDR_WIDTH-1:0] o_axi_awaddr, // Write address |
| output wire [7:0] o_axi_awlen, // Write Burst Length |
| output wire [2:0] o_axi_awsize, // Write Burst size |
| output wire [1:0] o_axi_awburst, // Write Burst type |
| output wire [0:0] o_axi_awlock, // Write lock type |
| output wire [3:0] o_axi_awcache, // Write Cache type |
| output wire [2:0] o_axi_awprot, // Write Protection type |
| output wire [3:0] o_axi_awqos, // Write Quality of Svc |
| |
| // AXI write data channel signals |
| output reg o_axi_wvalid, // Write valid |
| input wire i_axi_wready, // Write data ready |
| output reg [C_AXI_DATA_WIDTH-1:0] o_axi_wdata, // Write data |
| output reg [C_AXI_DATA_WIDTH/8-1:0] o_axi_wstrb, // Write strobes |
| output wire o_axi_wlast, // Last write transaction |
| |
| // AXI write response channel signals |
| input wire i_axi_bvalid, // Write reponse valid |
| output wire o_axi_bready, // Response ready |
| input wire [C_AXI_ID_WIDTH-1:0] i_axi_bid, // Response ID |
| input wire [1:0] i_axi_bresp, // Write response |
| |
| // AXI read address channel signals |
| output reg o_axi_arvalid, // Read address valid |
| input wire i_axi_arready, // Read address ready |
| output wire [C_AXI_ID_WIDTH-1:0] o_axi_arid, // Read ID |
| output reg [C_AXI_ADDR_WIDTH-1:0] o_axi_araddr, // Read address |
| output wire [7:0] o_axi_arlen, // Read Burst Length |
| output wire [2:0] o_axi_arsize, // Read Burst size |
| output wire [1:0] o_axi_arburst, // Read Burst type |
| output wire [0:0] o_axi_arlock, // Read lock type |
| output wire [3:0] o_axi_arcache, // Read Cache type |
| output wire [2:0] o_axi_arprot, // Read Protection type |
| output wire [3:0] o_axi_arqos, // Read Protection type |
| |
| // AXI read data channel signals |
| input wire i_axi_rvalid, // Read reponse valid |
| output wire o_axi_rready, // Read Response ready |
| input wire [C_AXI_ID_WIDTH-1:0] i_axi_rid, // Response ID |
| input wire [C_AXI_DATA_WIDTH-1:0] i_axi_rdata, // Read data |
| input wire [1:0] i_axi_rresp, // Read response |
| input wire i_axi_rlast, // Read last |
| |
| // We'll share the clock and the reset |
| input wire i_wb_cyc, |
| input wire i_wb_stb, |
| input wire i_wb_we, |
| input wire [(AW-1):0] i_wb_addr, |
| input wire [(DW-1):0] i_wb_data, |
| input wire [(DW/8-1):0] i_wb_sel, |
| output reg o_wb_stall, |
| output reg o_wb_ack, |
| output reg [(DW-1):0] o_wb_data, |
| output reg o_wb_err |
| // }}} |
| ); |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Localparameter declarations, initial parameter consistency check |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| localparam LG_AXI_DW = $clog2(C_AXI_DATA_WIDTH); |
| localparam LG_WB_DW = $clog2(DW); |
| localparam FIFOLN = (1<<LGFIFO); |
| localparam SUBW = LG_AXI_DW-LG_WB_DW; |
| |
| // The various address widths must be properly related. We'll insist |
| // upon that relationship here. |
| initial begin |
| // This design can't (currently) handle WB widths wider than |
| // the AXI width it is driving. It can only handle widths |
| // mismatches in the other direction |
| if (C_AXI_DATA_WIDTH < DW) |
| $stop; |
| if (DW == 8 && AW != C_AXI_ADDR_WIDTH) |
| $stop; |
| |
| // There must be a definitive relationship between the address |
| // widths of the AXI and WB, and that width is dependent upon |
| // the WB data width |
| if (C_AXI_ADDR_WIDTH != AW + $clog2(DW)-3) |
| $stop; |
| if ( (C_AXI_DATA_WIDTH / DW !=32) |
| &&(C_AXI_DATA_WIDTH / DW !=16) |
| &&(C_AXI_DATA_WIDTH / DW != 8) |
| &&(C_AXI_DATA_WIDTH / DW != 4) |
| &&(C_AXI_DATA_WIDTH / DW != 2) |
| &&(C_AXI_DATA_WIDTH != DW)) |
| $stop; |
| end |
| // }}} |
| |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Internal register and wire declarations |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| |
| // Things we're not changing ... |
| localparam DWSIZE = $clog2(DW)-3; |
| assign o_axi_awid = AXI_WRITE_ID; |
| assign o_axi_awlen = 8'h0; // Burst length is one |
| assign o_axi_awsize = DWSIZE[2:0]; |
| assign o_axi_wlast = 1; |
| assign o_axi_awburst = 2'b01; // Incrementing address (ignored) |
| assign o_axi_awlock = 1'b0; // Normal signaling |
| assign o_axi_arlock = 1'b0; // Normal signaling |
| assign o_axi_awcache = 4'h3; // Normal: no cache, modifiable |
| // |
| assign o_axi_arid = AXI_READ_ID; |
| assign o_axi_arlen = 8'h0; // Burst length is one |
| assign o_axi_arsize = DWSIZE[2:0]; |
| assign o_axi_arburst = 2'b01; // Incrementing address (ignored) |
| assign o_axi_arcache = 4'h3; // Normal: no cache, modifiable |
| assign o_axi_awprot = 3'b010; // Unpriviledged, unsecure, data access |
| assign o_axi_arprot = 3'b010; // Unpriviledged, unsecure, data access |
| assign o_axi_awqos = 4'h0; // Lowest quality of service (unused) |
| assign o_axi_arqos = 4'h0; // Lowest quality of service (unused) |
| |
| reg direction, full, empty, flushing, nearfull; |
| reg [LGFIFO:0] npending; |
| // |
| wire skid_ready, m_valid, m_we; |
| reg m_ready; |
| wire [AW-1:0] m_addr; |
| wire [DW-1:0] m_data; |
| wire [DW/8-1:0] m_sel; |
| |
| // }}} |
| |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Overarching command logic |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| initial direction = 0; |
| always @(posedge i_clk) |
| if (empty) |
| direction <= m_we; |
| |
| initial npending = 0; |
| initial empty = 1; |
| initial full = 0; |
| initial nearfull = 0; |
| always @(posedge i_clk) |
| if (i_reset) |
| begin |
| npending <= 0; |
| empty <= 1; |
| full <= 0; |
| nearfull <= 0; |
| end else case ({m_valid && m_ready, i_axi_bvalid||i_axi_rvalid}) |
| 2'b10: begin |
| npending <= npending + 1; |
| empty <= 0; |
| nearfull <= &(npending[LGFIFO-1:1]); |
| full <= &(npending[LGFIFO-1:0]); |
| end |
| 2'b01: begin |
| nearfull <= full; |
| npending <= npending - 1; |
| empty <= (npending == 1); |
| full <= 0; |
| end |
| default: begin end |
| endcase |
| |
| initial flushing = 0; |
| always @(posedge i_clk) |
| if (i_reset) |
| flushing <= 0; |
| else if ((i_axi_rvalid && i_axi_rresp[1]) |
| ||(i_axi_bvalid && i_axi_bresp[1]) |
| ||(!i_wb_cyc && !empty)) |
| flushing <= 1'b1; |
| else if (empty) |
| flushing <= 1'b0; |
| // }}} |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Wishbone input skidbuffer |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| skidbuffer #(.DW(1+AW+DW+(DW/8)), |
| .OPT_OUTREG(1'b0)) |
| skid (i_clk, i_reset || !i_wb_cyc, |
| i_wb_stb, skid_ready, |
| { i_wb_we, i_wb_addr, i_wb_data, i_wb_sel }, |
| m_valid, m_ready, |
| { m_we, m_addr, m_data, m_sel }); |
| |
| always @(*) |
| o_wb_stall = !skid_ready; |
| |
| always @(*) |
| begin |
| m_ready = 1; |
| |
| if (flushing || nearfull || ((m_we != direction)&&(!empty))) |
| m_ready = 1'b0; |
| if (o_axi_awvalid && !i_axi_awready) |
| m_ready = 1'b0; |
| if (o_axi_wvalid && !i_axi_wready) |
| m_ready = 1'b0; |
| if (o_axi_arvalid && !i_axi_arready) |
| m_ready = 1'b0; |
| end |
| // }}} |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // AXI Signaling |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| |
| // |
| // Write transactions |
| // |
| |
| // awvalid, wvalid |
| // {{{ |
| // Send write transactions |
| initial o_axi_awvalid = 0; |
| initial o_axi_wvalid = 0; |
| always @(posedge i_clk) |
| if (i_reset) |
| begin |
| o_axi_awvalid <= 0; |
| o_axi_wvalid <= 0; |
| end else if (m_valid && m_we && m_ready) |
| begin |
| o_axi_awvalid <= 1; |
| o_axi_wvalid <= 1; |
| end else begin |
| if (i_axi_awready) |
| o_axi_awvalid <= 0; |
| if (i_axi_wready) |
| o_axi_wvalid <= 0; |
| end |
| // }}} |
| |
| // wdata |
| // {{{ |
| always @(posedge i_clk) |
| if (!o_axi_wvalid || i_axi_wready) |
| o_axi_wdata <= {(C_AXI_DATA_WIDTH/DW){m_data}}; |
| // }}} |
| |
| // wstrb |
| // {{{ |
| generate if (DW == C_AXI_DATA_WIDTH) |
| begin : NO_WSTRB_ADJUSTMENT |
| // {{{ |
| always @(posedge i_clk) |
| if (!o_axi_wvalid || i_axi_wready) |
| o_axi_wstrb <= m_sel; |
| // }}} |
| end else if (OPT_LITTLE_ENDIAN) |
| begin : LITTLE_ENDIAN_WSTRB |
| // {{{ |
| always @(posedge i_clk) |
| if (!o_axi_wvalid || i_axi_wready) |
| // Verilator lint_off WIDTH |
| o_axi_wstrb <= m_sel << ((DW/8) * m_addr[SUBW-1:0]); |
| // Verilator lint_on WIDTH |
| // }}} |
| end else begin : BIG_ENDIAN_WSTRB |
| // {{{ |
| reg [SUBW-1:0] neg_addr; |
| |
| always @(*) |
| neg_addr = ~m_addr[SUBW-1:0]; |
| |
| always @(posedge i_clk) |
| if (!o_axi_wvalid || i_axi_wready) |
| // Verilator lint_off WIDTH |
| o_axi_wstrb <= m_sel << ((DW/8)* neg_addr); |
| // Verilator lint_on WIDTH |
| // }}} |
| end endgenerate |
| // }}} |
| |
| // |
| // Read transactions |
| // |
| |
| // arvalid |
| // {{{ |
| initial o_axi_arvalid = 0; |
| always @(posedge i_clk) |
| if (i_reset) |
| o_axi_arvalid <= 0; |
| else if (m_valid && !m_we && m_ready) |
| o_axi_arvalid <= 1; |
| else if (i_axi_arready) |
| begin |
| o_axi_arvalid <= 0; |
| end |
| // }}} |
| |
| // awaddr, araddr |
| // {{{ |
| generate if (OPT_LITTLE_ENDIAN || DW == C_AXI_DATA_WIDTH) |
| begin |
| // {{{ |
| always @(posedge i_clk) |
| if (!o_axi_awvalid || i_axi_awready) |
| o_axi_awaddr <= { m_addr, {($clog2(DW)-3){1'b0}} }; |
| |
| always @(posedge i_clk) |
| if (!o_axi_arvalid || i_axi_arready) |
| o_axi_araddr <= { m_addr, {($clog2(DW)-3){1'b0}} }; |
| // }}} |
| end else begin : OPT_BIG_ENDIAN |
| // {{{ |
| reg [SUBW-1:0] neg_addr; |
| |
| always @(*) |
| neg_addr = ~m_addr[SUBW-1:0]; |
| |
| always @(posedge i_clk) |
| if (!o_axi_awvalid || i_axi_awready) |
| begin |
| o_axi_awaddr <= 0; |
| o_axi_awaddr <= m_addr << ($clog2(DW)-3); |
| o_axi_awaddr[$clog2(DW)-3 +: SUBW] <= neg_addr; |
| end |
| |
| always @(posedge i_clk) |
| if (!o_axi_arvalid || i_axi_arready) |
| begin |
| o_axi_araddr <= 0; |
| o_axi_araddr <= m_addr << ($clog2(DW)-3); |
| o_axi_araddr[$clog2(DW)-3 +: SUBW] <= neg_addr; |
| end |
| // }}} |
| end endgenerate |
| // }}} |
| |
| // rdata, and returned o_wb_data, o_wb_ack, o_wb_err |
| // {{{ |
| generate if (DW == C_AXI_DATA_WIDTH) |
| begin : NO_READ_DATA_SELECT_NECESSARY |
| // {{{ |
| always @(*) |
| o_wb_data = i_axi_rdata; |
| |
| always @(*) |
| o_wb_ack = !flushing&&((i_axi_rvalid && !i_axi_rresp[1]) |
| ||(i_axi_bvalid && !i_axi_bresp[1])); |
| |
| always @(*) |
| o_wb_err = !flushing&&((i_axi_rvalid && i_axi_rresp[1]) |
| ||(i_axi_bvalid && i_axi_bresp[1])); |
| // }}} |
| end else begin : READ_FIFO_DATA_SELECT |
| // {{{ |
| |
| reg [SUBW-1:0] addr_fifo [0:(1<<LGFIFO)-1]; |
| reg [SUBW-1:0] fifo_value; |
| reg [LGFIFO:0] wr_addr, rd_addr; |
| wire [C_AXI_DATA_WIDTH-1:0] return_data; |
| |
| initial o_wb_ack = 0; |
| always @(posedge i_clk) |
| if (i_reset || !i_wb_cyc || flushing) |
| o_wb_ack <= 0; |
| else |
| o_wb_ack <= ((i_axi_rvalid && !i_axi_rresp[1]) |
| ||(i_axi_bvalid && !i_axi_bresp[1])); |
| |
| initial o_wb_err = 0; |
| always @(posedge i_clk) |
| if (i_reset || !i_wb_cyc || flushing) |
| o_wb_err <= 0; |
| else |
| o_wb_err <= ((i_axi_rvalid && i_axi_rresp[1]) |
| ||(i_axi_bvalid && i_axi_bresp[1])); |
| |
| |
| initial wr_addr = 0; |
| always @(posedge i_clk) |
| if (i_reset) |
| wr_addr <= 0; |
| else if (m_valid && m_ready) |
| wr_addr <= wr_addr + 1; |
| |
| always @(posedge i_clk) |
| if (m_valid && m_ready) |
| addr_fifo[wr_addr[LGFIFO-1:0]] <= m_addr[SUBW-1:0]; |
| |
| initial rd_addr = 0; |
| always @(posedge i_clk) |
| if (i_reset) |
| rd_addr <= 0; |
| else if (i_axi_bvalid || i_axi_rvalid) |
| rd_addr <= rd_addr + 1; |
| |
| always @(*) |
| fifo_value = addr_fifo[rd_addr[LGFIFO-1:0]]; |
| |
| if (OPT_LITTLE_ENDIAN) |
| begin : LITTLE_ENDIAN_RDATA |
| |
| assign return_data = i_axi_rdata >> (fifo_value * DW); |
| |
| end else begin : BIG_ENDIAN_RDATA |
| |
| reg [SUBW-1:0] neg_fifo_value; |
| |
| always @(*) |
| neg_fifo_value = ~fifo_value; |
| |
| assign return_data = i_axi_rdata |
| >> (neg_fifo_value * DW); |
| |
| end |
| |
| always @(posedge i_clk) |
| o_wb_data <= return_data[DW-1:0]; |
| |
| // Make Verilator happy here |
| if (C_AXI_DATA_WIDTH > DW) |
| begin : UNUSED_DATA |
| // verilator lint_off UNUSED |
| wire unused_data; |
| assign unused_data = &{ 1'b0, |
| return_data[C_AXI_DATA_WIDTH-1:DW] }; |
| end |
| // verilator lint_on UNUSED |
| `ifdef FORMAL |
| always @(*) |
| assert(wr_addr - rd_addr == npending); |
| |
| always @(*) |
| assert(empty == (wr_addr == rd_addr)); |
| |
| |
| // |
| // ... |
| // |
| `endif |
| // }}} |
| end endgenerate |
| // }}} |
| |
| // Read data channel / response logic |
| assign o_axi_rready = 1'b1; |
| assign o_axi_bready = 1'b1; |
| // }}} |
| |
| // Make verilator's -Wall happy |
| // {{{ |
| // verilator lint_off UNUSED |
| wire unused; |
| assign unused = &{ 1'b0, full, i_axi_bid, i_axi_bresp[0], i_axi_rid, i_axi_rresp[0], i_axi_rlast, m_data, m_sel }; |
| generate if (C_AXI_DATA_WIDTH > DW) |
| begin |
| wire [C_AXI_DATA_WIDTH-1:DW] unused_data; |
| assign unused_data = i_axi_rdata[C_AXI_DATA_WIDTH-1:DW]; |
| end endgenerate |
| // verilator lint_on UNUSED |
| // }}} |
| |
| ///////////////////////////////////////////////////////////////////////// |
| ///////////////////////////////////////////////////////////////////////// |
| ///////////////////////////////////////////////////////////////////////// |
| // |
| // Formal methods section |
| // {{{ |
| // Below are a scattering of the formal properties used. They are not the |
| // complete set of properties. Those are maintained elsewhere. |
| ///////////////////////////////////////////////////////////////////////// |
| ///////////////////////////////////////////////////////////////////////// |
| ///////////////////////////////////////////////////////////////////////// |
| `ifdef FORMAL |
| // |
| // ... |
| // |
| |
| // Parameters |
| initial assert( (C_AXI_DATA_WIDTH / DW ==32) |
| ||(C_AXI_DATA_WIDTH / DW ==16) |
| ||(C_AXI_DATA_WIDTH / DW == 8) |
| ||(C_AXI_DATA_WIDTH / DW == 4) |
| ||(C_AXI_DATA_WIDTH / DW == 2) |
| ||(C_AXI_DATA_WIDTH == DW)); |
| // |
| initial assert( C_AXI_ADDR_WIDTH == AW + (LG_WB_DW-3)); |
| |
| |
| initial begin |
| assert(C_AXI_DATA_WIDTH >= DW); |
| assert(DW == 8 && AW == C_AXI_ADDR_WIDTH); |
| assert(C_AXI_ADDR_WIDTH == AW + $clog2(DW)-3); |
| end |
| // }}} |
| |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Setup / f_past_valid |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| |
| initial f_past_valid = 1'b0; |
| always @(posedge i_clk) |
| f_past_valid <= 1'b1; |
| // }}} |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Assumptions about the WISHBONE inputs |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| always @(*) |
| if (!f_past_valid) |
| assume(i_reset); |
| |
| fwb_slave #(.DW(DW),.AW(AW), |
| .F_MAX_STALL(0), |
| .F_MAX_ACK_DELAY(0), |
| .F_LGDEPTH(F_LGDEPTH), |
| .F_MAX_REQUESTS(0)) |
| f_wb(i_clk, i_reset, i_wb_cyc, i_wb_stb, i_wb_we, i_wb_addr, |
| i_wb_data, i_wb_sel, |
| o_wb_ack, o_wb_stall, o_wb_data, o_wb_err, |
| f_wb_nreqs, f_wb_nacks, f_wb_outstanding); |
| |
| // }}} |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Assumptions about the AXI inputs |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| |
| faxi_master #( |
| // {{{ |
| .C_AXI_ID_WIDTH(C_AXI_ID_WIDTH), |
| .C_AXI_DATA_WIDTH(C_AXI_DATA_WIDTH), |
| .C_AXI_ADDR_WIDTH(C_AXI_ADDR_WIDTH) |
| // ... |
| // }}} |
| ) f_axi(.i_clk(i_clk), .i_axi_reset_n(!i_reset), |
| // {{{ |
| // Write address channel |
| .i_axi_awready(i_axi_awready), |
| .i_axi_awid( o_axi_awid), |
| .i_axi_awaddr( o_axi_awaddr), |
| .i_axi_awlen( o_axi_awlen), |
| .i_axi_awsize( o_axi_awsize), |
| .i_axi_awburst(o_axi_awburst), |
| .i_axi_awlock( o_axi_awlock), |
| .i_axi_awcache(o_axi_awcache), |
| .i_axi_awprot( o_axi_awprot), |
| .i_axi_awqos( o_axi_awqos), |
| .i_axi_awvalid(o_axi_awvalid), |
| // Write data channel |
| .i_axi_wready( i_axi_wready), |
| .i_axi_wdata( o_axi_wdata), |
| .i_axi_wstrb( o_axi_wstrb), |
| .i_axi_wlast( o_axi_wlast), |
| .i_axi_wvalid( o_axi_wvalid), |
| // Write response channel |
| .i_axi_bid( i_axi_bid), |
| .i_axi_bresp( i_axi_bresp), |
| .i_axi_bvalid( i_axi_bvalid), |
| .i_axi_bready( o_axi_bready), |
| // Read address channel |
| .i_axi_arready(i_axi_arready), |
| .i_axi_arid( o_axi_arid), |
| .i_axi_araddr( o_axi_araddr), |
| .i_axi_arlen( o_axi_arlen), |
| .i_axi_arsize( o_axi_arsize), |
| .i_axi_arburst(o_axi_arburst), |
| .i_axi_arlock( o_axi_arlock), |
| .i_axi_arcache(o_axi_arcache), |
| .i_axi_arprot( o_axi_arprot), |
| .i_axi_arqos( o_axi_arqos), |
| .i_axi_arvalid(o_axi_arvalid), |
| // Read data channel |
| .i_axi_rid( i_axi_rid), |
| .i_axi_rresp( i_axi_rresp), |
| .i_axi_rvalid( i_axi_rvalid), |
| .i_axi_rdata( i_axi_rdata), |
| .i_axi_rlast( i_axi_rlast), |
| .i_axi_rready( o_axi_rready), |
| // Counts |
| .f_axi_awr_nbursts(f_axi_awr_nbursts), |
| .f_axi_wr_pending(f_axi_wr_pending), |
| .f_axi_rd_nbursts(f_axi_rd_nbursts), |
| .f_axi_rd_outstanding(f_axi_rd_outstanding) |
| // |
| // ... |
| // |
| // }}} |
| ); |
| |
| always @(*) |
| if (!flushing && i_wb_cyc) |
| assert(f_wb_outstanding == npending + (r_stb ? 1:0) |
| + ( ((C_AXI_DATA_WIDTH != DW) |
| && (o_wb_ack|o_wb_err))? 1:0)); |
| else if (flushing && i_wb_cyc && !o_wb_err) |
| assert(f_wb_outstanding == (r_stb ? 1:0)); |
| |
| always @(*) |
| if (f_axi_awr_nbursts > 0) |
| begin |
| assert(direction); |
| assert(f_axi_rd_nbursts == 0); |
| assert(f_axi_awr_nbursts + (o_axi_awvalid ? 1:0) == npending); |
| assert(f_axi_wr_pending == (o_axi_wvalid&&!o_axi_awvalid ? 1:0)); |
| |
| // |
| // ... |
| // |
| end |
| always @(*) |
| if (o_axi_awvalid) |
| assert(o_axi_wvalid); |
| |
| // Some quick read checks |
| always @(*) |
| if (f_axi_rd_nbursts > 0) |
| begin |
| assert(!direction); |
| assert(f_axi_rd_nbursts+(o_axi_arvalid ? 1:0) |
| == npending); |
| assert(f_axi_awr_nbursts == 0); |
| |
| // |
| // ... |
| // |
| end |
| |
| always @(*) |
| if (direction) |
| begin |
| assert(npending == (o_axi_awvalid ? 1:0) + f_axi_awr_nbursts); |
| assert(!o_axi_arvalid); |
| assert(f_axi_rd_nbursts == 0); |
| assert(!i_axi_rvalid); |
| end else begin |
| assert(npending == (o_axi_arvalid ? 1:0) + f_axi_rd_nbursts); |
| assert(!o_axi_awvalid); |
| assert(!o_axi_wvalid); |
| assert(f_axi_awr_nbursts == 0); |
| end |
| // }}} |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Pending counter properties |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| |
| always @(*) |
| begin |
| assert(npending <= { 1'b1, {(LGFIFO){1'b0}} }); |
| assert(empty == (npending == 0)); |
| assert(full == (npending == {1'b1, {(LGFIFO){1'b0}}})); |
| assert(nearfull == (npending >= {1'b0, {(LGFIFO){1'b1}}})); |
| if (full) |
| assert(o_wb_stall); |
| end |
| // }}} |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Assertions about the AXI4 ouputs |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| |
| // Write response channel |
| always @(posedge i_clk) |
| // We keep bready high, so the other condition doesn't |
| // need to be checked |
| assert(o_axi_bready); |
| |
| // AXI read data channel signals |
| always @(posedge i_clk) |
| // We keep o_axi_rready high, so the other condition's |
| // don't need to be checked here |
| assert(o_axi_rready); |
| |
| // |
| // AXI write address channel |
| // |
| // |
| always @(*) |
| begin |
| if (o_axi_awvalid || o_axi_wvalid || f_axi_awr_nbursts>0) |
| assert(direction); |
| // |
| // ... |
| // |
| end |
| // |
| // AXI read address channel |
| // |
| always @(*) |
| begin |
| if (o_axi_arvalid || i_axi_rvalid || f_axi_rd_nbursts > 0) |
| assert(!direction); |
| // |
| // ... |
| // |
| end |
| |
| // |
| // AXI write response channel |
| // |
| |
| |
| // |
| // AXI read data channel signals |
| // |
| // }}} |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Formal contract check |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Prove that a write to this address will change this value |
| // |
| |
| // Some extra register declarations |
| // {{{ |
| (* anyconst *) reg [C_AXI_ADDR_WIDTH-1:0] f_const_addr; |
| reg [C_AXI_DATA_WIDTH-1:0] f_data; |
| // }}} |
| |
| // |
| // Assume a basic bus response to the given data and address |
| // |
| integer iN; |
| |
| // f_data |
| // {{{ |
| initial f_data = 0; |
| always @(posedge i_clk) |
| if (o_axi_wvalid && i_axi_wready && o_axi_awaddr == f_const_addr) |
| begin |
| for(iN=0; iN<C_AXI_DATA_WIDTH/8; iN=iN+1) |
| begin |
| if (o_axi_wstrb[iN]) |
| f_data[8*iN +: 8] <= o_axi_wdata[8*iN +: 8]; |
| end |
| end |
| // }}} |
| |
| // Assume RDATA == f_data if appropriate |
| // {{{ |
| always @(*) |
| if (i_axi_rvalid && o_axi_rready && f_axi_rd_ckvalid |
| && (f_axi_rd_ckaddr == f_const_addr)) |
| assume(i_axi_rdata == f_data); |
| // }}} |
| |
| // f_wb_addr -- A WB address designed to match f_const_addr (AXI addr) |
| // {{{ |
| always @(*) |
| begin |
| f_wb_addr = f_const_addr[C_AXI_ADDR_WIDTH-1:DWSIZE]; |
| if (!OPT_LITTLE_ENDIAN && SUBW > 0) |
| f_wb_addr[0 +: SUBW] = ~f_wb_addr[0 +: SUBW]; |
| end |
| // }}} |
| |
| // Assume the address is Wishbone word aligned |
| // {{{ |
| generate if (DW > 8) |
| begin |
| always @(*) |
| assume(f_const_addr[$clog2(DW)-4:0] == 0); |
| end endgenerate |
| // }}} |
| |
| // f_axi_data -- Replicate f_wb_data across the whole word |
| // {{{ |
| always @(*) |
| f_axi_data = {(C_AXI_DATA_WIDTH/DW){f_wb_data}}; |
| // }}} |
| |
| // |
| // ... |
| // |
| |
| always @(*) |
| begin |
| f_valid_wb_response = 1; |
| for(iN=0; iN<DW/8; iN=iN+1) |
| begin |
| if (f_wb_strb[iN] && (o_wb_data[iN*8 +: 8] != f_wb_data[iN*8 +: 8])) |
| f_valid_wb_response = 0; |
| end |
| end |
| // }}} |
| |
| // f_valid_axi_data |
| // {{{ |
| always @(*) |
| begin |
| f_valid_axi_data = 1; |
| for(iN=0; iN<C_AXI_DATA_WIDTH/8; iN=iN+1) |
| begin |
| if (f_axi_strb[iN] && (f_axi_data[iN*8 +: 8] != f_data[iN*8 +: 8])) |
| f_valid_axi_data = 0; |
| end |
| end |
| // }}} |
| |
| // f_valid_axi_response |
| // {{{ |
| always @(*) |
| begin |
| f_valid_axi_response = 1; |
| for(iN=0; iN<C_AXI_DATA_WIDTH/8; iN=iN+1) |
| begin |
| if (f_axi_strb[iN] && (i_axi_rdata[iN*8 +: 8] != f_data[iN*8 +: 8])) |
| f_valid_axi_response = 0; |
| end |
| end |
| // }}} |
| |
| // |
| // ... |
| // |
| |
| generate if (DW == C_AXI_DATA_WIDTH) |
| begin |
| |
| always @(*) |
| f_axi_strb = f_wb_strb; |
| |
| end else if (OPT_LITTLE_ENDIAN) |
| begin |
| |
| always @(*) |
| f_axi_strb <= f_wb_strb << ( (DW/8) * |
| f_wb_addr[SUBW-1:0]); |
| |
| end else // if (!OPT_LITTLE_ENDIAN) |
| begin |
| reg [SUBW-1:0] f_neg_addr; |
| |
| always @(*) |
| f_neg_addr = ~f_wb_addr[SUBW-1:0]; |
| |
| always @(*) |
| f_axi_strb <= f_wb_strb << ( (DW/8) * f_neg_addr ); |
| |
| end endgenerate |
| // }}} |
| |
| |
| // }}} |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Ad-hoc assertions |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| |
| generate if (DW > 8) |
| begin |
| always @(*) |
| if (o_axi_awvalid) |
| assert(o_axi_awaddr[$clog2(DW)-4:0] == 0); |
| |
| always @(*) |
| if (o_axi_arvalid) |
| assert(o_axi_araddr[$clog2(DW)-4:0] == 0); |
| |
| end endgenerate |
| |
| // }}} |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Cover checks |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| reg [F_LGDEPTH-1:0] r_hit_reads, r_hit_writes, |
| r_check_fault, check_fault, |
| cvr_nreads, cvr_nwrites; |
| reg cvr_flushed, cvr_read2write, cvr_write2read; |
| |
| initial r_hit_reads = 0; |
| always @(posedge i_clk) |
| if (i_reset) |
| r_hit_writes <= 0; |
| else if (f_axi_awr_nbursts > 3) |
| r_hit_writes <= 1; |
| |
| initial r_hit_reads = 0; |
| always @(posedge i_clk) |
| if (i_reset) |
| r_hit_reads <= 0; |
| else if (f_axi_rd_nbursts > 3) |
| r_hit_reads <= 1; |
| |
| always @(*) |
| begin |
| check_fault = 0; |
| if (!i_wb_cyc && o_axi_awvalid) |
| check_fault = 1; |
| if (!i_wb_cyc && o_axi_wvalid) |
| check_fault = 1; |
| if (!i_wb_cyc && f_axi_awr_nbursts > 0) |
| check_fault = 1; |
| if (!i_wb_cyc && i_axi_bvalid) |
| check_fault = 1; |
| // |
| if (!i_wb_cyc && o_axi_arvalid) |
| check_fault = 1; |
| if (!i_wb_cyc && f_axi_rd_outstanding > 0) |
| check_fault = 1; |
| if (!i_wb_cyc && i_axi_rvalid) |
| check_fault = 1; |
| if (!i_wb_cyc && (o_wb_ack | o_wb_err)) |
| check_fault = 1; |
| |
| if (flushing) |
| check_fault = 1; |
| end |
| |
| initial r_check_fault = 0; |
| always @(posedge i_clk) |
| if (i_reset) |
| r_check_fault <= 0; |
| else if (check_fault) |
| r_check_fault <= 1; |
| |
| always @(*) |
| cover(r_hit_writes && r_hit_reads && f_axi_rd_nbursts == 0 |
| && f_axi_awr_nbursts == 0 |
| && !o_axi_awvalid && !o_axi_arvalid && !o_axi_wvalid |
| && !i_axi_bvalid && !i_axi_rvalid |
| && !o_wb_ack && !o_wb_stall && !i_wb_stb |
| && !check_fault && !r_check_fault); |
| |
| // |
| // ... |
| // |
| |
| initial cvr_flushed = 1'b0; |
| always @(posedge i_clk) |
| if (i_reset) |
| cvr_flushed <= 1'b0; |
| else if (flushing) |
| cvr_flushed <= 1'b1; |
| |
| always @(*) |
| begin |
| cover(!i_reset && cvr_flushed && !flushing); |
| cover(!i_reset && cvr_flushed && !flushing && !o_wb_stall); |
| end |
| |
| // |
| // Let's cover our ability to turn around, from reads to writes or from |
| // writes to reads. |
| // |
| // Note that without the RMW option above, switching direction requires |
| // dropping i_wb_cyc. Let's just make certain here, that if we do so, |
| // we don't drop it until after all of the returns come back. |
| // |
| initial cvr_read2write = 0; |
| always @(posedge i_clk) |
| if (i_reset || (!i_wb_cyc && f_wb_nreqs != f_wb_nacks)) |
| cvr_read2write <= 0; |
| else if (!direction && !empty && m_we) |
| cvr_read2write <= 1; |
| |
| initial cvr_write2read = 0; |
| always @(posedge i_clk) |
| if (i_reset || (!i_wb_cyc && f_wb_nreqs != f_wb_nacks)) |
| cvr_write2read <= 0; |
| else if (direction && !empty && !m_we) |
| cvr_write2read <= 1; |
| |
| always @(*) |
| begin |
| cover(cvr_read2write && direction && o_wb_ack && f_wb_outstanding == 1); |
| cover(cvr_write2read && !direction && o_wb_ack && f_wb_outstanding == 1); |
| end |
| |
| reg [2:0] cvr_ack_after_abort; |
| |
| initial cvr_ack_after_abort = 0; |
| always @(posedge i_clk) |
| if (i_reset) |
| cvr_ack_after_abort <= 0; |
| else begin |
| if (!i_wb_cyc) |
| cvr_ack_after_abort[2:0] <= (empty) ? 0 : 3'b01; |
| if (cvr_ack_after_abort[0] && i_wb_cyc && r_stb && flushing) |
| cvr_ack_after_abort[1] <= 1; |
| if (o_wb_ack && &cvr_ack_after_abort[1:0]) |
| cvr_ack_after_abort[2] <= 1; |
| end |
| |
| always @(*) |
| cover(&cvr_ack_after_abort[1:0]); |
| always @(*) |
| cover(!flushing && (&cvr_ack_after_abort[1:0])); |
| always @(*) |
| cover(&cvr_ack_after_abort[2:0]); |
| always @(*) |
| cover(!i_wb_cyc && &cvr_ack_after_abort[2:0]); |
| |
| initial cvr_nwrites = 0; |
| always @(posedge i_clk) |
| if (i_reset || flushing || !i_wb_cyc || !i_wb_we || o_wb_err) |
| cvr_nwrites <= 0; |
| else if (i_axi_bvalid && o_axi_bready) |
| cvr_nwrites <= cvr_nwrites + 1; |
| |
| initial cvr_nreads = 0; |
| always @(posedge i_clk) |
| if (i_reset || flushing || !i_wb_cyc || i_wb_we || o_wb_err) |
| cvr_nreads <= 0; |
| else if (i_axi_rvalid && o_axi_rready) |
| cvr_nreads <= cvr_nreads + 1; |
| |
| always @(*) |
| cover(cvr_nwrites == 3 && !o_wb_ack && !o_wb_err && !i_wb_cyc); |
| |
| always @(*) |
| cover(cvr_nreads == 3 && !o_wb_ack && !o_wb_err && !i_wb_cyc); |
| |
| // |
| // Generate a cover that doesn't include an abort |
| // {{{ |
| (* anyconst *) reg f_never_abort; |
| |
| always @(*) |
| if (f_never_abort && f_wb_nacks != f_wb_nreqs) |
| assume(!i_reset && i_wb_cyc && !o_wb_err); |
| |
| always @(posedge i_clk) |
| if (f_never_abort && $past(o_wb_ack) && o_wb_ack) |
| assume($changed(o_wb_data)); |
| |
| always @(*) |
| cover(cvr_nreads == 3 && !o_wb_ack && !o_wb_err && !i_wb_cyc |
| && f_never_abort); |
| // }}} |
| |
| // }}} |
| `endif // FORMAL |
| // }}} |
| endmodule |