[prim_sync_reqack_data] Fix SVA checking DST-to-SRC data stability
This commit reduces the window during which data must be stable. Since the
next REQ only takes 1 SRC clock cycle (and 2 DST clock cycles) to cross
over from SRC to DST, it doesn't make sense to check that the data remains
stable for 2 SRC clock cycles after the SRC handshake.
This resolves lowRISC/OpenTitan#4797.
Signed-off-by: Pirmin Vogel <vogelpi@lowrisc.org>
diff --git a/hw/ip/prim/rtl/prim_sync_reqack_data.sv b/hw/ip/prim/rtl/prim_sync_reqack_data.sv
index d73e45d..542fb43 100644
--- a/hw/ip/prim/rtl/prim_sync_reqack_data.sv
+++ b/hw/ip/prim/rtl/prim_sync_reqack_data.sv
@@ -95,9 +95,11 @@
end else if (DataSrc2Dst == 1'b0 && DataReg == 1'b0) begin : gen_assert_data_dst2src
// DST domain shall not change data while waiting for SRC domain to latch it (together with
- // receiving ACK). Assert that the data is stable +/- 2 SRC cycles around the SRC handshake.
+ // receiving ACK). It takes 2 SRC cycles for ACK to cross over from DST to SRC, and 1 SRC cycle
+ // for the next REQ to cross over from SRC to DST. Assert that the data is stable during that
+ // window, i.e. [-2,+1] SRC cycles around the SRC handshake.
`ASSERT(SyncReqAckDataHoldDst2Src,
- src_req_i && src_ack_o |-> $past(data_o,2) == data_o && $stable(data_o) [*3],
+ src_req_i && src_ack_o |-> $past(data_o,2) == data_o && $stable(data_o) [*2],
clk_src_i, !rst_src_ni)
end
