From 3038edc09a2eb15762f2e58533f429489107520b Mon Sep 17 00:00:00 2001 From: Alejandro Soto Date: Wed, 6 Mar 2024 02:38:24 -0600 Subject: rtl/wb2axip: add to version control --- rtl/wb2axip/sfifo.v | 482 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 482 insertions(+) create mode 100644 rtl/wb2axip/sfifo.v (limited to 'rtl/wb2axip/sfifo.v') diff --git a/rtl/wb2axip/sfifo.v b/rtl/wb2axip/sfifo.v new file mode 100644 index 0000000..c60dffe --- /dev/null +++ b/rtl/wb2axip/sfifo.v @@ -0,0 +1,482 @@ +//////////////////////////////////////////////////////////////////////////////// +// +// 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<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 -- cgit v1.2.3