[prim] SRAM Async FIFO
In this commit, SRAM Asynchronous FIFO primitive lib is added. It
follows same principle in the prim_fifo_async but the logic uses
Dual-port SRAM to store the data.
Signed-off-by: Eunchan Kim <eunchan@opentitan.org>
diff --git a/hw/formal/tools/jaspergold/fpv.tcl b/hw/formal/tools/jaspergold/fpv.tcl
index e993d52..a268b5b 100644
--- a/hw/formal/tools/jaspergold/fpv.tcl
+++ b/hw/formal/tools/jaspergold/fpv.tcl
@@ -69,6 +69,12 @@
# clock clk_main_i -both_edges
# reset -expr {!rst_main_ni}
+} elseif {$env(DUT_TOP) == "prim_fifo_async_sram_adapter_fpv"} {
+ clock clk_wr_i -factor 2
+ clock -rate {wvalid_i, wready_o, wdata_i} clk_wr_i
+ clock clk_rd_i -factor 3
+ clock -rate {rvalid_o, rready_i, rdata_o} clk_rd_i
+ reset -expr {!rst_ni}
} else {
clock clk_i -both_edges
reset -expr {!rst_ni}
diff --git a/hw/ip/prim/fpv/prim_fifo_async_sram_adapter_fpv.core b/hw/ip/prim/fpv/prim_fifo_async_sram_adapter_fpv.core
new file mode 100644
index 0000000..1b546d8
--- /dev/null
+++ b/hw/ip/prim/fpv/prim_fifo_async_sram_adapter_fpv.core
@@ -0,0 +1,27 @@
+CAPI=2:
+# Copyright lowRISC contributors.
+# Licensed under the Apache License, Version 2.0, see LICENSE for details.
+# SPDX-License-Identifier: Apache-2.0
+name: "lowrisc:fpv:prim_fifo_async_sram_adapter_fpv:0.1"
+description: "prim_fifo_async_sram_adapter FPV target"
+filesets:
+ files_formal:
+ depend:
+ - lowrisc:prim:all
+ - lowrisc:prim:ram_2p_async_adv
+ files:
+ - tb/prim_fifo_async_sram_adapter_fpv.sv
+ file_type: systemVerilogSource
+
+targets:
+ default: &default_target
+ default_tool: icarus
+ filesets:
+ - files_formal
+ toplevel: prim_fifo_async_sram_adapter_fpv
+
+ formal:
+ <<: *default_target
+
+ lint:
+ <<: *default_target
diff --git a/hw/ip/prim/fpv/tb/prim_fifo_async_sram_adapter_fpv.sv b/hw/ip/prim/fpv/tb/prim_fifo_async_sram_adapter_fpv.sv
new file mode 100644
index 0000000..fb3dda9
--- /dev/null
+++ b/hw/ip/prim/fpv/tb/prim_fifo_async_sram_adapter_fpv.sv
@@ -0,0 +1,204 @@
+// Copyright lowRISC contributors.
+// Licensed under the Apache License, Version 2.0, see LICENSE for details.
+// SPDX-License-Identifier: Apache-2.0
+//
+// Testbench module for prim_fifo_sram_async
+
+module prim_fifo_async_sram_adapter_fpv #(
+ parameter int unsigned Width = 32,
+ parameter int unsigned Depth = 16,
+
+ parameter int unsigned FpgaSram = 0 // Use FF based
+) (
+ input clk_wr_i,
+ input clk_rd_i,
+
+ input rst_ni,
+
+ input wvalid_i,
+ output logic wready_o,
+ input [Width-1:0] wdata_i,
+
+ output logic rvalid_o,
+ input rready_i,
+ output logic [Width-1:0] rdata_o
+);
+
+ localparam int unsigned SramAw = 7;
+ localparam int unsigned SramDw = 32;
+ localparam logic [SramAw-1:0] SramBaseAddr = 'h 30;
+
+ logic w_sram_req;
+ logic w_sram_gnt;
+ logic w_sram_write;
+ logic [SramAw-1:0] w_sram_addr;
+ logic [SramDw-1:0] w_sram_wdata;
+ logic [SramDw-1:0] w_sram_wmask;
+ logic w_sram_rvalid; // not used
+ logic [SramDw-1:0] w_sram_rdata; // not used
+ logic [1:0] w_sram_rerror; // not used
+
+ logic r_sram_req;
+ logic r_sram_gnt;
+ logic r_sram_write;
+ logic [SramAw-1:0] r_sram_addr;
+ logic [SramDw-1:0] r_sram_wdata; // not used
+ logic [SramDw-1:0] r_sram_wmask; // not used
+ logic r_sram_rvalid;
+ logic [SramDw-1:0] r_sram_rdata;
+ logic [1:0] r_sram_rerror;
+
+ prim_fifo_async_sram_adapter #(
+ .Width (Width),
+ .Depth (Depth),
+
+ .SramAw (SramAw), // TODO: random with constraint
+ .SramDw (SramDw), // TODO: random with constraint
+
+ .SramBaseAddr(SramBaseAddr) // TODO: random?
+ ) dut (
+ .clk_wr_i,
+ .rst_wr_ni (rst_ni),
+ .clk_rd_i,
+ .rst_rd_ni (rst_ni),
+
+ .wvalid_i,
+ .wready_o,
+ .wdata_i,
+
+ .wdepth_o (),
+
+ .rvalid_o,
+ .rready_i,
+ .rdata_o,
+
+ .rdepth_o (),
+
+ // Sram Interface
+ .w_sram_req_o (w_sram_req ),
+ .w_sram_gnt_i (w_sram_gnt ),
+ .w_sram_write_o (w_sram_write ),
+ .w_sram_addr_o (w_sram_addr ),
+ .w_sram_wdata_o (w_sram_wdata ),
+ .w_sram_wmask_o (w_sram_wmask ),
+ .w_sram_rvalid_i(w_sram_rvalid), // not used
+ .w_sram_rdata_i (w_sram_rdata ), // not used
+ .w_sram_rerror_i(w_sram_rerror), // not used
+
+ // Read SRAM port
+ .r_sram_req_o (r_sram_req ),
+ .r_sram_gnt_i (r_sram_gnt ),
+ .r_sram_write_o (r_sram_write ),
+ .r_sram_addr_o (r_sram_addr ),
+ .r_sram_wdata_o (r_sram_wdata ), // not used
+ .r_sram_wmask_o (r_sram_wmask ), // not used
+ .r_sram_rvalid_i(r_sram_rvalid),
+ .r_sram_rdata_i (r_sram_rdata ),
+ .r_sram_rerror_i(r_sram_rerror),
+
+ .r_full_o(),
+
+ .r_notempty_o(),
+
+ .w_full_o()
+ );
+
+if (FpgaSram == 1) begin : g_sram_fpga
+ // FPV looks like does not like the style of ram_2p.
+ prim_ram_2p #(
+ .Depth (2**SramAw),
+ .Width (SramDw),
+ .DataBitsPerMask (1)
+ ) u_sram (
+ .clk_a_i (clk_wr_i),
+ .clk_b_i (clk_rd_i),
+
+ .a_req_i (w_sram_req ),
+ .a_write_i (w_sram_write ),
+ .a_addr_i (w_sram_addr ),
+ .a_wdata_i (w_sram_wdata ),
+ .a_wmask_i (w_sram_wmask ),
+ .a_rdata_o (w_sram_rdata ),
+
+ .b_req_i (r_sram_req ),
+ .b_write_i (r_sram_write ),
+ .b_addr_i (r_sram_addr ),
+ .b_wdata_i (r_sram_wdata ),
+ .b_wmask_i (r_sram_wmask ),
+ .b_rdata_o (r_sram_rdata ),
+
+ .cfg_i ('0)
+ );
+end else begin : g_sram_ff
+ logic [SramDw-1:0] mem [2**SramAw];
+
+ always_ff @(posedge clk_wr_i) begin
+ if (w_sram_req && w_sram_write) begin
+ for (int unsigned i = 0; i < SramDw ; i++) begin
+ if (w_sram_wmask[i]) mem[w_sram_addr][i] <= w_sram_wdata[i];
+ end // for
+ end // if
+ end
+
+ always_ff @(posedge clk_rd_i) begin
+ if (r_sram_req && !r_sram_write) begin
+ r_sram_rdata <= mem[r_sram_addr];
+ end
+ end
+end // !FpgaSram
+
+ assign w_sram_gnt = w_sram_req;
+
+ always_ff @(posedge clk_wr_i) begin
+ w_sram_rvalid <= w_sram_req && !w_sram_write;
+ end
+
+ assign w_sram_rerror = '0;
+
+ assign r_sram_gnt = r_sram_req;
+
+ always_ff @(posedge clk_rd_i) begin
+ r_sram_rvalid <= r_sram_req && !r_sram_write;
+ end
+
+ assign r_sram_rerror = '0;
+
+ `ASSUME_FPV(WdataBins_M,
+ wvalid_i |-> wdata_i inside {
+ 32'h DEAD_BEEF, 32'h5A5A_A5A5, 32'h 1234_5678
+ },
+ clk_wr_i, !rst_ni)
+
+`ifdef FPV_ON
+ logic [Width-1:0] storage [Depth];
+ logic [Width-1:0] rdata;
+ logic [$clog2(Depth)-1:0] wptr, rptr;
+ logic wack, rack;
+
+ assign wack = wvalid_i && wready_o;
+ assign rack = rvalid_o && rready_i;
+
+ always_ff @(posedge clk_wr_i or negedge rst_ni) begin
+ if (!rst_ni) wptr <= '0;
+ else if (wack) wptr <= wptr+1;
+ end
+ always_ff @(posedge clk_rd_i or negedge rst_ni) begin
+ if (!rst_ni) rptr <= '0;
+ else if (rack) rptr <= rptr+1;
+ end
+
+ always_ff @(posedge clk_wr_i or negedge rst_ni) begin
+ if (!rst_ni) storage <= '{default:'0};
+ else if (wack) begin
+ storage[wptr] <= wdata_i;
+ end
+ end
+
+ assign rdata = storage[rptr];
+
+ `ASSERT(DataIntegrityCheck_A,
+ rack |-> rdata_o == rdata,
+ clk_rd_i, !rst_ni)
+`endif // FPV_ON
+
+endmodule : prim_fifo_async_sram_adapter_fpv
diff --git a/hw/ip/prim/prim_fifo.core b/hw/ip/prim/prim_fifo.core
index 169e247..8f2b077 100644
--- a/hw/ip/prim/prim_fifo.core
+++ b/hw/ip/prim/prim_fifo.core
@@ -12,6 +12,7 @@
- lowrisc:prim:util
- lowrisc:prim:flop_2sync
files:
+ - rtl/prim_fifo_async_sram_adapter.sv
- rtl/prim_fifo_async.sv
- rtl/prim_fifo_sync.sv
file_type: systemVerilogSource
diff --git a/hw/ip/prim/rtl/prim_fifo_async_sram_adapter.sv b/hw/ip/prim/rtl/prim_fifo_async_sram_adapter.sv
new file mode 100644
index 0000000..1cebd53
--- /dev/null
+++ b/hw/ip/prim/rtl/prim_fifo_async_sram_adapter.sv
@@ -0,0 +1,411 @@
+// Copyright lowRISC contributors.
+// Licensed under the Apache License, Version 2.0, see LICENSE for details.
+// SPDX-License-Identifier: Apache-2.0
+//
+// Generic Asynchronous SRAM FIFO (Dual port SRAM)
+
+`include "prim_assert.sv"
+
+module prim_fifo_async_sram_adapter #(
+ parameter int unsigned Width = 32,
+ parameter int unsigned Depth = 16,
+
+ // SRAM parameters
+ parameter int unsigned SramAw = 16,
+
+ // If SramDw > Width, upper data bits are 0.
+ parameter int unsigned SramDw = 32,
+ parameter logic [SramAw-1:0] SramBaseAddr = 'h 0,
+
+ // derived
+ localparam int unsigned DepthW = $clog2(Depth+1)
+) (
+ // Write port
+ input clk_wr_i,
+ input rst_wr_ni,
+ input wvalid_i,
+ output logic wready_o,
+ input [Width-1:0] wdata_i,
+ output logic [DepthW-1:0] wdepth_o,
+
+ // Read port
+ input clk_rd_i,
+ input rst_rd_ni,
+ output logic rvalid_o,
+ input rready_i,
+ output logic [Width-1:0] rdata_o,
+ output logic [DepthW-1:0] rdepth_o,
+
+ output logic r_full_o,
+ output logic r_notempty_o,
+
+ output logic w_full_o,
+
+ // TODO: watermark(threshold) ?
+
+ // SRAM interface
+ // Write SRAM port
+ output logic w_sram_req_o,
+ input w_sram_gnt_i,
+ output logic w_sram_write_o,
+ output logic [SramAw-1:0] w_sram_addr_o,
+ output logic [SramDw-1:0] w_sram_wdata_o,
+ output logic [SramDw-1:0] w_sram_wmask_o,
+ input w_sram_rvalid_i, // not used
+ input [SramDw-1:0] w_sram_rdata_i, // not used
+ input [1:0] w_sram_rerror_i, // not used
+
+ // Read SRAM port
+ output logic r_sram_req_o,
+ input r_sram_gnt_i,
+ output logic r_sram_write_o,
+ output logic [SramAw-1:0] r_sram_addr_o,
+ output logic [SramDw-1:0] r_sram_wdata_o, // not used
+ output logic [SramDw-1:0] r_sram_wmask_o, // not used
+ input r_sram_rvalid_i,
+ input [SramDw-1:0] r_sram_rdata_i,
+ input [1:0] r_sram_rerror_i
+);
+
+ ////////////////
+ // Definition //
+ ////////////////
+ // w_: write clock domain signals
+ // r_: read clock domain signals
+
+ // PtrVW: Pointer Value (without msb, flip) width
+ localparam int unsigned PtrVW = $clog2(Depth);
+ // PtrW: Read/Write pointer with flip bit
+ localparam int unsigned PtrW = PtrVW+1;
+
+ ////////////
+ // Signal //
+ ////////////
+
+ logic [PtrW-1:0] w_wptr_q, w_wptr_d, w_wptr_gray_d, w_wptr_gray_q;
+ logic [PtrW-1:0] r_wptr_gray, r_wptr;
+ logic [PtrVW-1:0] w_wptr_v, r_wptr_v;
+ logic w_wptr_p, r_wptr_p; // phase
+
+ logic [PtrW-1:0] r_rptr_q, r_rptr_d, r_rptr_gray_d, r_rptr_gray_q;
+ logic [PtrW-1:0] w_rptr_gray, w_rptr;
+ logic [PtrVW-1:0] r_rptr_v, w_rptr_v;
+ logic r_rptr_p, w_rptr_p; // phase
+
+ logic w_wptr_inc, r_rptr_inc;
+
+ logic w_full, r_full, r_empty;
+
+ // SRAM response one clock delayed. So store the value into read clock
+ // domain
+ logic stored;
+ logic [Width-1:0] rdata_q, rdata_d;
+
+ // SRAM has another read pointer (for address of SRAM req)
+ // It is -1 of r_rptr if stored, else same to r_rptr
+ logic r_sram_rptr_inc;
+ logic [PtrW-1:0] r_sram_rptr;
+
+ // r_sram_rptr == r_wptr
+ // Used to determine r_sram_req
+ logic r_sramrptr_empty;
+
+ logic rfifo_ack; // Used to check if FIFO read interface consumes a data
+ logic rsram_ack;
+
+ //////////////
+ // Datapath //
+ //////////////
+
+ // Begin: Write pointer sync to read clock ========================
+ assign w_wptr_inc = wvalid_i & wready_o;
+
+ assign w_wptr_d = w_wptr_q + PtrW'(1);
+
+ always_ff @(posedge clk_wr_i or negedge rst_wr_ni) begin
+ if (!rst_wr_ni) begin
+ w_wptr_q <= PtrW'(0);
+ w_wptr_gray_q <= PtrW'(0);
+ end else if (w_wptr_inc) begin
+ w_wptr_q <= w_wptr_d;
+ w_wptr_gray_q <= w_wptr_gray_d;
+ end
+ end
+
+ assign w_wptr_v = w_wptr_q[0+:PtrVW];
+ assign w_wptr_p = w_wptr_q[PtrW-1];
+
+ assign w_wptr_gray_d = dec2gray(w_wptr_d);
+
+ prim_flop_2sync #(
+ .Width (PtrW)
+ ) u_sync_wptr_gray (
+ .clk_i (clk_rd_i),
+ .rst_ni (rst_rd_ni),
+ .d_i (w_wptr_gray_q),
+ .q_o (r_wptr_gray)
+ );
+
+ assign r_wptr = gray2dec(r_wptr_gray);
+ assign r_wptr_p = r_wptr[PtrW-1];
+ assign r_wptr_v = r_wptr[0+:PtrVW];
+
+ assign wdepth_o = (w_wptr_p == w_rptr_p)
+ ? DepthW'(w_wptr_v - w_rptr_v)
+ : DepthW'({1'b1, w_wptr_v} - {1'b 0, w_rptr_v});
+ // End: Write pointer sync to read clock ------------------------
+
+ // Begin: Read pointer sync to write clock ========================
+ //assign r_rptr_inc = rvalid_o & rready_i;
+ //assign r_rptr_inc = r_sram_req_o && r_sram_gnt_i;
+ // Increase the read pointer (crossing the clock domain) only when the
+ // reader acked.
+ assign r_rptr_inc = rfifo_ack;
+
+ assign r_rptr_d = r_rptr_q + PtrW'(1);
+
+ always_ff @(posedge clk_rd_i or negedge rst_rd_ni) begin
+ if (!rst_rd_ni) begin
+ r_rptr_q <= PtrW'(0);
+ r_rptr_gray_q <= PtrW'(0);
+ end else if (r_rptr_inc) begin
+ r_rptr_q <= r_rptr_d;
+ r_rptr_gray_q <= r_rptr_gray_d;
+ end
+ end
+
+ assign r_rptr_v = r_rptr_q[0+:PtrVW];
+ assign r_rptr_p = r_rptr_q[PtrW-1];
+
+ assign r_rptr_gray_d = dec2gray(r_rptr_d);
+
+ prim_flop_2sync #(
+ .Width (PtrW)
+ ) u_sync_rptr_gray (
+ .clk_i (clk_wr_i),
+ .rst_ni (rst_wr_ni),
+ .d_i (r_rptr_gray_q),
+ .q_o (w_rptr_gray)
+ );
+
+ assign w_rptr = gray2dec(w_rptr_gray);
+ assign w_rptr_p = w_rptr[PtrW-1];
+ assign w_rptr_v = w_rptr[0+:PtrVW];
+
+ assign rdepth_o = (r_wptr_p == r_rptr_p)
+ ? DepthW'(r_wptr_v - r_rptr_v)
+ : DepthW'({1'b1, r_wptr_v} - {1'b 0, r_rptr_v});
+ // End: Read pointer sync to write clock ------------------------
+
+ // Begin: SRAM Read pointer
+ assign r_sram_rptr_inc = rsram_ack;
+
+ always_ff @(posedge clk_rd_i or negedge rst_rd_ni) begin
+ if (!rst_rd_ni) begin
+ r_sram_rptr <= PtrW'(0);
+ end else if (r_sram_rptr_inc) begin
+ r_sram_rptr <= r_sram_rptr + PtrW'(1);
+ end
+ end
+
+ assign r_sramrptr_empty = (r_wptr == r_sram_rptr);
+ // End: SRAM Read pointer
+
+ // Full/ Empty
+ localparam logic [PtrW-1:0] XorMask = PtrW'(1) << (PtrW-1);
+ assign w_full = (w_wptr_q == (w_rptr ^ XorMask));
+ assign r_full = (r_wptr == (r_rptr_q ^ XorMask));
+ assign r_empty = (r_wptr == r_rptr_q);
+
+ assign r_full_o = r_full;
+ assign r_notempty_o = !r_empty;
+ assign w_full_o = w_full;
+
+ assign rsram_ack = r_sram_req_o && r_sram_gnt_i;
+ assign rfifo_ack = rvalid_o && rready_i;
+
+ // SRAM Write Request
+ assign w_sram_req_o = wvalid_i && !w_full;
+ assign wready_o = !w_full && w_sram_gnt_i;
+ assign w_sram_write_o = 1'b 1; // Always write
+ assign w_sram_addr_o = SramBaseAddr + SramAw'(w_wptr_v);
+
+ assign w_sram_wdata_o = SramDw'(wdata_i);
+ assign w_sram_wmask_o = SramDw'(2**Width-1);
+
+ logic w_unused_sram;
+ assign w_unused_sram = ^{w_sram_rvalid_i, w_sram_rdata_i, w_sram_rerror_i};
+
+ // SRAM Read Request
+ // Request Scenario (!r_empty):
+ // - storage empty: Send request if
+ // !r_sram_rvalid_i || (rfifo_ack && r_sram_rvalid_i);
+ // - storage !empty: depends on the rfifo_ack:
+ // - r_rptr_inc: Can request more
+ // - !r_rptr_inc: Can't request
+ always_comb begin : r_sram_req
+ r_sram_req_o = 1'b 0;
+ // Karnough Map (!empty): sram_req
+ // {sram_rv, rfifo_ack} | 00 | 01 | 11 | 10
+ // ----------------------------------------------------------
+ // stored | 0 | 1 | impossible | 1 | 0
+ // | 1 | 0 | 1 | X | impossible
+ //
+ // req_o = r_ptr_inc || (!stored && !r_sram_rvalid_i)
+
+ if (stored) begin
+ // storage has data. depends on rfifo_ack
+ // rfifo_ack can be replaced to rready_i as `rvalid_o` is 1
+ r_sram_req_o = !r_sramrptr_empty && rfifo_ack;
+ end else begin
+ // storage has no data.
+ // Can send request only when the reader accept the request or no
+ // previous request sent out.
+ r_sram_req_o = !r_sramrptr_empty && !(r_sram_rvalid_i ^ rfifo_ack);
+ end
+ end : r_sram_req
+
+ assign rvalid_o = stored || r_sram_rvalid_i;
+ assign r_sram_write_o = 1'b 0; // always read
+ assign r_sram_wdata_o = '0;
+ assign r_sram_wmask_o = '0;
+
+ // Send SRAM request with sram read pointer.
+ assign r_sram_addr_o = SramBaseAddr + SramAw'(r_sram_rptr[0+:PtrVW]);
+
+ assign rdata_d = r_sram_rdata_i[0+:Width];
+
+ assign rdata_o = (stored) ? rdata_q : rdata_d;
+
+ logic unused_rsram;
+ assign unused_rsram = ^{r_sram_rerror_i};
+
+ // read clock domain rdata storage
+ logic store;
+
+ // Karnough Map (r_sram_rvalid_i):
+ // rfifo_ack | 0 | 1 |
+ // ---------------------
+ // stored 0 | 1 | 0 |
+ // 1 | 0 | 1 |
+ //
+ // stored = s.r.v && XNOR(stored, rptr_inc)
+ assign store = r_sram_rvalid_i && !(stored ^ rfifo_ack);
+
+ always_ff @(posedge clk_rd_i or negedge rst_rd_ni) begin
+ if (!rst_rd_ni) begin
+ stored <= 1'b 0;
+ rdata_q <= Width'(0);
+ end else if (store) begin
+ stored <= 1'b 1;
+ rdata_q <= rdata_d;
+ end else if (!r_sram_rvalid_i && rfifo_ack) begin
+ // No request sent, host reads the data
+ stored <= 1'b 0;
+ rdata_q <= Width'(0);
+ end
+ end
+
+ //////////////
+ // Function //
+ //////////////
+
+ // dec2gray / gray2dec copied from prim_fifo_async.sv
+ function automatic [PtrW-1:0] dec2gray(input logic [PtrW-1:0] decval);
+ logic [PtrW-1:0] decval_sub;
+ logic [PtrW-1:0] decval_in;
+ logic unused_decval_msb;
+
+ decval_sub = (PtrW)'(Depth) - {1'b0, decval[PtrW-2:0]} - 1'b1;
+
+ decval_in = decval[PtrW-1] ? decval_sub : decval;
+
+ // We do not care about the MSB, hence we mask it out
+ unused_decval_msb = decval_in[PtrW-1];
+ decval_in[PtrW-1] = 1'b0;
+
+ // Perform the XOR conversion
+ dec2gray = decval_in;
+ dec2gray ^= (decval_in >> 1);
+
+ // Override the MSB
+ dec2gray[PtrW-1] = decval[PtrW-1];
+ endfunction
+
+ // Algorithm walks up from 0..N-1 then flips the upper bit and walks down from N-1 to 0.
+ function automatic [PtrW-1:0] gray2dec(input logic [PtrW-1:0] grayval);
+ logic [PtrW-1:0] dec_tmp, dec_tmp_sub;
+ logic unused_decsub_msb;
+
+ dec_tmp = '0;
+ for (int i = PtrW-2; i >= 0; i--) begin
+ dec_tmp[i] = dec_tmp[i+1] ^ grayval[i];
+ end
+ dec_tmp_sub = (PtrW)'(Depth) - dec_tmp - 1'b1;
+ if (grayval[PtrW-1]) begin
+ gray2dec = dec_tmp_sub;
+ // Override MSB
+ gray2dec[PtrW-1] = 1'b1;
+ unused_decsub_msb = dec_tmp_sub[PtrW-1];
+ end else begin
+ gray2dec = dec_tmp;
+ end
+ endfunction
+
+ ///////////////
+ // Assertion //
+ ///////////////
+
+ `ASSERT_INIT(ParamCheckDepth_A, (Depth == 2**$clog2(Depth)))
+
+ // Use FF if less than 4.
+ `ASSERT_INIT(MinDepth_A, Depth >= 4)
+
+ // SramDw greather than or equal to Width
+ `ASSERT_INIT(WidthMatch_A, SramDw >= Width)
+
+ // Not stored, Not read valid, but rptr_inc case is impossible
+ `ASSERT(RptrIncDataValid_A,
+ r_rptr_inc |-> stored || r_sram_rvalid_i,
+ clk_rd_i, !rst_rd_ni)
+ `ASSERT(SramRvalid_A,
+ r_sram_rvalid_i |-> !stored || r_rptr_inc,
+ clk_rd_i, !rst_rd_ni)
+
+ // FIFO interface
+ `ASSERT(NoWAckInFull_A, w_wptr_inc |-> !w_full,
+ clk_wr_i, !rst_wr_ni)
+
+ `ASSERT(WptrIncrease_A,
+ w_wptr_inc |=> w_wptr_v == PtrVW'($past(w_wptr_v) + 1),
+ clk_wr_i, !rst_wr_ni)
+ `ASSERT(WptrGrayOneBitAtATime_A,
+ w_wptr_inc |=> $countones(w_wptr_gray_q ^ $past(w_wptr_gray_q)) == 1,
+ clk_wr_i, !rst_wr_ni)
+
+ `ASSERT(NoRAckInEmpty_A, r_rptr_inc |-> !r_empty,
+ clk_rd_i, !rst_rd_ni)
+
+ `ASSERT(RptrIncrease_A,
+ r_rptr_inc |=> PtrVW'($past(r_rptr_v) + 1) == r_rptr_v,
+ clk_rd_i, !rst_rd_ni)
+ `ASSERT(RptrGrayOneBitAtATime_A,
+ r_rptr_inc |=> $countones(r_rptr_gray_q ^ $past(r_rptr_gray_q)) == 1,
+ clk_rd_i, !rst_rd_ni)
+
+ // SRAM interface
+ `ASSERT(WSramRvalid_A, !w_sram_rvalid_i, clk_wr_i, !rst_wr_ni)
+ `ASSUME_FPV(WSramRdataError_M, w_sram_rdata_i == '0 && w_sram_rerror_i == '0,
+ clk_wr_i, !rst_wr_ni)
+
+ `ASSUME(RSramRvalidOneCycle_M,
+ r_sram_req_o && r_sram_gnt_i |=> r_sram_rvalid_i,
+ clk_rd_i, !rst_rd_ni)
+ `ASSUME_FPV(RErrorTied_M, r_sram_rerror_i == '0,
+ clk_rd_i, !rst_rd_ni)
+
+
+ // FPV coverage
+ `COVER_FPV(WFull_C, w_full, clk_wr_i, !rst_wr_ni)
+
+endmodule : prim_fifo_async_sram_adapter
