commit 0fad9274ebb110c755db2fa936aab0baf422c21c
author Rupert Swarbrick <rswarbrick@lowrisc.org> Thu Feb 03 07:52:41 2022 +0000
committer Rupert Swarbrick <rswarbrick@gmail.com> Tue Feb 08 13:03:18 2022 +0000
tree 501b4f6e8bd81797cc2d262effe7a6b0bca94433
parent cc159e919757a96b2ece03b1099139978e248380

[otbn,dv] Fix assertion in RND FSM checking

If we are prefetching and a response comes in from the
EDN (edn_rnd_ack_i) at the same time as an instruction reads from
RND (rnd_req_i), we go to the "full" state, not the "reading" state.

The FSM I'd sketched out in the assertions was bogus: when both of
those signals are asserted at the same time, we can't go into both
READING and FULL states!

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

hw/ip/otbn/dv/uvm/env/otbn_rnd_if.sv

diff --git a/hw/ip/otbn/dv/uvm/env/otbn_rnd_if.sv b/hw/ip/otbn/dv/uvm/env/otbn_rnd_if.sv
index c02f351..6b0311d 100644
--- a/hw/ip/otbn/dv/uvm/env/otbn_rnd_if.sv
+++ b/hw/ip/otbn/dv/uvm/env/otbn_rnd_if.sv
@@ -149,7 +149,7 @@
   `ASSERT_EDGE(IDLE,        READING,     rnd_req_i)
   `ASSERT_EDGE(IDLE,        PREFETCHING, rnd_prefetch_req_i)
   `ASSERT_EDGE(READING,     FULL,        edn_rnd_ack_i)
-  `ASSERT_EDGE(PREFETCHING, READING,     rnd_req_i)
+  `ASSERT_EDGE(PREFETCHING, READING,     rnd_req_i && !edn_rnd_ack_i)
   `ASSERT_EDGE(PREFETCHING, FULL,        edn_rnd_ack_i)
   `ASSERT_EDGE(FULL,        IDLE,        rnd_req_i)