Skip to content

Commit

Permalink
[prim,fpv] Fix delays in assertions of prim_fifo_async_sram_adapter
Browse files Browse the repository at this point in the history
Rather strangely, these were originally correct but became wrong with
commit 1ebc7a9 (which was made as the author brought up an FPV
environment). Make them right again.

Signed-off-by: Rupert Swarbrick <[email protected]>
  • Loading branch information
rswarbrick committed Aug 29, 2024
1 parent cf32d0f commit d93d4ac
Showing 1 changed file with 5 additions and 2 deletions.
7 changes: 5 additions & 2 deletions hw/ip/prim/rtl/prim_fifo_async_sram_adapter.sv
Original file line number Diff line number Diff line change
Expand Up @@ -404,11 +404,14 @@ module prim_fifo_async_sram_adapter #(
`ASSERT(NoWAckInFull_A, w_wptr_inc |-> !w_full,
clk_wr_i, !rst_wr_ni)

// If a valid/ready handshake happens for the write pointer, that pointer should increment by one
`ASSERT(WptrIncrease_A,
w_wptr_inc |=> w_wptr_v == PtrVW'($past(w_wptr_v,2) + 1),
w_wptr_inc |=> w_wptr_q == $past(w_wptr_q) + PtrW'(1),
clk_wr_i, !rst_wr_ni)
// Check that the Gray coding works correctly, so the increment to w_wptr_gray_q changes exactly
// one bit.
`ASSERT(WptrGrayOneBitAtATime_A,
w_wptr_inc |=> $countones(w_wptr_gray_q ^ $past(w_wptr_gray_q,2)) == 1,
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,
Expand Down

0 comments on commit d93d4ac

Please sign in to comment.