483 lines
11 KiB
Verilog
483 lines
11 KiB
Verilog
////////////////////////////////////////////////////////////////////////////////
|
|
//
|
|
// Filename: sfifo.v
|
|
// {{{
|
|
// Project: WB2AXIPSP: bus bridges and other odds and ends
|
|
//
|
|
// Purpose: A synchronous data FIFO.
|
|
//
|
|
// Creator: Dan Gisselquist, Ph.D.
|
|
// Gisselquist Technology, LLC
|
|
//
|
|
////////////////////////////////////////////////////////////////////////////////
|
|
//
|
|
// Written and distributed by Gisselquist Technology, LLC
|
|
// }}}
|
|
// This design is hereby granted to the public domain.
|
|
// {{{
|
|
// This program is distributed in the hope that it will be useful, but WITHOUT
|
|
// ANY WARRANTY; without even the implied warranty of MERCHANTIBILITY or
|
|
// FITNESS FOR A PARTICULAR PURPOSE.
|
|
//
|
|
////////////////////////////////////////////////////////////////////////////////
|
|
//
|
|
`default_nettype none
|
|
// }}}
|
|
module sfifo #(
|
|
// {{{
|
|
parameter BW=8, // Byte/data width
|
|
parameter LGFLEN=4,
|
|
parameter [0:0] OPT_ASYNC_READ = 1'b1,
|
|
parameter [0:0] OPT_WRITE_ON_FULL = 1'b0,
|
|
parameter [0:0] OPT_READ_ON_EMPTY = 1'b0
|
|
// }}}
|
|
) (
|
|
// {{{
|
|
input wire i_clk,
|
|
input wire i_reset,
|
|
//
|
|
// Write interface
|
|
input wire i_wr,
|
|
input wire [(BW-1):0] i_data,
|
|
output wire o_full,
|
|
output reg [LGFLEN:0] o_fill,
|
|
//
|
|
// Read interface
|
|
input wire i_rd,
|
|
output reg [(BW-1):0] o_data,
|
|
output wire o_empty // True if FIFO is empty
|
|
`ifdef FORMAL
|
|
`ifdef F_PEEK
|
|
, output wire [LGFLEN:0] f_first_addr,
|
|
output wire [LGFLEN:0] f_second_addr,
|
|
output reg [BW-1:0] f_first_data, f_second_data,
|
|
|
|
output reg f_first_in_fifo,
|
|
f_second_in_fifo,
|
|
output reg [LGFLEN:0] f_distance_to_first,
|
|
f_distance_to_second
|
|
`endif
|
|
`endif
|
|
// }}}
|
|
);
|
|
|
|
// Register/net declarations
|
|
// {{{
|
|
localparam FLEN=(1<<LGFLEN);
|
|
reg r_full, r_empty;
|
|
reg [(BW-1):0] mem[0:(FLEN-1)];
|
|
reg [LGFLEN:0] wr_addr, rd_addr;
|
|
|
|
wire w_wr = (i_wr && !o_full);
|
|
wire w_rd = (i_rd && !o_empty);
|
|
// }}}
|
|
////////////////////////////////////////////////////////////////////////
|
|
//
|
|
// Write half
|
|
// {{{
|
|
////////////////////////////////////////////////////////////////////////
|
|
//
|
|
//
|
|
|
|
// o_fill
|
|
// {{{
|
|
initial o_fill = 0;
|
|
always @(posedge i_clk)
|
|
if (i_reset)
|
|
o_fill <= 0;
|
|
else case({ w_wr, w_rd })
|
|
2'b01: o_fill <= o_fill - 1;
|
|
2'b10: o_fill <= o_fill + 1;
|
|
default: o_fill <= wr_addr - rd_addr;
|
|
endcase
|
|
// }}}
|
|
|
|
// r_full, o_full
|
|
// {{{
|
|
initial r_full = 0;
|
|
always @(posedge i_clk)
|
|
if (i_reset)
|
|
r_full <= 0;
|
|
else case({ w_wr, w_rd})
|
|
2'b01: r_full <= 1'b0;
|
|
2'b10: r_full <= (o_fill == { 1'b0, {(LGFLEN){1'b1}} });
|
|
default: r_full <= (o_fill == { 1'b1, {(LGFLEN){1'b0}} });
|
|
endcase
|
|
|
|
assign o_full = (i_rd && OPT_WRITE_ON_FULL) ? 1'b0 : r_full;
|
|
// }}}
|
|
|
|
// wr_addr, the write address pointer
|
|
// {{{
|
|
initial wr_addr = 0;
|
|
always @(posedge i_clk)
|
|
if (i_reset)
|
|
wr_addr <= 0;
|
|
else if (w_wr)
|
|
wr_addr <= wr_addr + 1'b1;
|
|
// }}}
|
|
|
|
// Write to memory
|
|
// {{{
|
|
always @(posedge i_clk)
|
|
if (w_wr)
|
|
mem[wr_addr[(LGFLEN-1):0]] <= i_data;
|
|
// }}}
|
|
// }}}
|
|
////////////////////////////////////////////////////////////////////////
|
|
//
|
|
// Read half
|
|
// {{{
|
|
////////////////////////////////////////////////////////////////////////
|
|
//
|
|
//
|
|
|
|
// rd_addr, the read address pointer
|
|
// {{{
|
|
initial rd_addr = 0;
|
|
always @(posedge i_clk)
|
|
if (i_reset)
|
|
rd_addr <= 0;
|
|
else if (w_rd)
|
|
rd_addr <= rd_addr + 1;
|
|
// }}}
|
|
|
|
// r_empty, o_empty
|
|
// {{{
|
|
initial r_empty = 1'b1;
|
|
always @(posedge i_clk)
|
|
if (i_reset)
|
|
r_empty <= 1'b1;
|
|
else case ({ w_wr, w_rd })
|
|
2'b01: r_empty <= (o_fill <= 1);
|
|
2'b10: r_empty <= 1'b0;
|
|
default: begin end
|
|
endcase
|
|
|
|
assign o_empty = (OPT_READ_ON_EMPTY && i_wr) ? 1'b0 : r_empty;
|
|
// }}}
|
|
|
|
// Read from the FIFO
|
|
// {{{
|
|
generate if (OPT_ASYNC_READ && OPT_READ_ON_EMPTY)
|
|
begin : ASYNCHRONOUS_READ_ON_EMPTY
|
|
// o_data
|
|
// {{{
|
|
always @(*)
|
|
begin
|
|
o_data = mem[rd_addr[LGFLEN-1:0]];
|
|
if (r_empty)
|
|
o_data = i_data;
|
|
end
|
|
// }}}
|
|
end else if (OPT_ASYNC_READ)
|
|
begin : ASYNCHRONOUS_READ
|
|
// o_data
|
|
// {{{
|
|
always @(*)
|
|
o_data = mem[rd_addr[LGFLEN-1:0]];
|
|
// }}}
|
|
end else begin : REGISTERED_READ
|
|
// {{{
|
|
reg bypass_valid;
|
|
reg [BW-1:0] bypass_data, rd_data;
|
|
reg [LGFLEN-1:0] rd_next;
|
|
|
|
always @(*)
|
|
rd_next = rd_addr[LGFLEN-1:0] + 1;
|
|
|
|
// Memory read, bypassing it if we must
|
|
// {{{
|
|
initial bypass_valid = 0;
|
|
always @(posedge i_clk)
|
|
if (i_reset)
|
|
bypass_valid <= 0;
|
|
else if (r_empty || i_rd)
|
|
begin
|
|
if (!i_wr)
|
|
bypass_valid <= 1'b0;
|
|
else if (r_empty || (i_rd && (o_fill == 1)))
|
|
bypass_valid <= 1'b1;
|
|
else
|
|
bypass_valid <= 1'b0;
|
|
end
|
|
|
|
always @(posedge i_clk)
|
|
if (r_empty || i_rd)
|
|
bypass_data <= i_data;
|
|
|
|
initial mem[0] = 0;
|
|
initial rd_data = 0;
|
|
always @(posedge i_clk)
|
|
if (w_rd)
|
|
rd_data <= mem[rd_next];
|
|
|
|
always @(*)
|
|
if (OPT_READ_ON_EMPTY && r_empty)
|
|
o_data = i_data;
|
|
else if (bypass_valid)
|
|
o_data = bypass_data;
|
|
else
|
|
o_data = rd_data;
|
|
// }}}
|
|
// }}}
|
|
end endgenerate
|
|
// }}}
|
|
// }}}
|
|
////////////////////////////////////////////////////////////////////////////////
|
|
////////////////////////////////////////////////////////////////////////////////
|
|
////////////////////////////////////////////////////////////////////////////////
|
|
//
|
|
// FORMAL METHODS
|
|
// {{{
|
|
////////////////////////////////////////////////////////////////////////////////
|
|
////////////////////////////////////////////////////////////////////////////////
|
|
////////////////////////////////////////////////////////////////////////////////
|
|
//
|
|
`ifdef FORMAL
|
|
|
|
//
|
|
// Assumptions about our input(s)
|
|
//
|
|
//
|
|
`ifdef SFIFO
|
|
`define ASSUME assume
|
|
`else
|
|
`define ASSUME assert
|
|
`endif
|
|
|
|
reg f_past_valid;
|
|
wire [LGFLEN:0] f_fill, f_next;
|
|
wire f_empty;
|
|
|
|
initial f_past_valid = 1'b0;
|
|
always @(posedge i_clk)
|
|
f_past_valid <= 1'b1;
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
//
|
|
// Assertions about our flags and counters
|
|
// {{{
|
|
////////////////////////////////////////////////////////////////////////
|
|
//
|
|
//
|
|
|
|
assign f_fill = wr_addr - rd_addr;
|
|
assign f_empty = (wr_addr == rd_addr);
|
|
assign f_next = rd_addr + 1'b1;
|
|
|
|
always @(*)
|
|
begin
|
|
assert(f_fill <= { 1'b1, {(LGFLEN){1'b0}} });
|
|
assert(o_fill == f_fill);
|
|
|
|
assert(r_full == (f_fill == {1'b1, {(LGFLEN){1'b0}} }));
|
|
assert(r_empty == (f_fill == 0));
|
|
|
|
if (!OPT_WRITE_ON_FULL)
|
|
begin
|
|
assert(o_full == r_full);
|
|
end else begin
|
|
assert(o_full == (r_full && !i_rd));
|
|
end
|
|
|
|
if (!OPT_READ_ON_EMPTY)
|
|
begin
|
|
assert(o_empty == r_empty);
|
|
end else begin
|
|
assert(o_empty == (r_empty && !i_wr));
|
|
end
|
|
end
|
|
|
|
always @(posedge i_clk)
|
|
if (!OPT_ASYNC_READ && f_past_valid)
|
|
begin
|
|
if (f_fill == 0)
|
|
begin
|
|
assert(r_empty);
|
|
assert(o_empty || (OPT_READ_ON_EMPTY && i_wr));
|
|
end else if ($past(f_fill)>1)
|
|
begin
|
|
assert(!r_empty);
|
|
end else if ($past(!i_rd && f_fill > 0))
|
|
assert(!r_empty);
|
|
end
|
|
|
|
always @(*)
|
|
if (!r_empty)
|
|
begin
|
|
// This also applies for the registered read case
|
|
assert(mem[rd_addr[LGFLEN-1:0]] == o_data);
|
|
end else if (OPT_READ_ON_EMPTY)
|
|
assert(o_data == i_data);
|
|
|
|
// }}}
|
|
////////////////////////////////////////////////////////////////////////
|
|
//
|
|
// Formal contract: (Twin write test)
|
|
// {{{
|
|
// If you write two values in succession, you should be able to read
|
|
// those same two values in succession some time later.
|
|
//
|
|
////////////////////////////////////////////////////////////////////////
|
|
//
|
|
//
|
|
|
|
// Verilator lint_off UNDRIVEN
|
|
(* anyconst *) reg [LGFLEN:0] fw_first_addr;
|
|
// Verilator lint_on UNDRIVEN
|
|
`ifndef F_PEEK
|
|
wire [LGFLEN:0] f_first_addr;
|
|
wire [LGFLEN:0] f_second_addr;
|
|
reg [BW-1:0] f_first_data, f_second_data;
|
|
|
|
reg f_first_in_fifo, f_second_in_fifo;
|
|
reg [LGFLEN:0] f_distance_to_first, f_distance_to_second;
|
|
`endif
|
|
reg f_first_addr_in_fifo, f_second_addr_in_fifo;
|
|
|
|
assign f_first_addr = fw_first_addr;
|
|
assign f_second_addr = f_first_addr + 1;
|
|
|
|
always @(*)
|
|
begin
|
|
f_distance_to_first = (f_first_addr - rd_addr);
|
|
f_first_addr_in_fifo = 0;
|
|
if ((f_fill != 0) && (f_distance_to_first < f_fill))
|
|
f_first_addr_in_fifo = 1;
|
|
end
|
|
|
|
always @(*)
|
|
begin
|
|
f_distance_to_second = (f_second_addr - rd_addr);
|
|
f_second_addr_in_fifo = 0;
|
|
if ((f_fill != 0) && (f_distance_to_second < f_fill))
|
|
f_second_addr_in_fifo = 1;
|
|
end
|
|
|
|
always @(posedge i_clk)
|
|
if (w_wr && wr_addr == f_first_addr)
|
|
f_first_data <= i_data;
|
|
|
|
always @(posedge i_clk)
|
|
if (w_wr && wr_addr == f_second_addr)
|
|
f_second_data <= i_data;
|
|
|
|
always @(*)
|
|
if (f_first_addr_in_fifo)
|
|
assert(mem[f_first_addr[LGFLEN-1:0]] == f_first_data);
|
|
always @(*)
|
|
f_first_in_fifo = (f_first_addr_in_fifo && (mem[f_first_addr[LGFLEN-1:0]] == f_first_data));
|
|
|
|
always @(*)
|
|
if (f_second_addr_in_fifo)
|
|
assert(mem[f_second_addr[LGFLEN-1:0]] == f_second_data);
|
|
|
|
always @(*)
|
|
f_second_in_fifo = (f_second_addr_in_fifo && (mem[f_second_addr[LGFLEN-1:0]] == f_second_data));
|
|
|
|
always @(*)
|
|
if (f_first_in_fifo && (o_fill == 1 || f_distance_to_first == 0))
|
|
assert(o_data == f_first_data);
|
|
|
|
always @(*)
|
|
if (f_second_in_fifo && (o_fill == 1 || f_distance_to_second == 0))
|
|
assert(o_data == f_second_data);
|
|
|
|
always @(posedge i_clk)
|
|
if (f_past_valid && !$past(i_reset))
|
|
begin
|
|
case({$past(f_first_in_fifo), $past(f_second_in_fifo)})
|
|
2'b00: begin
|
|
if ($past(w_wr && (!w_rd || !r_empty))
|
|
&&($past(wr_addr == f_first_addr)))
|
|
begin
|
|
assert(f_first_in_fifo);
|
|
end else begin
|
|
assert(!f_first_in_fifo);
|
|
end
|
|
//
|
|
// The second could be in the FIFO, since
|
|
// one might write other data than f_first_data
|
|
//
|
|
// assert(!f_second_in_fifo);
|
|
end
|
|
2'b01: begin
|
|
assert(!f_first_in_fifo);
|
|
if ($past(w_rd && (rd_addr==f_second_addr)))
|
|
begin
|
|
assert((o_empty&&!OPT_ASYNC_READ)||!f_second_in_fifo);
|
|
end else begin
|
|
assert(f_second_in_fifo);
|
|
end
|
|
end
|
|
2'b10: begin
|
|
if ($past(w_wr)
|
|
&&($past(wr_addr == f_second_addr)))
|
|
begin
|
|
assert(f_second_in_fifo);
|
|
end else begin
|
|
assert(!f_second_in_fifo);
|
|
end
|
|
if ($past(!w_rd ||(rd_addr != f_first_addr)))
|
|
assert(f_first_in_fifo);
|
|
end
|
|
2'b11: begin
|
|
assert(f_second_in_fifo);
|
|
if ($past(!w_rd ||(rd_addr != f_first_addr)))
|
|
begin
|
|
assert(f_first_in_fifo);
|
|
if (rd_addr == f_first_addr)
|
|
assert(o_data == f_first_data);
|
|
end else begin
|
|
assert(!f_first_in_fifo);
|
|
assert(o_data == f_second_data);
|
|
end
|
|
end
|
|
endcase
|
|
end
|
|
// }}}
|
|
////////////////////////////////////////////////////////////////////////
|
|
//
|
|
// Cover properties
|
|
// {{{
|
|
////////////////////////////////////////////////////////////////////////
|
|
//
|
|
//
|
|
`ifdef SFIFO
|
|
reg f_was_full;
|
|
initial f_was_full = 0;
|
|
always @(posedge i_clk)
|
|
if (o_full)
|
|
f_was_full <= 1;
|
|
|
|
always @(posedge i_clk)
|
|
cover($fell(f_empty));
|
|
|
|
always @(posedge i_clk)
|
|
cover($fell(o_empty));
|
|
|
|
always @(posedge i_clk)
|
|
cover(f_was_full && f_empty);
|
|
|
|
always @(posedge i_clk)
|
|
cover($past(o_full,2)&&(!$past(o_full))&&(o_full));
|
|
|
|
always @(posedge i_clk)
|
|
if (f_past_valid)
|
|
cover($past(o_empty,2)&&(!$past(o_empty))&& o_empty);
|
|
`endif
|
|
// }}}
|
|
|
|
// Make Verilator happy
|
|
// Verilator lint_off UNUSED
|
|
wire unused_formal;
|
|
assign unused_formal = &{ 1'b0, f_next[LGFLEN], f_empty };
|
|
// Verilator lint_on UNUSED
|
|
`endif // FORMAL
|
|
// }}}
|
|
endmodule
|
|
`ifndef YOSYS
|
|
`default_nettype wire
|
|
`endif
|