| Line 1... |
Line 1... |
|
`error This full featured AXI to WB converter does not (yet) work
|
////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////
|
//
|
//
|
// Filename: axim2wbsp.v
|
// Filename: axim2wbsp.v
|
//
|
//
|
// Project: Pipelined Wishbone to AXI converter
|
// Project: Pipelined Wishbone to AXI converter
|
//
|
//
|
// Purpose: So ... this converter works in the other direction. This
|
// Purpose: So ... this converter works in the other direction from
|
// converter takes AXI commands, and organizes them into pipelined
|
// wbm2axisp. This converter takes AXI commands, and organizes
|
// wishbone commands.
|
// them into pipelined wishbone commands.
|
//
|
//
|
//
|
//
|
// We'll treat AXI as two separate busses: one for writes, another for
|
// We'll treat AXI as two separate busses: one for writes, another for
|
// reads, further, we'll insist that the two channels AXI uses for writes
|
// reads, further, we'll insist that the two channels AXI uses for writes
|
// combine into one channel for our purposes.
|
// combine into one channel for our purposes.
|
| Line 17... |
Line 18... |
// Creator: Dan Gisselquist, Ph.D.
|
// Creator: Dan Gisselquist, Ph.D.
|
// Gisselquist Technology, LLC
|
// Gisselquist Technology, LLC
|
//
|
//
|
////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////
|
//
|
//
|
// Copyright (C) 2016, Gisselquist Technology, LLC
|
// Copyright (C) 2016-2019, Gisselquist Technology, LLC
|
//
|
//
|
// This program is free software (firmware): you can redistribute it and/or
|
// This file is part of the pipelined Wishbone to AXI converter project, a
|
// modify it under the terms of the GNU General Public License as published
|
// project that contains multiple bus bridging designs and formal bus property
|
// by the Free Software Foundation, either version 3 of the License, or (at
|
// sets.
|
// your option) any later version.
|
//
|
//
|
// The bus bridge designs and property sets are free RTL designs: you can
|
// This program is distributed in the hope that it will be useful, but WITHOUT
|
// redistribute them and/or modify any of them under the terms of the GNU
|
// ANY WARRANTY; without even the implied warranty of MERCHANTIBILITY or
|
// Lesser General Public License as published by the Free Software Foundation,
|
// FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
|
// either version 3 of the License, or (at your option) any later version.
|
// for more details.
|
//
|
//
|
// The bus bridge designs and property sets are distributed in the hope that
|
// You should have received a copy of the GNU General Public License along
|
// they will be useful, but WITHOUT ANY WARRANTY; without even the implied
|
// with this program. (It's in the $(ROOT)/doc directory, run make with no
|
// warranty of MERCHANTIBILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
|
// target there if the PDF file isn't present.) If not, see
|
// 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.
|
// <http://www.gnu.org/licenses/> for a copy.
|
//
|
//
|
// License: GPL, v3, as defined and found on www.gnu.org,
|
// License: LGPL, v3, as defined and found on www.gnu.org,
|
// http://www.gnu.org/licenses/gpl.html
|
// http://www.gnu.org/licenses/lgpl.html
|
//
|
|
//
|
//
|
////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////
|
//
|
//
|
//
|
//
|
|
`default_nettype none
|
|
//
|
module axim2wbsp( i_clk, i_axi_reset_n,
|
module axim2wbsp( i_clk, i_axi_reset_n,
|
//
|
//
|
o_axi_awready, // Slave is ready to accept
|
o_axi_awready, // Slave is ready to accept
|
i_axi_awid, i_axi_awaddr, i_axi_awlen, i_axi_awsize, i_axi_awburst,
|
i_axi_awid, i_axi_awaddr, i_axi_awlen, i_axi_awsize, i_axi_awburst,
|
i_axi_awlock, i_axi_awcache, i_axi_awprot, i_axi_awqos, i_axi_awvalid,
|
i_axi_awlock, i_axi_awcache, i_axi_awprot, i_axi_awqos, i_axi_awvalid,
|
| Line 73... |
Line 79... |
i_axi_rready, // Read Response ready
|
i_axi_rready, // Read Response ready
|
// Wishbone interface
|
// Wishbone interface
|
o_reset, o_wb_cyc, o_wb_stb, o_wb_we, o_wb_addr, o_wb_data, o_wb_sel,
|
o_reset, o_wb_cyc, o_wb_stb, o_wb_we, o_wb_addr, o_wb_data, o_wb_sel,
|
i_wb_ack, i_wb_stall, i_wb_data, i_wb_err);
|
i_wb_ack, i_wb_stall, i_wb_data, i_wb_err);
|
//
|
//
|
parameter C_AXI_ID_WIDTH = 6; // The AXI id width used for R&W
|
parameter C_AXI_ID_WIDTH = 2; // The AXI id width used for R&W
|
// This is an int between 1-16
|
// This is an int between 1-16
|
parameter C_AXI_DATA_WIDTH = 32;// Width of the AXI R&W data
|
parameter C_AXI_DATA_WIDTH = 32;// Width of the AXI R&W data
|
parameter C_AXI_ADDR_WIDTH = 28; // AXI Address width
|
parameter C_AXI_ADDR_WIDTH = 28; // AXI Address width
|
localparam DW = C_AXI_DATA_WIDTH;
|
localparam DW = C_AXI_DATA_WIDTH;
|
localparam AW = (C_AXI_DATA_WIDTH== 8) ? (C_AXI_ADDR_WIDTH)
|
localparam AW = (C_AXI_DATA_WIDTH== 8) ? (C_AXI_ADDR_WIDTH)
|
:((C_AXI_DATA_WIDTH== 16) ? (C_AXI_ADDR_WIDTH-1)
|
:((C_AXI_DATA_WIDTH== 16) ? (C_AXI_ADDR_WIDTH-1)
|
:((C_AXI_DATA_WIDTH== 32) ? (C_AXI_ADDR_WIDTH-2)
|
:((C_AXI_DATA_WIDTH== 32) ? (C_AXI_ADDR_WIDTH-2)
|
:((C_AXI_DATA_WIDTH== 64) ? (C_AXI_ADDR_WIDTH-3)
|
:((C_AXI_DATA_WIDTH== 64) ? (C_AXI_ADDR_WIDTH-3)
|
:((C_AXI_DATA_WIDTH==128) ? (C_AXI_ADDR_WIDTH-4)
|
:((C_AXI_DATA_WIDTH==128) ? (C_AXI_ADDR_WIDTH-4)
|
:(C_AXI_ADDR_WIDTH-5)))));
|
:(C_AXI_ADDR_WIDTH-5)))));
|
|
parameter LGFIFO = 4;
|
|
parameter [0:0] F_STRICT_ORDER = 0;
|
|
parameter [0:0] F_CONSECUTIVE_IDS = 0;
|
|
parameter [0:0] F_OPT_BURSTS = 1'b0;
|
|
parameter [0:0] F_OPT_CLK2FFLOGIC = 1'b0;
|
|
parameter F_MAXSTALL = 3;
|
|
parameter F_MAXDELAY = 3;
|
|
parameter [0:0] OPT_READONLY = 1'b1;
|
|
parameter [0:0] OPT_WRITEONLY = 1'b0;
|
|
parameter [7:0] OPT_MAXBURST = 8'h3;
|
//
|
//
|
input wire i_clk; // System clock
|
input wire i_clk; // System clock
|
input wire i_axi_reset_n;
|
input wire i_axi_reset_n;
|
|
|
// AXI write address channel signals
|
// AXI write address channel signals
|
| Line 167... |
Line 183... |
|
|
assign r_wb_we = 1'b0;
|
assign r_wb_we = 1'b0;
|
assign w_wb_we = 1'b1;
|
assign w_wb_we = 1'b1;
|
// verilator lint_on UNUSED
|
// verilator lint_on UNUSED
|
|
|
|
`ifdef FORMAL
|
|
wire [(LGFIFO-1):0] f_wr_fifo_ahead, f_wr_fifo_dhead,
|
|
f_wr_fifo_neck, f_wr_fifo_torso,
|
|
f_wr_fifo_tail,
|
|
f_rd_fifo_head, f_rd_fifo_neck,
|
|
f_rd_fifo_torso, f_rd_fifo_tail;
|
|
wire [(LGFIFO-1):0] f_wb_nreqs, f_wb_nacks,
|
|
f_wb_outstanding;
|
|
wire [(LGFIFO-1):0] f_wb_wr_nreqs, f_wb_wr_nacks,
|
|
f_wb_wr_outstanding;
|
|
wire [(LGFIFO-1):0] f_wb_rd_nreqs, f_wb_rd_nacks,
|
|
f_wb_rd_outstanding;
|
|
`endif
|
|
|
|
generate if (!OPT_READONLY)
|
|
begin : AXI_WR
|
aximwr2wbsp #(
|
aximwr2wbsp #(
|
.C_AXI_ID_WIDTH(C_AXI_ID_WIDTH),
|
.C_AXI_ID_WIDTH(C_AXI_ID_WIDTH),
|
.C_AXI_DATA_WIDTH(C_AXI_DATA_WIDTH),
|
.C_AXI_DATA_WIDTH(C_AXI_DATA_WIDTH),
|
.C_AXI_ADDR_WIDTH(C_AXI_ADDR_WIDTH), .AW(AW))
|
.C_AXI_ADDR_WIDTH(C_AXI_ADDR_WIDTH), .AW(AW),
|
|
.LGFIFO(LGFIFO))
|
axi_write_decoder(
|
axi_write_decoder(
|
.i_axi_clk(i_clk), .i_axi_reset_n(i_axi_reset_n),
|
.i_axi_clk(i_clk), .i_axi_reset_n(i_axi_reset_n),
|
//
|
//
|
.o_axi_awready(o_axi_awready),
|
.o_axi_awready(o_axi_awready),
|
.i_axi_awid( i_axi_awid),
|
.i_axi_awid( i_axi_awid),
|
| Line 204... |
Line 237... |
.o_wb_addr( w_wb_addr),
|
.o_wb_addr( w_wb_addr),
|
.o_wb_data( w_wb_data),
|
.o_wb_data( w_wb_data),
|
.o_wb_sel( w_wb_sel),
|
.o_wb_sel( w_wb_sel),
|
.i_wb_ack( w_wb_ack),
|
.i_wb_ack( w_wb_ack),
|
.i_wb_stall(w_wb_stall),
|
.i_wb_stall(w_wb_stall),
|
.i_wb_err( w_wb_err));
|
.i_wb_err( w_wb_err)
|
|
`ifdef FORMAL
|
|
,
|
|
.f_fifo_ahead(f_wr_fifo_ahead),
|
|
.f_fifo_dhead(f_wr_fifo_dhead),
|
|
.f_fifo_neck( f_wr_fifo_neck),
|
|
.f_fifo_torso(f_wr_fifo_torso),
|
|
.f_fifo_tail( f_wr_fifo_tail)
|
|
`endif
|
|
);
|
|
end else begin
|
|
assign w_wb_cyc = 0;
|
|
assign w_wb_stb = 0;
|
|
assign w_wb_addr = 0;
|
|
assign w_wb_data = 0;
|
|
assign w_wb_sel = 0;
|
|
assign o_axi_awready = 0;
|
|
assign o_axi_wready = 0;
|
|
assign o_axi_bvalid = (i_axi_wvalid)&&(i_axi_wlast);
|
|
assign o_axi_bresp = 2'b11;
|
|
assign o_axi_bid = i_axi_awid;
|
|
`ifdef FORMAL
|
|
assign f_wr_fifo_ahead = 0;
|
|
assign f_wr_fifo_dhead = 0;
|
|
assign f_wr_fifo_neck = 0;
|
|
assign f_wr_fifo_torso = 0;
|
|
assign f_wr_fifo_tail = 0;
|
|
`endif
|
|
end endgenerate
|
assign w_wb_we = 1'b1;
|
assign w_wb_we = 1'b1;
|
|
|
|
generate if (!OPT_WRITEONLY)
|
|
begin : AXI_RD
|
aximrd2wbsp #(
|
aximrd2wbsp #(
|
.C_AXI_ID_WIDTH(C_AXI_ID_WIDTH),
|
.C_AXI_ID_WIDTH(C_AXI_ID_WIDTH),
|
.C_AXI_DATA_WIDTH(C_AXI_DATA_WIDTH),
|
.C_AXI_DATA_WIDTH(C_AXI_DATA_WIDTH),
|
.C_AXI_ADDR_WIDTH(C_AXI_ADDR_WIDTH), .AW(AW))
|
.C_AXI_ADDR_WIDTH(C_AXI_ADDR_WIDTH), .AW(AW),
|
|
.LGFIFO(LGFIFO))
|
axi_read_decoder(
|
axi_read_decoder(
|
.i_axi_clk(i_clk), .i_axi_reset_n(i_axi_reset_n),
|
.i_axi_clk(i_clk), .i_axi_reset_n(i_axi_reset_n),
|
//
|
//
|
.o_axi_arready(o_axi_arready),
|
.o_axi_arready(o_axi_arready),
|
.i_axi_arid( i_axi_arid),
|
.i_axi_arid( i_axi_arid),
|
| Line 239... |
Line 303... |
.o_wb_stb( r_wb_stb),
|
.o_wb_stb( r_wb_stb),
|
.o_wb_addr( r_wb_addr),
|
.o_wb_addr( r_wb_addr),
|
.i_wb_ack( r_wb_ack),
|
.i_wb_ack( r_wb_ack),
|
.i_wb_stall(r_wb_stall),
|
.i_wb_stall(r_wb_stall),
|
.i_wb_data( i_wb_data),
|
.i_wb_data( i_wb_data),
|
.i_wb_err( r_wb_err));
|
.i_wb_err( r_wb_err)
|
|
`ifdef FORMAL
|
|
,
|
|
.f_fifo_head(f_rd_fifo_head),
|
|
.f_fifo_neck(f_rd_fifo_neck),
|
|
.f_fifo_torso(f_rd_fifo_torso),
|
|
.f_fifo_tail(f_rd_fifo_tail)
|
|
`endif
|
|
);
|
|
end else begin
|
|
assign r_wb_cyc = 0;
|
|
assign r_wb_stb = 0;
|
|
assign r_wb_addr = 0;
|
|
//
|
|
assign o_axi_arready = 1'b1;
|
|
assign o_axi_rvalid = (i_axi_arvalid)&&(o_axi_arready);
|
|
assign o_axi_rid = (i_axi_arid);
|
|
assign o_axi_rvalid = (i_axi_arvalid);
|
|
assign o_axi_rlast = (i_axi_arvalid);
|
|
assign o_axi_rresp = (i_axi_arvalid) ? 2'b11 : 2'b00;
|
|
assign o_axi_rdata = 0;
|
|
`ifdef FORMAL
|
|
assign f_rd_fifo_head = 0;
|
|
assign f_rd_fifo_neck = 0;
|
|
assign f_rd_fifo_torso = 0;
|
|
assign f_rd_fifo_tail = 0;
|
|
`endif
|
|
end endgenerate
|
|
|
|
generate if (OPT_READONLY)
|
|
begin : ARB_RD
|
|
assign o_wb_cyc = r_wb_cyc;
|
|
assign o_wb_stb = r_wb_stb;
|
|
assign o_wb_we = 1'b0;
|
|
assign o_wb_addr = r_wb_addr;
|
|
assign o_wb_data = 32'h0;
|
|
assign o_wb_sel = 0;
|
|
assign r_wb_ack = i_wb_ack;
|
|
assign r_wb_stall= i_wb_stall;
|
|
assign r_wb_ack = i_wb_ack;
|
|
assign r_wb_err = i_wb_err;
|
|
|
|
`ifdef FORMAL
|
|
fwb_master #(.DW(DW), .AW(AW),
|
|
.F_LGDEPTH(LGFIFO),
|
|
.F_MAX_STALL(F_MAXSTALL),
|
|
.F_MAX_ACK_DELAY(F_MAXDELAY),
|
|
.F_OPT_CLK2FFLOGIC(F_OPT_CLK2FFLOGIC))
|
|
f_wb(i_clk, !i_axi_reset_n,
|
|
o_wb_cyc, o_wb_stb, o_wb_we, o_wb_addr, o_wb_data,
|
|
o_wb_sel,
|
|
i_wb_ack, i_wb_stall, i_wb_data, i_wb_err,
|
|
f_wb_nreqs, f_wb_nacks, f_wb_outstanding);
|
|
|
|
assign f_wb_rd_nreqs = f_wb_nreqs;
|
|
assign f_wb_rd_nacks = f_wb_nacks;
|
|
assign f_wb_rd_outstanding = f_wb_outstanding;
|
|
`endif
|
|
end else if (OPT_WRITEONLY)
|
|
begin : ARB_WR
|
|
assign o_wb_cyc = w_wb_cyc;
|
|
assign o_wb_stb = w_wb_stb;
|
|
assign o_wb_we = 1'b1;
|
|
assign o_wb_addr = w_wb_addr;
|
|
assign o_wb_data = w_wb_data;
|
|
assign o_wb_sel = w_wb_sel;
|
|
assign w_wb_ack = i_wb_ack;
|
|
assign w_wb_stall= i_wb_stall;
|
|
assign w_wb_ack = i_wb_ack;
|
|
assign w_wb_err = i_wb_err;
|
|
|
wbarbiter #(
|
|
`ifdef FORMAL
|
`ifdef FORMAL
|
.F_LGDEPTH(C_AXI_DATA_WIDTH),
|
fwb_master #(.DW(DW), .AW(AW),
|
|
.F_LGDEPTH(LGFIFO),
|
|
.F_MAX_STALL(F_MAXSTALL),
|
|
.F_MAX_ACK_DELAY(F_MAXDELAY))
|
|
f_wb(i_clk, !i_axi_reset_n,
|
|
o_wb_cyc, o_wb_stb, o_wb_we, o_wb_addr, o_wb_data,
|
|
o_wb_sel,
|
|
i_wb_ack, i_wb_stall, i_wb_data, i_wb_err,
|
|
f_wb_nreqs, f_wb_nacks, f_wb_outstanding);
|
|
|
|
assign f_wb_wr_nreqs = f_wb_nreqs;
|
|
assign f_wb_wr_nacks = f_wb_nacks;
|
|
assign f_wb_wr_outstanding = f_wb_outstanding;
|
`endif
|
`endif
|
.DW(C_AXI_DATA_WIDTH),
|
end else begin : ARB_WB
|
.AW(AW))
|
wbarbiter #(.DW(DW), .AW(AW),
|
|
.F_LGDEPTH(LGFIFO),
|
|
.F_MAX_STALL(F_MAXSTALL),
|
|
.F_OPT_CLK2FFLOGIC(F_OPT_CLK2FFLOGIC),
|
|
.F_MAX_ACK_DELAY(F_MAXDELAY))
|
readorwrite(i_clk, !i_axi_reset_n,
|
readorwrite(i_clk, !i_axi_reset_n,
|
r_wb_cyc, r_wb_stb, 1'b0, r_wb_addr, w_wb_data, w_wb_sel,
|
r_wb_cyc, r_wb_stb, 1'b0, r_wb_addr, w_wb_data, w_wb_sel,
|
r_wb_ack, r_wb_stall, r_wb_err,
|
r_wb_ack, r_wb_stall, r_wb_err,
|
w_wb_cyc, w_wb_stb, 1'b1, w_wb_addr, w_wb_data, w_wb_sel,
|
w_wb_cyc, w_wb_stb, 1'b1, w_wb_addr, w_wb_data, w_wb_sel,
|
w_wb_ack, w_wb_stall, w_wb_err,
|
w_wb_ack, w_wb_stall, w_wb_err,
|
o_wb_cyc, o_wb_stb, o_wb_we, o_wb_addr, o_wb_data, o_wb_sel,
|
o_wb_cyc, o_wb_stb, o_wb_we, o_wb_addr, o_wb_data, o_wb_sel,
|
i_wb_ack, i_wb_stall, i_wb_err);
|
i_wb_ack, i_wb_stall, i_wb_err
|
|
`ifdef FORMAL
|
|
,
|
|
f_wb_rd_nreqs, f_wb_rd_nacks, f_wb_rd_outstanding,
|
|
f_wb_wr_nreqs, f_wb_wr_nacks, f_wb_wr_outstanding,
|
|
f_wb_nreqs, f_wb_nacks, f_wb_outstanding
|
|
`endif
|
|
);
|
|
end endgenerate
|
|
|
assign o_reset = (i_axi_reset_n == 1'b0);
|
assign o_reset = (i_axi_reset_n == 1'b0);
|
|
|
`ifdef FORMAL
|
`ifdef FORMAL
|
|
|
`ifdef AXIM2WBSP
|
`ifdef AXIM2WBSP
|
|
generate if (F_OPT_CLK2FFLOGIC)
|
|
begin
|
reg f_last_clk;
|
reg f_last_clk;
|
|
|
initial f_last_clk = 0;
|
initial f_last_clk = 0;
|
always @($global_clock)
|
always @($global_clock)
|
begin
|
begin
|
assume(i_clk == f_last_clk);
|
assume(i_clk == f_last_clk);
|
f_last_clk <= !f_last_clk;
|
f_last_clk <= !f_last_clk;
|
|
|
|
if ((f_past_valid)&&(!$rose(i_clk)))
|
|
assume($stable(i_axi_reset_n));
|
end
|
end
|
|
end endgenerate
|
`else
|
`else
|
`endif
|
`endif
|
|
|
reg f_past_valid;
|
reg f_past_valid;
|
|
|
initial f_past_valid = 1'b0;
|
initial f_past_valid = 1'b0;
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
f_past_valid = 1'b1;
|
f_past_valid = 1'b1;
|
|
|
|
initial assume(!i_axi_reset_n);
|
|
always @(*)
|
|
if (!f_past_valid)
|
|
assume(!i_axi_reset_n);
|
|
|
|
generate if (F_OPT_CLK2FFLOGIC)
|
|
begin
|
|
|
|
always @($global_clock)
|
|
if ((f_past_valid)&&(!$rose(i_clk)))
|
|
assert($stable(i_axi_reset_n));
|
|
end endgenerate
|
|
|
wire [(C_AXI_ID_WIDTH-1):0] f_axi_rd_outstanding,
|
wire [(C_AXI_ID_WIDTH-1):0] f_axi_rd_outstanding,
|
f_axi_wr_outstanding,
|
f_axi_wr_outstanding,
|
f_axi_awr_outstanding;
|
f_axi_awr_outstanding;
|
wire [((1<<C_AXI_ID_WIDTH)-1):0] f_axi_rd_id_outstanding,
|
wire [((1<<C_AXI_ID_WIDTH)-1):0] f_axi_rd_id_outstanding,
|
f_axi_awr_id_outstanding,
|
f_axi_awr_id_outstanding,
|
f_axi_wr_id_outstanding;
|
f_axi_wr_id_outstanding;
|
wire [(C_AXI_ID_WIDTH-1):0] f_wb_nreqs,
|
wire [8:0] f_axi_wr_pending,
|
f_wb_nacks, f_wb_outstanding;
|
f_axi_rd_count,
|
wire [(C_AXI_ID_WIDTH-1):0] f_wb_wr_nreqs,
|
f_axi_wr_count;
|
f_wb_wr_nacks, f_wb_wr_outstanding;
|
|
wire [(C_AXI_ID_WIDTH-1):0] f_wb_rd_nreqs,
|
/*
|
f_wb_rd_nacks, f_wb_rd_outstanding;
|
generate if (!OPT_READONLY)
|
|
begin : F_WB_WRITE
|
fwb_slave #(.DW(DW), .AW(AW),
|
fwb_slave #(.DW(DW), .AW(AW),
|
.F_MAX_STALL(0),
|
.F_MAX_STALL(0),
|
.F_MAX_ACK_DELAY(0),
|
.F_MAX_ACK_DELAY(0),
|
.F_LGDEPTH(C_AXI_ID_WIDTH),
|
.F_LGDEPTH(C_AXI_ID_WIDTH),
|
.F_OPT_RMW_BUS_OPTION(1),
|
.F_OPT_RMW_BUS_OPTION(1),
|
.F_OPT_DISCONTINUOUS(1))
|
.F_OPT_DISCONTINUOUS(1))
|
f_wb_wr(i_clk, !i_axi_reset_n,
|
f_wb_wr(i_clk, !i_axi_reset_n,
|
w_wb_cyc, w_wb_stb, w_wb_we, w_wb_addr, w_wb_data,
|
w_wb_cyc, w_wb_stb, w_wb_we, w_wb_addr, w_wb_data,
|
w_wb_sel,
|
w_wb_sel,
|
w_wb_ack, w_wb_stall, i_wb_data, w_wb_err,
|
w_wb_ack, w_wb_stall, i_wb_data, w_wb_err,
|
f_wb_wr_nreqs, f_wb_wr_nacks, f_wb_wr_outstanding);
|
f_wb_wr_nreqs, f_wb_wr_nacks, f_wb_wr_outstanding);
|
|
end else begin
|
fwb_slave #(.DW(DW), .AW(AW),
|
assign f_wb_wr_nreqs = 0;
|
.F_MAX_STALL(0),
|
assign f_wb_wr_nacks = 0;
|
.F_MAX_ACK_DELAY(0),
|
assign f_wb_wr_outstanding = 0;
|
.F_LGDEPTH(C_AXI_ID_WIDTH),
|
end endgenerate
|
.F_OPT_RMW_BUS_OPTION(1),
|
*/
|
.F_OPT_DISCONTINUOUS(1))
|
|
f_wb_rd(i_clk, !i_axi_reset_n,
|
/*
|
r_wb_cyc, r_wb_stb, r_wb_we, r_wb_addr, w_wb_data, w_wb_sel,
|
generate if (!OPT_WRITEONLY)
|
r_wb_ack, r_wb_stall, i_wb_data, r_wb_err,
|
begin : F_WB_READ
|
f_wb_rd_nreqs, f_wb_rd_nacks, f_wb_rd_outstanding);
|
fwb_slave #(.DW(DW), .AW(AW),
|
|
.F_MAX_STALL(0),
|
fwb_master #(.DW(DW), .AW(AW),
|
.F_MAX_ACK_DELAY(0),
|
.F_MAX_STALL(3),
|
.F_LGDEPTH(C_AXI_ID_WIDTH),
|
.F_MAX_ACK_DELAY(3),
|
.F_OPT_RMW_BUS_OPTION(1),
|
.F_LGDEPTH(C_AXI_ID_WIDTH))
|
.F_OPT_DISCONTINUOUS(1))
|
f_wb(i_clk, !i_axi_reset_n,
|
f_wb_rd(i_clk, !i_axi_reset_n,
|
o_wb_cyc, o_wb_stb, o_wb_we, o_wb_addr, o_wb_data,
|
r_wb_cyc, r_wb_stb, r_wb_we, r_wb_addr, w_wb_data, w_wb_sel,
|
o_wb_sel,
|
r_wb_ack, r_wb_stall, i_wb_data, r_wb_err,
|
i_wb_ack, i_wb_stall, i_wb_data, i_wb_err,
|
f_wb_rd_nreqs, f_wb_rd_nacks, f_wb_rd_outstanding);
|
f_wb_nreqs, f_wb_nacks, f_wb_outstanding);
|
end else begin
|
|
assign f_wb_rd_nreqs = 0;
|
always @(*)
|
assign f_wb_rd_nacks = 0;
|
assume(i_axi_awlen < 8'h4);
|
assign f_wb_rd_outstanding = 0;
|
|
end endgenerate
|
always @(*)
|
*/
|
assume(i_axi_arlen < 8'h4);
|
|
|
/*
|
always @(*)
|
fwb_master #(.DW(DW), .AW(AW),
|
assume(i_axi_arvalid == 0);
|
.F_MAX_STALL(F_MAXSTALL),
|
|
.F_MAX_ACK_DELAY(F_MAXDELAY),
|
|
.F_LGDEPTH(C_AXI_ID_WIDTH))
|
|
f_wb(i_clk, !i_axi_reset_n,
|
|
o_wb_cyc, o_wb_stb, o_wb_we, o_wb_addr, o_wb_data,
|
|
o_wb_sel,
|
|
i_wb_ack, i_wb_stall, i_wb_data, i_wb_err,
|
|
f_wb_nreqs, f_wb_nacks, f_wb_outstanding);
|
|
*/
|
|
|
faxi_slave #(
|
faxi_slave #(
|
.C_AXI_ID_WIDTH(C_AXI_ID_WIDTH),
|
.C_AXI_ID_WIDTH(C_AXI_ID_WIDTH),
|
.C_AXI_DATA_WIDTH(C_AXI_DATA_WIDTH),
|
.C_AXI_DATA_WIDTH(C_AXI_DATA_WIDTH),
|
.C_AXI_ADDR_WIDTH(C_AXI_ADDR_WIDTH),
|
.C_AXI_ADDR_WIDTH(C_AXI_ADDR_WIDTH),
|
.F_AXI_MAXSTALL(0),
|
.F_AXI_MAXSTALL(0),
|
.F_AXI_MAXDELAY(0))
|
.F_AXI_MAXDELAY(0),
|
|
.F_AXI_MAXBURST(OPT_MAXBURST),
|
|
.F_OPT_CLK2FFLOGIC(F_OPT_CLK2FFLOGIC))
|
f_axi(.i_clk(i_clk), .i_axi_reset_n(i_axi_reset_n),
|
f_axi(.i_clk(i_clk), .i_axi_reset_n(i_axi_reset_n),
|
// AXI write address channnel
|
// AXI write address channnel
|
.i_axi_awready(o_axi_awready),
|
.i_axi_awready(o_axi_awready),
|
.i_axi_awid( i_axi_awid),
|
.i_axi_awid( i_axi_awid),
|
.i_axi_awaddr( i_axi_awaddr),
|
.i_axi_awaddr( i_axi_awaddr),
|
| Line 358... |
Line 543... |
.i_axi_wdata( i_axi_wdata),
|
.i_axi_wdata( i_axi_wdata),
|
.i_axi_wstrb( i_axi_wstrb),
|
.i_axi_wstrb( i_axi_wstrb),
|
.i_axi_wlast( i_axi_wlast),
|
.i_axi_wlast( i_axi_wlast),
|
.i_axi_wvalid( i_axi_wvalid),
|
.i_axi_wvalid( i_axi_wvalid),
|
// AXI write acknowledgement channel
|
// AXI write acknowledgement channel
|
.i_axi_bid( o_axi_bid), // Response ID
|
.i_axi_bid( o_axi_bid),
|
.i_axi_bresp( o_axi_bresp), // Write response
|
.i_axi_bresp( o_axi_bresp),
|
.i_axi_bvalid(o_axi_bvalid), // Write reponse valid
|
.i_axi_bvalid(o_axi_bvalid),
|
.i_axi_bready(i_axi_bready), // Response ready
|
.i_axi_bready(i_axi_bready),
|
// AXI read address channel
|
// AXI read address channel
|
.i_axi_arready(o_axi_arready), // Read address ready
|
.i_axi_arready(o_axi_arready),
|
.i_axi_arid( i_axi_arid), // Read ID
|
.i_axi_arid( i_axi_arid),
|
.i_axi_araddr( i_axi_araddr), // Read address
|
.i_axi_araddr( i_axi_araddr),
|
.i_axi_arlen( i_axi_arlen), // Read Burst Length
|
.i_axi_arlen( i_axi_arlen),
|
.i_axi_arsize( i_axi_arsize), // Read Burst size
|
.i_axi_arsize( i_axi_arsize),
|
.i_axi_arburst(i_axi_arburst), // Read Burst type
|
.i_axi_arburst(i_axi_arburst),
|
.i_axi_arlock( i_axi_arlock), // Read lock type
|
.i_axi_arlock( i_axi_arlock),
|
.i_axi_arcache(i_axi_arcache), // Read Cache type
|
.i_axi_arcache(i_axi_arcache),
|
.i_axi_arprot( i_axi_arprot), // Read Protection type
|
.i_axi_arprot( i_axi_arprot),
|
.i_axi_arqos( i_axi_arqos), // Read Protection type
|
.i_axi_arqos( i_axi_arqos),
|
.i_axi_arvalid(i_axi_arvalid), // Read address valid
|
.i_axi_arvalid(i_axi_arvalid),
|
// AXI read data return
|
// AXI read data return
|
.i_axi_rid( o_axi_rid), // Response ID
|
.i_axi_rid( o_axi_rid),
|
.i_axi_rresp( o_axi_rresp), // Read response
|
.i_axi_rresp( o_axi_rresp),
|
.i_axi_rvalid( o_axi_rvalid), // Read reponse valid
|
.i_axi_rvalid( o_axi_rvalid),
|
.i_axi_rdata( o_axi_rdata), // Read data
|
.i_axi_rdata( o_axi_rdata),
|
.i_axi_rlast( o_axi_rlast), // Read last
|
.i_axi_rlast( o_axi_rlast),
|
.i_axi_rready( i_axi_rready), // Read Response ready
|
.i_axi_rready( i_axi_rready),
|
// Quantify where we are within a transaction
|
// Quantify where we are within a transaction
|
.f_axi_rd_outstanding( f_axi_rd_outstanding),
|
.f_axi_rd_outstanding( f_axi_rd_outstanding),
|
.f_axi_wr_outstanding( f_axi_wr_outstanding),
|
.f_axi_wr_outstanding( f_axi_wr_outstanding),
|
.f_axi_awr_outstanding(f_axi_awr_outstanding),
|
.f_axi_awr_outstanding(f_axi_awr_outstanding),
|
.f_axi_rd_id_outstanding(f_axi_rd_id_outstanding),
|
.f_axi_rd_id_outstanding(f_axi_rd_id_outstanding),
|
.f_axi_awr_id_outstanding(f_axi_awr_id_outstanding),
|
.f_axi_awr_id_outstanding(f_axi_awr_id_outstanding),
|
.f_axi_wr_id_outstanding(f_axi_wr_id_outstanding));
|
.f_axi_wr_id_outstanding(f_axi_wr_id_outstanding),
|
|
.f_axi_wr_pending(f_axi_wr_pending),
|
|
.f_axi_rd_count(f_axi_rd_count),
|
|
.f_axi_wr_count(f_axi_wr_count));
|
|
|
|
wire f_axi_ard_req, f_axi_awr_req, f_axi_wr_req,
|
|
f_axi_rd_ack, f_axi_wr_ack;
|
|
|
|
assign f_axi_ard_req = (i_axi_arvalid)&&(o_axi_arready);
|
|
assign f_axi_awr_req = (i_axi_awvalid)&&(o_axi_awready);
|
|
assign f_axi_wr_req = (i_axi_wvalid)&&(o_axi_wready);
|
|
assign f_axi_wr_ack = (o_axi_bvalid)&&(i_axi_bready);
|
|
assign f_axi_rd_ack = (o_axi_rvalid)&&(i_axi_rready);
|
|
|
|
wire [(LGFIFO-1):0] f_awr_fifo_axi_used,
|
|
f_dwr_fifo_axi_used,
|
|
f_rd_fifo_axi_used,
|
|
f_wr_fifo_wb_outstanding,
|
|
f_rd_fifo_wb_outstanding;
|
|
|
|
assign f_awr_fifo_axi_used = f_wr_fifo_ahead - f_wr_fifo_tail;
|
|
assign f_dwr_fifo_axi_used = f_wr_fifo_dhead - f_wr_fifo_tail;
|
|
assign f_rd_fifo_axi_used = f_rd_fifo_head - f_rd_fifo_tail;
|
|
assign f_wr_fifo_wb_outstanding = f_wr_fifo_neck - f_wr_fifo_torso;
|
|
assign f_rd_fifo_wb_outstanding = f_rd_fifo_neck - f_rd_fifo_torso;
|
|
|
|
// The number of outstanding requests must always be greater than
|
|
// the number of AXI requests creating them--since the AXI requests
|
|
// may be burst requests.
|
|
//
|
|
always @(*)
|
|
if (OPT_READONLY)
|
|
begin
|
|
assert(f_axi_awr_outstanding == 0);
|
|
assert(f_axi_wr_outstanding == 0);
|
|
assert(f_axi_awr_id_outstanding == 0);
|
|
assert(f_axi_wr_id_outstanding == 0);
|
|
assert(f_axi_wr_pending == 0);
|
|
assert(f_axi_wr_count == 0);
|
|
end else begin
|
|
assert(f_awr_fifo_axi_used >= f_axi_awr_outstanding);
|
|
assert(f_dwr_fifo_axi_used >= f_axi_wr_outstanding);
|
|
assert(f_wr_fifo_ahead >= f_axi_awr_outstanding);
|
|
end
|
|
|
|
/*
|
|
always @(*)
|
|
assert((!w_wb_cyc)
|
|
||(f_wr_fifo_wb_outstanding
|
|
// -(((w_wb_stall)&&(w_wb_stb))? 1'b1:1'b0)
|
|
+(((w_wb_ack)&&(w_wb_err))? 1'b1:1'b0)
|
|
== f_wb_wr_outstanding));
|
|
*/
|
|
|
|
wire f_r_wb_req, f_r_wb_ack, f_r_wb_stall;
|
|
assign f_r_wb_req = (r_wb_stb)&&(!r_wb_stall);
|
|
assign f_r_wb_ack = (r_wb_cyc)&&((r_wb_ack)||(r_wb_err));
|
|
assign f_r_wb_stall=(r_wb_stb)&&(r_wb_stall);
|
|
|
|
/*
|
|
always @(*)
|
|
if ((i_axi_reset_n)&&(r_wb_cyc))
|
|
assert(f_rd_fifo_wb_outstanding
|
|
// -((f_r_wb_req)? 1'b1:1'b0)
|
|
-((r_wb_stb)? 1'b1:1'b0)
|
|
//+(((f_r_wb_ack)&&(!f_r_wb_req))? 1'b1:1'b0)
|
|
== f_wb_rd_outstanding);
|
|
*/
|
|
|
|
|
|
//
|
|
assert property((!OPT_READONLY)||(!OPT_WRITEONLY));
|
|
|
|
always @(*)
|
|
if (OPT_READONLY)
|
|
begin
|
|
assume(i_axi_awvalid == 0);
|
|
assume(i_axi_wvalid == 0);
|
|
end
|
|
always @(*)
|
|
if (OPT_WRITEONLY)
|
|
assume(i_axi_arvalid == 0);
|
|
|
|
always @(*)
|
|
if (i_axi_awvalid)
|
|
assume(i_axi_awburst[1] == 1'b0);
|
|
always @(*)
|
|
if (i_axi_arvalid)
|
|
assume(i_axi_arburst[1] == 1'b0);
|
|
|
|
always @(*)
|
|
if (F_OPT_BURSTS)
|
|
begin
|
|
assume((!i_axi_arvalid)||(i_axi_arlen<= OPT_MAXBURST));
|
|
assume((!i_axi_awvalid)||(i_axi_awlen<= OPT_MAXBURST));
|
|
end else begin
|
|
assume((!i_axi_arvalid)||(i_axi_arlen == 0));
|
|
assume((!i_axi_awvalid)||(i_axi_awlen == 0));
|
|
end
|
|
|
`endif
|
`endif
|
endmodule
|
endmodule
|
|
|
|
|
No newline at end of file
|
No newline at end of file
|
