OpenCores
URL https://opencores.org/ocsvn/wb2axip/wb2axip/trunk

Subversion Repositories wb2axip

Compare Revisions

  • This comparison shows the changes necessary to convert path 
    /
    from Rev 12 to Rev 13
    ↔ Reverse comparison
  •

Rev 12 → Rev 13

/wb2axip/trunk/rtl/wbm2axisp.v
55,19 → 55,19
`default_nettype none
//
module wbm2axisp #(
parameter C_AXI_ID_WIDTH = 3, // 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
parameter C_AXI_DATA_WIDTH = 32,// Width of the AXI R&W data
parameter C_AXI_ADDR_WIDTH = 28, // AXI Address width (log wordsize)
parameter DW = 8, // Wishbone data width
parameter AW = 26, // Wishbone address width (log wordsize)
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 DW = 32, // Wishbone data width
parameter AW = 26, // Wishbone address width (log wordsize)
parameter [0:0] STRICT_ORDER = 1 // Reorder, or not? 0 -> Reorder
) (
input i_clk, // System clock
// input i_reset,// Wishbone reset signal--unused
input wire i_clk, // System clock
// input wire i_reset,// Wishbone reset signal--unused
 
// AXI write address channel signals
input i_axi_awready, // Slave is ready to accept
input wire i_axi_awready, // Slave is ready to accept
output reg [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
80,20 → 80,20
output reg o_axi_awvalid, // Write address valid
 
// AXI write data channel signals
input i_axi_wready, // Write data ready
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
output wire o_axi_wlast, // Last write transaction
output reg o_axi_wvalid, // Write valid
 
// AXI write response channel signals
input [C_AXI_ID_WIDTH-1:0] i_axi_bid, // Response ID
input [1:0] i_axi_bresp, // Write response
input i_axi_bvalid, // Write reponse valid
input wire [C_AXI_ID_WIDTH-1:0] i_axi_bid, // Response ID
input wire [1:0] i_axi_bresp, // Write response
input wire i_axi_bvalid, // Write reponse valid
output wire o_axi_bready, // Response ready
 
// AXI read address channel signals
input i_axi_arready, // Read address ready
input wire i_axi_arready, // Read address ready
output wire [C_AXI_ID_WIDTH-1:0] o_axi_arid, // Read ID
output wire [C_AXI_ADDR_WIDTH-1:0] o_axi_araddr, // Read address
output wire [7:0] o_axi_arlen, // Read Burst Length
105,21 → 105,21
output wire [3:0] o_axi_arqos, // Read Protection type
output reg o_axi_arvalid, // Read address valid
 
// AXI read data channel signals
input [C_AXI_ID_WIDTH-1:0] i_axi_rid, // Response ID
input [1:0] i_axi_rresp, // Read response
input i_axi_rvalid, // Read reponse valid
input [C_AXI_DATA_WIDTH-1:0] i_axi_rdata, // Read data
input i_axi_rlast, // Read last
// AXI read data channel signals
input wire [C_AXI_ID_WIDTH-1:0] i_axi_rid, // Response ID
input wire [1:0] i_axi_rresp, // Read response
input wire i_axi_rvalid, // Read reponse valid
input wire [C_AXI_DATA_WIDTH-1:0] i_axi_rdata, // Read data
input wire i_axi_rlast, // Read last
output wire o_axi_rready, // Read Response ready
 
// We'll share the clock and the reset
input i_wb_cyc,
input i_wb_stb,
input i_wb_we,
input [(AW-1):0] i_wb_addr,
input [(DW-1):0] i_wb_data,
input [(DW/8-1):0] i_wb_sel,
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_ack,
output wire o_wb_stall,
output reg [(DW-1):0] o_wb_data,
165,8 → 165,9
assign o_axi_awqos = 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;
reg wb_mid_cycle, wb_mid_abort;
wire wb_abort;
 
// Command logic
// Transaction ID logic
wire [(LGFIFOLN-1):0] fifo_head;
214,8 → 215,8
end else if (C_AXI_DATA_WIDTH / DW == 4)
begin
always @(posedge i_clk)
if ((i_wb_stb)&&(!o_wb_stall)) // 26 bit address becomes 28 bit ...
o_axi_awaddr <= { i_wb_addr[AW-1:2], axi_bottom_addr };
if ((i_wb_stb)&&(!o_wb_stall)) // 26 bit address becomes 28 bit ...
o_axi_awaddr <= { i_wb_addr[AW-1:2], axi_bottom_addr };
end endgenerate
 
 
393,8 → 394,11
 
endgenerate
 
// verilator lint_off UNUSED
wire axi_rd_ack, axi_wr_ack, axi_ard_req, axi_awr_req, axi_wr_req,
axi_rd_err, axi_wr_err;
// verilator lint_on UNUSED
 
//
assign axi_ard_req = (o_axi_arvalid)&&(i_axi_arready);
assign axi_awr_req = (o_axi_awvalid)&&(i_axi_awready);
414,10 → 418,6
// 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
468,32 → 468,6
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;
initial r_fifo_full = 0;
always @(posedge i_clk)
532,13 → 506,10
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;
fifo_tail <= fifo_tail + 1'b1;
 
initial o_wb_ack = 0;
always @(posedge i_clk)
557,7 → 528,7
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])
else if (reorder_fifo_valid)
r_fifo_full <= 1'b0;
else
r_fifo_full <= (fifo_tail==n_fifo_head);
564,6 → 535,11
end
 
assign w_fifo_full = r_fifo_full;
 
// verilator lint_off UNUSED
wire [2*C_AXI_ID_WIDTH-1:0] strict_unused;
assign strict_unused = { i_axi_bid, i_axi_rid };
// verilator lint_on UNUSED
end endgenerate
 
//
570,11 → 546,7
// 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?
// Are we mid-cycle?
initial wb_mid_cycle = 0;
always @(posedge i_clk)
if ((fifo_head != fifo_tail)
591,7 → 563,6
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
604,6 → 575,12
||((o_axi_arvalid)&&(!i_axi_arready)));
 
 
// Make Verilator happy
// verilator lint_off UNUSED
wire [2:0] unused;
assign unused = { i_axi_bresp[0], i_axi_rresp[0], i_axi_rlast };
// verilator lint_on UNUSED
 
/////////////////////////////////////////////////////////////////////////
//
//
615,522 → 592,7
//
//
/////////////////////////////////////////////////////////////////////////
`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
// This section has been removed from this release.
//
endmodule

powered by: WebSVN 2.1.0

© copyright 1999-2024 OpenCores.org, equivalent to Oliscience, all rights reserved. OpenCores®, registered trademark.