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