| Line 1... |
Line 1... |
////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////
|
//
|
//
|
// Filename: wbm2axisp.v
|
// Filename: wbm2axisp.v (Wishbone master to AXI slave, pipelined)
|
//
|
//
|
// Project: Pipelined Wishbone to AXI converter
|
// Project: Pipelined Wishbone to AXI converter
|
//
|
//
|
// Purpose: The B4 Wishbone SPEC allows transactions at a speed as fast as
|
// 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 per clock. The AXI bus allows transactions at a speed of
|
| Line 50... |
Line 50... |
//
|
//
|
//
|
//
|
////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////
|
//
|
//
|
//
|
//
|
|
`default_nettype none
|
|
//
|
module wbm2axisp #(
|
module wbm2axisp #(
|
parameter C_AXI_ID_WIDTH = 6, // The AXI id width used for R&W
|
parameter C_AXI_ID_WIDTH = 3, // 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 = 128,// 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 (log wordsize)
|
parameter DW = 32, // Wishbone data width
|
parameter DW = 8, // Wishbone data width
|
parameter AW = 26, // Wishbone address width
|
parameter AW = 26, // Wishbone address width (log wordsize)
|
parameter STRICT_ORDER = 0 // Reorder, or not? 0 -> Reorder
|
parameter [0:0] STRICT_ORDER = 1 // Reorder, or not? 0 -> Reorder
|
) (
|
) (
|
input i_clk, // System clock
|
input i_clk, // System clock
|
// input i_reset,// Wishbone reset signal--unused
|
// input i_reset,// Wishbone reset signal--unused
|
|
|
// AXI write address channel signals
|
// AXI write address channel signals
|
| Line 126... |
Line 128... |
|
|
//*****************************************************************************
|
//*****************************************************************************
|
// Parameter declarations
|
// Parameter declarations
|
//*****************************************************************************
|
//*****************************************************************************
|
|
|
localparam CTL_SIG_WIDTH = 3; // Control signal width
|
localparam LG_AXI_DW = ( C_AXI_DATA_WIDTH == 8) ? 3
|
localparam RD_STS_WIDTH = 16; // Read status signal width
|
: ((C_AXI_DATA_WIDTH == 16) ? 4
|
localparam WR_STS_WIDTH = 16; // Write status signal width
|
: ((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
|
// Internal register and wire declarations
|
//*****************************************************************************
|
//*****************************************************************************
|
|
|
| Line 148... |
Line 163... |
assign o_axi_awprot = 3'b010; // Unpriviledged, unsecure, data access
|
assign o_axi_awprot = 3'b010; // Unpriviledged, unsecure, data access
|
assign o_axi_arprot = 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_awqos = 4'h0; // Lowest quality of service (unused)
|
assign o_axi_arqos = 4'h0; // Lowest quality of service (unused)
|
assign o_axi_arqos = 4'h0; // Lowest quality of service (unused)
|
|
|
|
reg wb_mid_cycle, wb_last_cyc_stb, wb_mid_abort;
|
|
wire wb_cyc_stb;
|
// Command logic
|
// Command logic
|
|
// Transaction ID logic
|
|
wire [(LGFIFOLN-1):0] fifo_head;
|
|
reg [(C_AXI_ID_WIDTH-1):0] transaction_id;
|
|
|
|
initial transaction_id = 0;
|
|
always @(posedge i_clk)
|
|
if ((i_wb_stb)&&(!o_wb_stall))
|
|
transaction_id <= transaction_id + 1'b1;
|
|
|
|
assign fifo_head = transaction_id;
|
|
|
|
wire [(DW/8-1):0] no_sel;
|
|
wire [(LG_AXI_DW-4):0] axi_bottom_addr;
|
|
assign no_sel = 0;
|
|
assign axi_bottom_addr = 0;
|
|
|
|
|
// Write address logic
|
// Write address logic
|
|
|
|
initial o_axi_awvalid = 0;
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
o_axi_awvalid <= (!o_wb_stall)&&(i_wb_stb)&&(i_wb_we)
|
o_axi_awvalid <= (!o_wb_stall)&&(i_wb_stb)&&(i_wb_we)
|
||(o_wb_stall)&&(o_axi_awvalid)&&(!i_axi_awready);
|
||(o_axi_awvalid)&&(!i_axi_awready);
|
|
|
generate
|
generate
|
if (DW == 32)
|
|
begin
|
initial o_axi_awid = -1;
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if (!o_wb_stall) // 26 bit address becomes 28 bit ...
|
if ((i_wb_stb)&&(!o_wb_stall))
|
o_axi_awaddr <= { i_wb_addr[AW-1:2], 4'b00 };
|
o_axi_awid <= transaction_id;
|
end else if (DW == 128)
|
|
|
if (C_AXI_DATA_WIDTH == DW)
|
begin
|
begin
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if (!o_wb_stall) // 28 bit address ...
|
if ((i_wb_stb)&&(!o_wb_stall)) // 26 bit address becomes 28 bit ...
|
o_axi_awaddr <= { i_wb_addr[AW-1:0], 4'b00 };
|
o_axi_awaddr <= { i_wb_addr[AW-1:0], axi_bottom_addr };
|
end endgenerate
|
end else if (C_AXI_DATA_WIDTH / DW == 2)
|
|
begin
|
|
|
reg [5:0] transaction_id;
|
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if (!i_wb_cyc)
|
if ((i_wb_stb)&&(!o_wb_stall)) // 26 bit address becomes 28 bit ...
|
transaction_id <= 6'h00;
|
o_axi_awaddr <= { i_wb_addr[AW-1:1], axi_bottom_addr };
|
else if ((i_wb_stb)&&(~o_wb_stall))
|
|
transaction_id <= transaction_id + 6'h01;
|
end else if (C_AXI_DATA_WIDTH / DW == 4)
|
|
begin
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if ((i_wb_stb)&&(~o_wb_stall))
|
if ((i_wb_stb)&&(!o_wb_stall)) // 26 bit address becomes 28 bit ...
|
o_axi_awid <= transaction_id;
|
o_axi_awaddr <= { i_wb_addr[AW-1:2], axi_bottom_addr };
|
|
end endgenerate
|
|
|
|
|
// Read address logic
|
// Read address logic
|
assign o_axi_arid = o_axi_awid;
|
assign o_axi_arid = o_axi_awid;
|
assign o_axi_araddr = o_axi_awaddr;
|
assign o_axi_araddr = o_axi_awaddr;
|
assign o_axi_arlen = o_axi_awlen;
|
assign o_axi_arlen = o_axi_awlen;
|
assign o_axi_arsize = 3'b101; // maximum bytes per burst is 32
|
assign o_axi_arsize = 3'b101; // maximum bytes per burst is 32
|
|
initial o_axi_arvalid = 1'b0;
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
o_axi_arvalid <= (!o_wb_stall)&&(i_wb_stb)&&(!i_wb_we)
|
o_axi_arvalid <= (!o_wb_stall)&&(i_wb_stb)&&(!i_wb_we)
|
||(o_wb_stall)&&(o_axi_arvalid)&&(!i_axi_arready);
|
||(o_axi_arvalid)&&(!i_axi_arready);
|
|
|
|
|
// Write data logic
|
// Write data logic
|
generate
|
generate
|
if (DW == 32)
|
if (C_AXI_DATA_WIDTH == DW)
|
begin
|
begin
|
|
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if (!o_wb_stall)
|
if ((i_wb_stb)&&(!o_wb_stall))
|
o_axi_wdata <= { i_wb_data, i_wb_data, i_wb_data, i_wb_data };
|
o_axi_wdata <= i_wb_data;
|
|
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if (!o_wb_stall)
|
if ((i_wb_stb)&&(!o_wb_stall))
|
case(i_wb_addr[1:0])
|
o_axi_wstrb<= i_wb_sel;
|
2'b00:o_axi_wstrb<={ 4'h0, 4'h0, 4'h0,i_wb_sel};
|
|
2'b01:o_axi_wstrb<={ 4'h0, 4'h0,i_wb_sel, 4'h0};
|
end else if (C_AXI_DATA_WIDTH/2 == DW)
|
2'b10:o_axi_wstrb<={ 4'h0,i_wb_sel, 4'h0, 4'h0};
|
begin
|
2'b11:o_axi_wstrb<={i_wb_sel, 4'h0, 4'h0, 4'h0};
|
|
|
always @(posedge i_clk)
|
|
if ((i_wb_stb)&&(!o_wb_stall))
|
|
o_axi_wdata <= { i_wb_data, i_wb_data };
|
|
|
|
always @(posedge i_clk)
|
|
if ((i_wb_stb)&&(!o_wb_stall))
|
|
case(i_wb_addr[0])
|
|
1'b0:o_axi_wstrb<={ no_sel,i_wb_sel };
|
|
1'b1:o_axi_wstrb<={i_wb_sel, no_sel };
|
endcase
|
endcase
|
end else if (DW == 128)
|
|
|
end else if (C_AXI_DATA_WIDTH/4 == DW)
|
begin
|
begin
|
|
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if (!o_wb_stall)
|
if ((i_wb_stb)&&(!o_wb_stall))
|
o_axi_wdata <= i_wb_data;
|
o_axi_wdata <= { i_wb_data, i_wb_data, i_wb_data, i_wb_data };
|
|
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if (!o_wb_stall)
|
if ((i_wb_stb)&&(!o_wb_stall))
|
o_axi_wstrb <= i_wb_sel;
|
case(i_wb_addr[1:0])
|
|
2'b00:o_axi_wstrb<={ no_sel, no_sel, no_sel, i_wb_sel };
|
|
2'b01:o_axi_wstrb<={ no_sel, no_sel, i_wb_sel, no_sel };
|
|
2'b10:o_axi_wstrb<={ no_sel, i_wb_sel, no_sel, no_sel };
|
|
2'b11:o_axi_wstrb<={ i_wb_sel, no_sel, no_sel, no_sel };
|
|
endcase
|
|
|
end endgenerate
|
end endgenerate
|
|
|
assign o_axi_wlast = 1'b1;
|
assign o_axi_wlast = 1'b1;
|
|
initial o_axi_wvalid = 0;
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
o_axi_wvalid <= ((!o_wb_stall)&&(i_wb_stb)&&(i_wb_we))
|
o_axi_wvalid <= ((!o_wb_stall)&&(i_wb_stb)&&(i_wb_we))
|
||(o_wb_stall)&&(o_axi_wvalid)&&(!i_axi_wready);
|
||(o_axi_wvalid)&&(!i_axi_wready);
|
|
|
// Read data channel / response logic
|
// Read data channel / response logic
|
assign o_axi_rready = 1'b1;
|
assign o_axi_rready = 1'b1;
|
assign o_axi_bready = 1'b1;
|
assign o_axi_bready = 1'b1;
|
|
|
|
wire [(LGFIFOLN-1):0] n_fifo_head, nn_fifo_head;
|
|
assign n_fifo_head = fifo_head+1'b1;
|
|
assign nn_fifo_head = { fifo_head[(LGFIFOLN-1):1]+1'b1, fifo_head[0] };
|
|
|
|
|
wire w_fifo_full;
|
wire w_fifo_full;
|
|
reg [(LGFIFOLN-1):0] fifo_tail;
|
|
|
generate
|
generate
|
|
if (C_AXI_DATA_WIDTH == DW)
|
|
begin
|
if (STRICT_ORDER == 0)
|
if (STRICT_ORDER == 0)
|
begin
|
begin
|
// Reorder FIFO
|
|
//
|
|
localparam LGFIFOLN = C_AXI_ID_WIDTH;
|
|
localparam FIFOLN = (1<<LGFIFOLN);
|
|
// FIFO reorder buffer
|
|
reg [(LGFIFOLN-1):0] fifo_tail;
|
|
reg [(C_AXI_DATA_WIDTH-1):0] reorder_fifo_data [0:(FIFOLN-1)];
|
reg [(C_AXI_DATA_WIDTH-1):0] reorder_fifo_data [0:(FIFOLN-1)];
|
reg [(FIFOLN-1):0] reorder_fifo_valid;
|
|
reg [(FIFOLN-1):0] reorder_fifo_err;
|
|
|
|
initial reorder_fifo_valid = 0;
|
always @(posedge i_clk)
|
initial reorder_fifo_err = 0;
|
if ((o_axi_rready)&&(i_axi_rvalid))
|
|
reorder_fifo_data[i_axi_rid] <= i_axi_rdata;
|
|
always @(posedge i_clk)
|
|
o_wb_data <= reorder_fifo_data[fifo_tail];
|
|
end else begin
|
|
reg [(C_AXI_DATA_WIDTH-1):0] reorder_fifo_data;
|
|
|
|
always @(posedge i_clk)
|
|
reorder_fifo_data <= i_axi_rdata;
|
|
always @(posedge i_clk)
|
|
o_wb_data <= reorder_fifo_data;
|
|
end
|
|
end else if (C_AXI_DATA_WIDTH / DW == 2)
|
|
begin
|
|
reg reorder_fifo_addr [0:(FIFOLN-1)];
|
|
|
|
reg low_addr;
|
|
always @(posedge i_clk)
|
|
if ((i_wb_stb)&&(!o_wb_stall))
|
|
low_addr <= i_wb_addr[0];
|
|
always @(posedge i_clk)
|
|
if ((o_axi_arvalid)&&(i_axi_arready))
|
|
reorder_fifo_addr[o_axi_arid] <= low_addr;
|
|
|
if (DW == 32)
|
if (STRICT_ORDER == 0)
|
|
begin
|
|
reg [(C_AXI_DATA_WIDTH-1):0] reorder_fifo_data [0:(FIFOLN-1)];
|
|
|
|
always @(posedge i_clk)
|
|
if ((o_axi_rready)&&(i_axi_rvalid))
|
|
reorder_fifo_data[i_axi_rid] <= i_axi_rdata;
|
|
always @(posedge i_clk)
|
|
reorder_fifo_data[i_axi_rid] <= i_axi_rdata;
|
|
always @(posedge i_clk)
|
|
case(reorder_fifo_addr[fifo_tail])
|
|
1'b0: o_wb_data <=reorder_fifo_data[fifo_tail][( DW-1): 0 ];
|
|
1'b1: o_wb_data <=reorder_fifo_data[fifo_tail][(2*DW-1):( DW)];
|
|
endcase
|
|
end else begin
|
|
reg [(C_AXI_DATA_WIDTH-1):0] reorder_fifo_data;
|
|
|
|
always @(posedge i_clk)
|
|
reorder_fifo_data <= i_axi_rdata;
|
|
always @(posedge i_clk)
|
|
case(reorder_fifo_addr[fifo_tail])
|
|
1'b0: o_wb_data <=reorder_fifo_data[( DW-1): 0 ];
|
|
1'b1: o_wb_data <=reorder_fifo_data[(2*DW-1):( DW)];
|
|
endcase
|
|
end
|
|
end else if (C_AXI_DATA_WIDTH / DW == 4)
|
begin
|
begin
|
reg [1:0] reorder_fifo_addr [0:(FIFOLN-1)];
|
reg [1:0] reorder_fifo_addr [0:(FIFOLN-1)];
|
|
|
|
|
reg [1:0] low_addr;
|
reg [1:0] low_addr;
|
| Line 252... |
Line 360... |
low_addr <= i_wb_addr[1:0];
|
low_addr <= i_wb_addr[1:0];
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if ((o_axi_arvalid)&&(i_axi_arready))
|
if ((o_axi_arvalid)&&(i_axi_arready))
|
reorder_fifo_addr[o_axi_arid] <= low_addr;
|
reorder_fifo_addr[o_axi_arid] <= low_addr;
|
|
|
|
if (STRICT_ORDER == 0)
|
|
begin
|
|
reg [(C_AXI_DATA_WIDTH-1):0] reorder_fifo_data [0:(FIFOLN-1)];
|
|
|
|
always @(posedge i_clk)
|
|
if ((o_axi_rready)&&(i_axi_rvalid))
|
|
reorder_fifo_data[i_axi_rid] <= i_axi_rdata;
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
case(reorder_fifo_addr[fifo_tail][1:0])
|
case(reorder_fifo_addr[fifo_tail][1:0])
|
2'b00: o_wb_data <=reorder_fifo_data[fifo_tail][ 31: 0];
|
2'b00: o_wb_data <=reorder_fifo_data[fifo_tail][( DW-1): 0 ];
|
2'b01: o_wb_data <=reorder_fifo_data[fifo_tail][ 63:32];
|
2'b01: o_wb_data <=reorder_fifo_data[fifo_tail][(2*DW-1):( DW)];
|
2'b10: o_wb_data <=reorder_fifo_data[fifo_tail][ 95:64];
|
2'b10: o_wb_data <=reorder_fifo_data[fifo_tail][(3*DW-1):(2*DW)];
|
2'b11: o_wb_data <=reorder_fifo_data[fifo_tail][127:96];
|
2'b11: o_wb_data <=reorder_fifo_data[fifo_tail][(4*DW-1):(3*DW)];
|
endcase
|
endcase
|
|
end else begin
|
|
reg [(C_AXI_DATA_WIDTH-1):0] reorder_fifo_data;
|
|
|
end else if (DW == 128)
|
|
begin
|
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
o_wb_data <= reorder_fifo_data[fifo_tail];
|
reorder_fifo_data <= i_axi_rdata;
|
|
always @(posedge i_clk)
|
|
case(reorder_fifo_addr[fifo_tail][1:0])
|
|
2'b00: o_wb_data <=reorder_fifo_data[( DW-1): 0];
|
|
2'b01: o_wb_data <=reorder_fifo_data[(2*DW-1):( DW)];
|
|
2'b10: o_wb_data <=reorder_fifo_data[(3*DW-1):(2*DW)];
|
|
2'b11: o_wb_data <=reorder_fifo_data[(4*DW-1):(3*DW)];
|
|
endcase
|
|
end
|
end
|
end
|
|
|
|
endgenerate
|
|
|
wire [(LGFIFOLN-1):0] fifo_head;
|
wire axi_rd_ack, axi_wr_ack, axi_ard_req, axi_awr_req, axi_wr_req,
|
assign fifo_head = transaction_id;
|
axi_rd_err, axi_wr_err;
|
|
//
|
|
assign axi_ard_req = (o_axi_arvalid)&&(i_axi_arready);
|
|
assign axi_awr_req = (o_axi_awvalid)&&(i_axi_awready);
|
|
assign axi_wr_req = (o_axi_wvalid )&&(i_axi_wready);
|
|
//
|
|
assign axi_rd_ack = (i_axi_rvalid)&&(o_axi_rready);
|
|
assign axi_wr_ack = (i_axi_bvalid)&&(o_axi_bready);
|
|
assign axi_rd_err = (axi_rd_ack)&&(i_axi_rresp[1]);
|
|
assign axi_wr_err = (axi_wr_ack)&&(i_axi_bresp[1]);
|
|
|
|
//
|
|
// We're going to need a FIFO on the return to make certain that we can
|
|
// select the right bits from the return value, in the case where
|
|
// DW != the axi data width.
|
|
//
|
|
// If we aren't using a strict order, this FIFO is can be used as a
|
|
// reorder buffer as well, to place our out of order bus responses
|
|
// back into order. Responses on the wishbone, however, are *always*
|
|
// done in order.
|
|
`ifdef FORMAL
|
|
reg [31:0] reorder_count;
|
|
`endif
|
|
integer k;
|
|
generate
|
|
if (STRICT_ORDER == 0)
|
|
begin
|
|
// Reorder FIFO
|
|
//
|
|
// FIFO reorder buffer
|
|
reg [(FIFOLN-1):0] reorder_fifo_valid;
|
|
reg [(FIFOLN-1):0] reorder_fifo_err;
|
|
|
|
initial reorder_fifo_valid = 0;
|
|
initial reorder_fifo_err = 0;
|
|
|
// Let's do some math to figure out where the FIFO head will
|
|
// point to next, but let's also insist that it be LGFIFOLN
|
|
// bits in size as well. This'll be part of the fifo_full
|
|
// calculation below.
|
|
wire [(LGFIFOLN-1):0] n_fifo_head, nn_fifo_head;
|
|
assign n_fifo_head = fifo_head+1'b1;
|
|
assign nn_fifo_head = { fifo_head[(LGFIFOLN-1):1]+1'b1, fifo_head[0] };
|
|
|
|
|
initial fifo_tail = 0;
|
|
initial o_wb_ack = 0;
|
|
initial o_wb_err = 0;
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
begin
|
begin
|
if ((i_axi_rvalid)&&(o_axi_rready))
|
if (axi_rd_ack)
|
reorder_fifo_data[i_axi_rid]<= i_axi_rdata;
|
|
if ((i_axi_rvalid)&&(o_axi_rready))
|
|
begin
|
begin
|
reorder_fifo_valid[i_axi_rid] <= 1'b1;
|
reorder_fifo_valid[i_axi_rid] <= 1'b1;
|
reorder_fifo_err[i_axi_rid] <= i_axi_rresp[1];
|
reorder_fifo_err[i_axi_rid] <= axi_rd_err;
|
end
|
end
|
if ((i_axi_bvalid)&&(o_axi_bready))
|
if (axi_wr_ack)
|
begin
|
begin
|
reorder_fifo_valid[i_axi_bid] <= 1'b1;
|
reorder_fifo_valid[i_axi_bid] <= 1'b1;
|
reorder_fifo_err[i_axi_bid] <= i_axi_bresp[1];
|
reorder_fifo_err[i_axi_bid] <= axi_wr_err;
|
end
|
end
|
|
|
if (reorder_fifo_valid[fifo_tail])
|
if (reorder_fifo_valid[fifo_tail])
|
begin
|
begin
|
o_wb_ack <= 1'b1;
|
o_wb_ack <= (!wb_abort)&&(!reorder_fifo_err[fifo_tail]);
|
o_wb_err <= reorder_fifo_err[fifo_tail];
|
o_wb_err <= (!wb_abort)&&( reorder_fifo_err[fifo_tail]);
|
fifo_tail <= fifo_tail + 6'h1;
|
fifo_tail <= fifo_tail + 1'b1;
|
reorder_fifo_valid[fifo_tail] <= 1'b0;
|
reorder_fifo_valid[fifo_tail] <= 1'b0;
|
reorder_fifo_err[fifo_tail] <= 1'b0;
|
reorder_fifo_err[fifo_tail] <= 1'b0;
|
end else begin
|
end else begin
|
o_wb_ack <= 1'b0;
|
o_wb_ack <= 1'b0;
|
o_wb_err <= 1'b0;
|
o_wb_err <= 1'b0;
|
end
|
end
|
|
|
if (!i_wb_cyc)
|
if (!i_wb_cyc)
|
begin
|
begin
|
reorder_fifo_valid <= {(FIFOLN){1'b0}};
|
// reorder_fifo_valid <= 0;
|
reorder_fifo_err <= {(FIFOLN){1'b0}};
|
// reorder_fifo_err <= 0;
|
fifo_tail <= 6'h0;
|
|
o_wb_err <= 1'b0;
|
o_wb_err <= 1'b0;
|
o_wb_ack <= 1'b0;
|
o_wb_ack <= 1'b0;
|
end
|
end
|
end
|
end
|
|
|
|
`ifdef FORMAL
|
|
always @(*)
|
|
begin
|
|
reorder_count = 0;
|
|
for(k=0; k<FIFOLN; k=k+1)
|
|
if (reorder_fifo_valid[k])
|
|
reorder_count = reorder_count + 1;
|
|
end
|
|
|
|
reg [(FIFOLN-1):0] f_reorder_fifo_valid_zerod,
|
|
f_reorder_fifo_err_zerod;
|
|
always @(*)
|
|
f_reorder_fifo_valid_zerod <=
|
|
((reorder_fifo_valid >> fifo_tail)
|
|
| (reorder_fifo_valid << (FIFOLN-fifo_tail)));
|
|
always @(*)
|
|
assert((f_reorder_fifo_valid_zerod & (~((1<<f_fifo_used)-1)))==0);
|
|
//
|
|
always @(*)
|
|
f_reorder_fifo_err_zerod <=
|
|
((reorder_fifo_valid >> fifo_tail)
|
|
| (reorder_fifo_valid << (FIFOLN-fifo_tail)));
|
|
always @(*)
|
|
assert((f_reorder_fifo_err_zerod & (~((1<<f_fifo_used)-1)))==0);
|
|
`endif
|
|
|
reg r_fifo_full;
|
reg r_fifo_full;
|
|
initial r_fifo_full = 0;
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
begin
|
begin
|
if (!i_wb_cyc)
|
if ((i_wb_stb)&&(!o_wb_stall)
|
r_fifo_full <= 1'b0;
|
|
else if ((i_wb_stb)&&(~o_wb_stall)
|
|
&&(reorder_fifo_valid[fifo_tail]))
|
&&(reorder_fifo_valid[fifo_tail]))
|
r_fifo_full <= (fifo_tail==n_fifo_head);
|
r_fifo_full <= (fifo_tail==n_fifo_head);
|
else if ((i_wb_stb)&&(~o_wb_stall))
|
else if ((i_wb_stb)&&(!o_wb_stall))
|
r_fifo_full <= (fifo_tail==nn_fifo_head);
|
r_fifo_full <= (fifo_tail==nn_fifo_head);
|
else if (reorder_fifo_valid[fifo_tail])
|
else if (reorder_fifo_valid[fifo_tail])
|
r_fifo_full <= 1'b0;
|
r_fifo_full <= 1'b0;
|
else
|
else
|
r_fifo_full <= (fifo_tail==n_fifo_head);
|
r_fifo_full <= (fifo_tail==n_fifo_head);
|
end
|
end
|
assign w_fifo_full = r_fifo_full;
|
assign w_fifo_full = r_fifo_full;
|
end else begin
|
end else begin
|
//
|
//
|
// Strict ordering, but can only read every fourth addresses
|
// Strict ordering
|
//
|
//
|
assign w_fifo_full = 1'b0;
|
reg reorder_fifo_valid;
|
|
reg reorder_fifo_err;
|
|
|
|
initial reorder_fifo_valid = 1'b0;
|
|
initial reorder_fifo_err = 1'b0;
|
|
always @(posedge i_clk)
|
|
if (axi_rd_ack)
|
|
begin
|
|
reorder_fifo_valid <= 1'b1;
|
|
reorder_fifo_err <= axi_rd_err;
|
|
end else if (axi_wr_ack)
|
|
begin
|
|
reorder_fifo_valid <= 1'b1;
|
|
reorder_fifo_err <= axi_wr_err;
|
|
end else begin
|
|
reorder_fifo_valid <= 1'b0;
|
|
reorder_fifo_err <= 1'b0;
|
|
end
|
|
|
|
always @(*)
|
|
reorder_count = (reorder_fifo_valid) ? 1 : 0;
|
|
|
|
initial fifo_tail = 0;
|
|
always @(posedge i_clk)
|
|
if (reorder_fifo_valid)
|
|
fifo_tail <= fifo_tail + 6'h1;
|
|
|
|
initial o_wb_ack = 0;
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
o_wb_data <= i_axi_rdata[31:0];
|
o_wb_ack <= (reorder_fifo_valid)&&(i_wb_cyc)&&(!wb_abort);
|
|
|
|
initial o_wb_err = 0;
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
o_wb_ack <= (i_wb_cyc)&&(
|
o_wb_err <= (reorder_fifo_err)&&(i_wb_cyc)&&(!wb_abort);
|
((i_axi_rvalid)&&(o_axi_rready))
|
|
||((i_axi_bvalid)&&(o_axi_bready)));
|
reg r_fifo_full;
|
|
initial r_fifo_full = 0;
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
o_wb_err <= (i_wb_cyc)&&((o_wb_err)
|
begin
|
||((i_axi_rvalid)&&(i_axi_rresp[1]))
|
if ((i_wb_stb)&&(!o_wb_stall)
|
||((i_axi_bvalid)&&(i_axi_bresp[1])));
|
&&(reorder_fifo_valid))
|
|
r_fifo_full <= (fifo_tail==n_fifo_head);
|
|
else if ((i_wb_stb)&&(!o_wb_stall))
|
|
r_fifo_full <= (fifo_tail==nn_fifo_head);
|
|
else if (reorder_fifo_valid[fifo_tail])
|
|
r_fifo_full <= 1'b0;
|
|
else
|
|
r_fifo_full <= (fifo_tail==n_fifo_head);
|
|
end
|
|
|
|
assign w_fifo_full = r_fifo_full;
|
end endgenerate
|
end endgenerate
|
|
|
|
//
|
|
// Wishbone abort logic
|
|
//
|
|
|
|
// Did we just accept something?
|
|
always @(posedge i_clk)
|
|
wb_cyc_stb <= (i_wb_cyc)&&(i_wb_stb)&&(!o_wb_stall);
|
|
|
|
// Else, are we mid-cycle?
|
|
initial wb_mid_cycle = 0;
|
|
always @(posedge i_clk)
|
|
if ((fifo_head != fifo_tail)
|
|
||(o_axi_arvalid)||(o_axi_awvalid)
|
|
||(o_axi_wvalid)
|
|
||(i_wb_cyc)&&(i_wb_stb)&&(!o_wb_stall))
|
|
wb_mid_cycle <= 1'b1;
|
|
else
|
|
wb_mid_cycle <= 1'b0;
|
|
|
|
always @(posedge i_clk)
|
|
if (wb_mid_cycle)
|
|
wb_mid_abort <= (wb_mid_abort)||(!i_wb_cyc);
|
|
else
|
|
wb_mid_abort <= 1'b0;
|
|
|
|
wire wb_abort;
|
|
assign wb_abort = ((wb_mid_cycle)&&(!i_wb_cyc))||(wb_mid_abort);
|
|
|
// Now, the difficult signal ... the stall signal
|
// Now, the difficult signal ... the stall signal
|
// Let's build for a single cycle input ... and only stall if something
|
// Let's build for a single cycle input ... and only stall if something
|
// outgoing is valid and nothing is ready.
|
// outgoing is valid and nothing is ready.
|
assign o_wb_stall = (i_wb_cyc)&&(
|
assign o_wb_stall = (i_wb_cyc)&&(
|
(w_fifo_full)
|
(w_fifo_full)||(wb_mid_abort)
|
||((o_axi_awvalid)&&(!i_axi_awready))
|
||((o_axi_awvalid)&&(!i_axi_awready))
|
||((o_axi_wvalid )&&(!i_axi_wready ))
|
||((o_axi_wvalid )&&(!i_axi_wready ))
|
||((o_axi_arvalid)&&(!i_axi_arready)));
|
||((o_axi_arvalid)&&(!i_axi_arready)));
|
endmodule
|
|
|
|
|
|
No newline at end of file
|
No newline at end of file
|
|
/////////////////////////////////////////////////////////////////////////
|
|
//
|
|
//
|
|
//
|
|
// Formal methods section
|
|
//
|
|
// These are only relevant when *proving* that this translator works
|
|
//
|
|
//
|
|
//
|
|
/////////////////////////////////////////////////////////////////////////
|
|
`ifdef FORMAL
|
|
reg f_err_state;
|
|
//
|
|
`ifdef WBM2AXISP
|
|
// If we are the top-level of the design ...
|
|
`define ASSUME assume
|
|
`define FORMAL_CLOCK assume(i_clk == !f_last_clk); f_last_clk <= i_clk;
|
|
`else
|
|
`define ASSUME assert
|
|
`define FORMAL_CLOCK f_last_clk <= i_clk; // Clock will be given to us valid already
|
|
`endif
|
|
|
|
// Parameters
|
|
initial assert( (C_AXI_DATA_WIDTH / DW == 4)
|
|
||(C_AXI_DATA_WIDTH / DW == 2)
|
|
||(C_AXI_DATA_WIDTH == DW));
|
|
//
|
|
initial assert( C_AXI_ADDR_WIDTH - LG_AXI_DW + LG_WB_DW == AW);
|
|
|
|
//
|
|
// Setup
|
|
//
|
|
|
|
reg f_past_valid, f_last_clk;
|
|
|
|
always @($global_clock)
|
|
begin
|
|
`FORMAL_CLOCK
|
|
|
|
// 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));
|
|
// Wishbone inputs
|
|
`ASSUME($stable(i_wb_cyc));
|
|
`ASSUME($stable(i_wb_stb));
|
|
`ASSUME($stable(i_wb_we));
|
|
`ASSUME($stable(i_wb_addr));
|
|
`ASSUME($stable(i_wb_data));
|
|
`ASSUME($stable(i_wb_sel));
|
|
end
|
|
end
|
|
|
|
initial f_past_valid = 1'b0;
|
|
always @(posedge i_clk)
|
|
f_past_valid <= 1'b1;
|
|
|
|
//////////////////////////////////////////////
|
|
//
|
|
//
|
|
// Assumptions about the WISHBONE inputs
|
|
//
|
|
//
|
|
//////////////////////////////////////////////
|
|
wire i_reset;
|
|
assign i_reset = !f_past_valid;
|
|
|
|
wire [(C_AXI_ID_WIDTH-1):0] f_wb_nreqs, f_wb_nacks,f_wb_outstanding;
|
|
fwb_slave #(.DW(DW),.AW(AW),
|
|
.F_MAX_STALL(0),
|
|
.F_MAX_ACK_DELAY(0),
|
|
.F_LGDEPTH(C_AXI_ID_WIDTH),
|
|
.F_MAX_REQUESTS((1<<(C_AXI_ID_WIDTH))-2))
|
|
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);
|
|
|
|
wire [(C_AXI_ID_WIDTH-1):0] f_axi_rd_outstanding,
|
|
f_axi_wr_outstanding,
|
|
f_axi_awr_outstanding;
|
|
|
|
wire [((1<<C_AXI_ID_WIDTH)-1):0] f_axi_rd_id_outstanding,
|
|
f_axi_wr_id_outstanding,
|
|
f_axi_awr_id_outstanding;
|
|
|
|
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_MAXSTALL(3),
|
|
.F_AXI_MAXDELAY(3),
|
|
.F_STRICT_ORDER(STRICT_ORDER),
|
|
.F_CONSECUTIVE_IDS(1'b1),
|
|
.F_OPT_BURSTS(1'b0),
|
|
.F_CHECK_IDS(1'b1))
|
|
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_rd_outstanding( f_axi_rd_outstanding),
|
|
.f_axi_wr_outstanding( f_axi_wr_outstanding),
|
|
.f_axi_awr_outstanding( f_axi_awr_outstanding),
|
|
// Outstanding ID's
|
|
.f_axi_rd_id_outstanding( f_axi_rd_id_outstanding),
|
|
.f_axi_wr_id_outstanding( f_axi_wr_id_outstanding),
|
|
.f_axi_awr_id_outstanding(f_axi_awr_id_outstanding)
|
|
);
|
|
|
|
|
|
|
|
//////////////////////////////////////////////
|
|
//
|
|
//
|
|
// Assumptions about the AXI inputs
|
|
//
|
|
//
|
|
//////////////////////////////////////////////
|
|
|
|
|
|
//////////////////////////////////////////////
|
|
//
|
|
//
|
|
// Assertions about the AXI4 ouputs
|
|
//
|
|
//
|
|
//////////////////////////////////////////////
|
|
|
|
wire [(LGFIFOLN-1):0] f_last_transaction_id;
|
|
assign f_last_transaction_id = transaction_id- 1;
|
|
always @(posedge i_clk)
|
|
if (f_past_valid)
|
|
begin
|
|
assert(o_axi_awid == f_last_transaction_id);
|
|
if ($past(o_wb_stall))
|
|
assert($stable(o_axi_awid));
|
|
end
|
|
|
|
// 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);
|
|
|
|
//
|
|
// Let's look into write requests
|
|
//
|
|
initial assert(!o_axi_awvalid);
|
|
initial assert(!o_axi_wvalid);
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&($past(i_wb_stb))&&($past(i_wb_we))&&(!$past(o_wb_stall)))
|
|
begin
|
|
// Following any write request that we accept, awvalid and
|
|
// wvalid should both be true
|
|
assert(o_axi_awvalid);
|
|
assert(o_axi_wvalid);
|
|
end
|
|
|
|
// Let's assume all responses will come within 120 clock ticks
|
|
parameter [(C_AXI_ID_WIDTH-1):0] F_AXI_MAXDELAY = 3,
|
|
F_AXI_MAXSTALL = 3; // 7'd120;
|
|
localparam [(C_AXI_ID_WIDTH):0] F_WB_MAXDELAY = F_AXI_MAXDELAY + 4;
|
|
|
|
//
|
|
// AXI write address channel
|
|
//
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&($past(i_wb_cyc))&&(!$past(o_wb_stall)))
|
|
begin
|
|
if (!$past(i_wb_stb))
|
|
assert(!o_axi_awvalid);
|
|
else
|
|
assert(o_axi_awvalid == $past(i_wb_we));
|
|
end
|
|
//
|
|
generate
|
|
if (C_AXI_DATA_WIDTH == DW)
|
|
begin
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&($past(i_wb_cyc))&&($past(i_wb_stb))&&($past(i_wb_we))
|
|
&&(!$past(o_wb_stall)))
|
|
assert(o_axi_awaddr == { $past(i_wb_addr[AW-1:0]), axi_bottom_addr });
|
|
|
|
end else if (C_AXI_DATA_WIDTH / DW == 2)
|
|
begin
|
|
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&($past(i_wb_cyc))&&($past(i_wb_stb))&&($past(i_wb_we))
|
|
&&(!$past(o_wb_stall)))
|
|
assert(o_axi_awaddr == { $past(i_wb_addr[AW-1:1]), axi_bottom_addr });
|
|
|
|
end else if (C_AXI_DATA_WIDTH / DW == 4)
|
|
begin
|
|
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&($past(i_wb_cyc))&&($past(i_wb_stb))&&($past(i_wb_we))
|
|
&&(!$past(o_wb_stall)))
|
|
assert(o_axi_awaddr == { $past(i_wb_addr[AW-1:2]), axi_bottom_addr });
|
|
|
|
end endgenerate
|
|
|
|
//
|
|
// AXI write data channel
|
|
//
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&($past(i_wb_cyc))&&(!$past(o_wb_stall)))
|
|
begin
|
|
if (!$past(i_wb_stb))
|
|
assert(!o_axi_wvalid);
|
|
else
|
|
assert(o_axi_wvalid == $past(i_wb_we));
|
|
end
|
|
//
|
|
generate
|
|
if (C_AXI_DATA_WIDTH == DW)
|
|
begin
|
|
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&($past(i_wb_stb))&&($past(i_wb_we)))
|
|
begin
|
|
assert(o_axi_wdata == $past(i_wb_data));
|
|
assert(o_axi_wstrb == $past(i_wb_sel));
|
|
end
|
|
|
|
end else if (C_AXI_DATA_WIDTH / DW == 2)
|
|
begin
|
|
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&($past(i_wb_stb))&&($past(i_wb_we)))
|
|
begin
|
|
case($past(i_wb_addr[0]))
|
|
1'b0: assert(o_axi_wdata[( DW-1): 0] == $past(i_wb_data));
|
|
1'b1: assert(o_axi_wdata[(2*DW-1):DW] == $past(i_wb_data));
|
|
endcase
|
|
|
|
case($past(i_wb_addr[0]))
|
|
1'b0: assert(o_axi_wstrb == { no_sel,$past(i_wb_sel)});
|
|
1'b1: assert(o_axi_wstrb == { $past(i_wb_sel),no_sel});
|
|
endcase
|
|
end
|
|
|
|
end else if (C_AXI_DATA_WIDTH / DW == 4)
|
|
begin
|
|
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&($past(i_wb_stb))&&(!$past(o_wb_stall))&&($past(i_wb_we)))
|
|
begin
|
|
case($past(i_wb_addr[1:0]))
|
|
2'b00: assert(o_axi_wdata[ (DW-1): 0 ] == $past(i_wb_data));
|
|
2'b00: assert(o_axi_wdata[(2*DW-1):( DW)] == $past(i_wb_data));
|
|
2'b00: assert(o_axi_wdata[(3*DW-1):(2*DW)] == $past(i_wb_data));
|
|
2'b11: assert(o_axi_wdata[(4*DW-1):(3*DW)] == $past(i_wb_data));
|
|
endcase
|
|
|
|
case($past(i_wb_addr[1:0]))
|
|
2'b00: assert(o_axi_wstrb == { {(3){no_sel}},$past(i_wb_sel)});
|
|
2'b01: assert(o_axi_wstrb == { {(2){no_sel}},$past(i_wb_sel), {(1){no_sel}}});
|
|
2'b10: assert(o_axi_wstrb == { {(1){no_sel}},$past(i_wb_sel), {(2){no_sel}}});
|
|
2'b11: assert(o_axi_wstrb == { $past(i_wb_sel),{(3){no_sel}}});
|
|
endcase
|
|
end
|
|
end endgenerate
|
|
|
|
//
|
|
// AXI read address channel
|
|
//
|
|
initial assert(!o_axi_arvalid);
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&($past(i_wb_cyc))&&(!$past(o_wb_stall)))
|
|
begin
|
|
if (!$past(i_wb_stb))
|
|
assert(!o_axi_arvalid);
|
|
else
|
|
assert(o_axi_arvalid == !$past(i_wb_we));
|
|
end
|
|
//
|
|
generate
|
|
if (C_AXI_DATA_WIDTH == DW)
|
|
begin
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&($past(i_wb_stb))&&($past(!i_wb_we))
|
|
&&(!$past(o_wb_stall)))
|
|
assert(o_axi_araddr == $past({ i_wb_addr[AW-1:0], axi_bottom_addr }));
|
|
|
|
end else if (C_AXI_DATA_WIDTH / DW == 2)
|
|
begin
|
|
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&($past(i_wb_stb))&&($past(!i_wb_we))
|
|
&&(!$past(o_wb_stall)))
|
|
assert(o_axi_araddr == $past({ i_wb_addr[AW-1:1], axi_bottom_addr }));
|
|
|
|
end else if (C_AXI_DATA_WIDTH / DW == 4)
|
|
begin
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&($past(i_wb_stb))&&($past(!i_wb_we))
|
|
&&(!$past(o_wb_stall)))
|
|
assert(o_axi_araddr == $past({ i_wb_addr[AW-1:2], axi_bottom_addr }));
|
|
|
|
end endgenerate
|
|
|
|
//
|
|
// AXI write response channel
|
|
//
|
|
|
|
|
|
//
|
|
// AXI read data channel signals
|
|
//
|
|
always @(posedge i_clk)
|
|
`ASSUME(f_axi_rd_outstanding <= f_wb_outstanding);
|
|
//
|
|
always @(posedge i_clk)
|
|
`ASSUME(f_axi_rd_outstanding + f_axi_wr_outstanding <= f_wb_outstanding);
|
|
always @(posedge i_clk)
|
|
`ASSUME(f_axi_rd_outstanding + f_axi_awr_outstanding <= f_wb_outstanding);
|
|
//
|
|
always @(posedge i_clk)
|
|
`ASSUME(f_axi_rd_outstanding + f_axi_wr_outstanding +2 > f_wb_outstanding);
|
|
always @(posedge i_clk)
|
|
`ASSUME(f_axi_rd_outstanding + f_axi_awr_outstanding +2 > f_wb_outstanding);
|
|
|
|
// Make sure we only create one request at a time
|
|
always @(posedge i_clk)
|
|
assert((!o_axi_arvalid)||(!o_axi_wvalid));
|
|
always @(posedge i_clk)
|
|
assert((!o_axi_arvalid)||(!o_axi_awvalid));
|
|
|
|
// Now, let's look into that FIFO. Without it, we know nothing about the ID's
|
|
|
|
// Error handling
|
|
always @(posedge i_clk)
|
|
if (!i_wb_cyc)
|
|
f_err_state <= 0;
|
|
else if (o_wb_err)
|
|
f_err_state <= 1;
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&($past(f_err_state))&&(
|
|
(!$past(o_wb_stall))||(!$past(i_wb_stb))))
|
|
`ASSUME(!i_wb_stb);
|
|
|
|
// Head and tail pointers
|
|
|
|
// The head should only increment when something goes through
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&((!$past(i_wb_stb))||($past(o_wb_stall))))
|
|
assert($stable(fifo_head));
|
|
|
|
// Can't overrun the FIFO
|
|
wire [(LGFIFOLN-1):0] f_fifo_tail_minus_one;
|
|
assign f_fifo_tail_minus_one = fifo_tail - 1'b1;
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&($past(fifo_head == f_fifo_tail_minus_one)))
|
|
assert(fifo_head != fifo_tail);
|
|
|
|
reg f_pre_ack;
|
|
|
|
wire [(LGFIFOLN-1):0] f_fifo_used;
|
|
assign f_fifo_used = fifo_head - fifo_tail;
|
|
|
|
initial assert(fifo_tail == 0);
|
|
initial assert(reorder_fifo_valid == 0);
|
|
initial assert(reorder_fifo_err == 0);
|
|
initial f_pre_ack = 1'b0;
|
|
always @(posedge i_clk)
|
|
begin
|
|
f_pre_ack <= (!wb_abort)&&((axi_rd_ack)||(axi_wr_ack));
|
|
if (STRICT_ORDER)
|
|
begin
|
|
`ASSUME((!axi_rd_ack)||(!axi_wr_ack));
|
|
|
|
if (f_past_valid)
|
|
assert((!$past(i_wb_cyc))
|
|
||(o_wb_ack == $past(f_pre_ack)));
|
|
end
|
|
end
|
|
|
|
//
|
|
// Verify that there are no outstanding requests outside of the FIFO
|
|
// window. This should never happen, but the formal tools need to know
|
|
// that.
|
|
//
|
|
always @(*)
|
|
begin
|
|
assert((f_axi_rd_id_outstanding&f_axi_wr_id_outstanding)==0);
|
|
assert((f_axi_rd_id_outstanding&f_axi_awr_id_outstanding)==0);
|
|
|
|
if (fifo_head == fifo_tail)
|
|
begin
|
|
assert(f_axi_rd_id_outstanding == 0);
|
|
assert(f_axi_wr_id_outstanding == 0);
|
|
assert(f_axi_awr_id_outstanding == 0);
|
|
end
|
|
|
|
for(k=0; k<(1<<LGFIFOLN); k=k+1)
|
|
begin
|
|
if ( ((fifo_tail < fifo_head)&&(k < fifo_tail))
|
|
||((fifo_tail < fifo_head)&&(k >= fifo_head))
|
|
||((fifo_head < fifo_tail)&&(k >= fifo_head)&&(k < fifo_tail))
|
|
//||((fifo_head < fifo_tail)&&(k >=fifo_tail))
|
|
)
|
|
begin
|
|
assert(f_axi_rd_id_outstanding[k]==0);
|
|
assert(f_axi_wr_id_outstanding[k]==0);
|
|
assert(f_axi_awr_id_outstanding[k]==0);
|
|
end
|
|
end
|
|
end
|
|
|
|
generate
|
|
if (STRICT_ORDER)
|
|
begin : STRICTREQ
|
|
|
|
reg [C_AXI_ID_WIDTH-1:0] f_last_axi_id;
|
|
wire [C_AXI_ID_WIDTH-1:0] f_next_axi_id,
|
|
f_expected_last_id;
|
|
assign f_next_axi_id = f_last_axi_id + 1'b1;
|
|
assign f_expected_last_id = fifo_head - 1'b1 - f_fifo_used;
|
|
|
|
initial f_last_axi_id = -1;
|
|
always @(posedge i_clk)
|
|
if (i_reset)
|
|
f_last_axi_id = -1;
|
|
else if ((axi_rd_ack)||(axi_wr_ack))
|
|
f_last_axi_id <= f_next_axi_id;
|
|
else if (f_fifo_used == 0)
|
|
assert(f_last_axi_id == fifo_head-1'b1);
|
|
|
|
always @(posedge i_clk)
|
|
if (axi_rd_ack)
|
|
`ASSUME(i_axi_rid == f_next_axi_id);
|
|
else if (axi_wr_ack)
|
|
`ASSUME(i_axi_bid == f_next_axi_id);
|
|
end endgenerate
|
|
|
|
reg f_pending, f_returning;
|
|
initial f_pending = 1'b0;
|
|
always @(*)
|
|
f_pending <= (o_axi_arvalid)||(o_axi_awvalid);
|
|
always @(*)
|
|
f_returning <= (axi_rd_ack)||(axi_wr_ack);
|
|
|
|
reg [(LGFIFOLN):0] f_pre_count;
|
|
|
|
always @(*)
|
|
f_pre_count <= f_axi_awr_outstanding
|
|
+ f_axi_rd_outstanding
|
|
+ reorder_count
|
|
+ { {(LGFIFOLN){1'b0}}, (o_wb_ack) }
|
|
+ { {(LGFIFOLN){1'b0}}, (f_pending) };
|
|
always @(posedge i_clk)
|
|
assert((wb_abort)||(o_wb_err)||(f_pre_count == f_wb_outstanding));
|
|
|
|
always @(posedge i_clk)
|
|
assert((wb_abort)||(o_wb_err)||(f_fifo_used == f_wb_outstanding
|
|
// + {{(LGFIFOLN){1'b0}},f_past_valid)(i_wb_stb)&&(!o_wb_ack)}
|
|
- {{(LGFIFOLN){1'b0}},(o_wb_ack)}));
|
|
|
|
always @(posedge i_clk)
|
|
if (o_axi_wvalid)
|
|
assert(f_fifo_used != 0);
|
|
always @(posedge i_clk)
|
|
if (o_axi_arvalid)
|
|
assert(f_fifo_used != 0);
|
|
always @(posedge i_clk)
|
|
if (o_axi_awvalid)
|
|
assert(f_fifo_used != 0);
|
|
|
|
`endif
|
|
endmodule
|
|
|
No newline at end of file
|
No newline at end of file
|
