[prim_sync_reqack] Modify/extend SVAs with respect to reset
This commit modifies/extends the SVAs as follows:
- If any of the two domains is reset, all other assertions are disabled.
- If one domain is reset, also the other domain is expected to be reset.
Both resets need to be active at the same time.
In addition, the expected reset sequence is documented.
This is related to lowRISC/OpenTitan#8758.
This is related to lowRISC/OpenTitan#14287.
Signed-off-by: Pirmin Vogel <vogelpi@lowrisc.org>
diff --git a/hw/ip/prim/rtl/prim_sync_reqack.sv b/hw/ip/prim/rtl/prim_sync_reqack.sv
index d81a124..d58217f 100644
--- a/hw/ip/prim/rtl/prim_sync_reqack.sv
+++ b/hw/ip/prim/rtl/prim_sync_reqack.sv
@@ -10,6 +10,8 @@
// Notes:
// - Once asserted, the source (SRC) domain is not allowed to de-assert REQ without ACK.
// - The destination (DST) domain is not allowed to send an ACK without a REQ.
+// - When resetting one domain, also the other domain needs to be reset with both resets being
+// active at the same time.
// - This module works both when syncing from a faster to a slower clock domain and vice versa.
// - Internally, this module uses a non-return-to-zero, two-phase handshake protocol. Assuming the
// DST domain responds with an ACK immediately, the latency from asserting the REQ in the
@@ -186,9 +188,18 @@
// SRC domain can only de-assert REQ after receiving ACK.
`ASSERT(SyncReqAckHoldReq, $fell(src_req_i) && req_chk_i |->
- $fell(src_ack_o), clk_src_i, !rst_src_ni || !req_chk_i)
+ $fell(src_ack_o), clk_src_i, !rst_src_ni || !rst_dst_ni || !req_chk_i)
// DST domain cannot assert ACK without REQ.
- `ASSERT(SyncReqAckAckNeedsReq, dst_ack_i |-> dst_req_o, clk_dst_i, !rst_dst_ni)
+ `ASSERT(SyncReqAckAckNeedsReq, dst_ack_i |->
+ dst_req_o, clk_dst_i, !rst_src_ni || !rst_dst_ni)
+
+ // Always reset both domains. Both resets need to be active at the same time.
+ `ASSERT(SyncReqAckRstSrc, $fell(rst_src_ni) |->
+ (##[0:$] !rst_dst_ni within !rst_src_ni [*1:$]),
+ clk_src_i, 0)
+ `ASSERT(SyncReqAckRstDst, $fell(rst_dst_ni) |->
+ (##[0:$] !rst_src_ni within !rst_dst_ni [*1:$]),
+ clk_dst_i, 0)
endmodule
diff --git a/hw/ip/prim/rtl/prim_sync_reqack_data.sv b/hw/ip/prim/rtl/prim_sync_reqack_data.sv
index 840d86d..d05d0f3 100644
--- a/hw/ip/prim/rtl/prim_sync_reqack_data.sv
+++ b/hw/ip/prim/rtl/prim_sync_reqack_data.sv
@@ -92,7 +92,7 @@
// SRC domain cannot change data while waiting for ACK.
`ASSERT(SyncReqAckDataHoldSrc2Dst, !$stable(data_i) |->
(!src_req_i || (src_req_i && src_ack_o)),
- clk_src_i, !rst_src_ni)
+ clk_src_i, !rst_src_ni || !rst_dst_ni)
// Register stage cannot be used.
`ASSERT_INIT(SyncReqAckDataReg, DataSrc2Dst && !DataReg)
@@ -121,10 +121,10 @@
// checks that the DST side doesn't do anything that it shouldn't know is safe.
`ASSERT(SyncReqAckDataHoldDst2SrcA,
src_req_i && src_ack_o |-> $past(data_o, 2) == data_o && $past(data_o) == data_o,
- clk_src_i, !rst_src_ni)
+ clk_src_i, !rst_src_ni || !rst_dst_ni)
`ASSERT(SyncReqAckDataHoldDst2SrcB,
$past(src_req_i && src_ack_o) |-> $past(data_o) == data_o,
- clk_src_i, !rst_src_ni)
+ clk_src_i, !rst_src_ni || !rst_dst_ni)
end
endmodule
