commit fa6d036059785714acc2e1c4b24f342df78996d6
author Rupert Swarbrick <rswarbrick@lowrisc.org> Mon May 09 16:51:56 2022 +0100
committer Rupert Swarbrick <rswarbrick@gmail.com> Wed May 11 08:08:48 2022 +0100
tree ce781b52e853e5359191e3d0c57a98e4d010231a
parent eae705771243aac7131fac6911fa70bf5aa422be

[otbn,dv] Fix timing of IdleIfLockedAndNotRotatingKeys_A assertion

The idle signal changes a cycle after the status input because of an
internal flop in the prim_mubi4_sender instance. Use a non-overlapped
implication to model this delay.

Signed-off-by: Rupert Swarbrick <rswarbrick@lowrisc.org>

hw/ip/otbn/dv/uvm/sva/otbn_idle_checker.sv

diff --git a/hw/ip/otbn/dv/uvm/sva/otbn_idle_checker.sv b/hw/ip/otbn/dv/uvm/sva/otbn_idle_checker.sv
index ec7e97c..4089b8e 100644
--- a/hw/ip/otbn/dv/uvm/sva/otbn_idle_checker.sv
+++ b/hw/ip/otbn/dv/uvm/sva/otbn_idle_checker.sv
@@ -117,7 +117,7 @@
           ((status_q_i == otbn_pkg::StatusLocked) && keys_busy) |->
           (idle_o_i == prim_mubi_pkg::MuBi4False))
   `ASSERT(IdleIfLockedAndNotRotatingKeys_A,
-          ((status_q_i == otbn_pkg::StatusLocked) && !keys_busy) |->
+          ((status_q_i == otbn_pkg::StatusLocked) && !keys_busy) |=>
           (idle_o_i == prim_mubi_pkg::MuBi4True))
 
   `ASSERT(NoStartKeyRotationWhenLocked_A,