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 8b5f4c9 commit 3c19d27
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 3c19d27

Please sign in to comment.