[otbn,dv] Assert that error bits are known

Signed-off-by: Andreas Kurth <[email protected]>
lowRISC · Sep 1, 2022 · 125b7c5 · 125b7c5
1 parent d0b9643
commit 125b7c5
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 0 deletions.
diff --git a/hw/ip/otbn/rtl/otbn.sv b/hw/ip/otbn/rtl/otbn.sv
@@ -1213,6 +1213,7 @@ module otbn
   `ASSERT_KNOWN(EdnRndOKnown_A, edn_rnd_o, clk_edn_i, !rst_edn_ni)
   `ASSERT_KNOWN(EdnUrndOKnown_A, edn_urnd_o, clk_edn_i, !rst_edn_ni)
   `ASSERT_KNOWN(OtbnOtpKeyO_A, otbn_otp_key_o, clk_otp_i, !rst_otp_ni)
+  `ASSERT_KNOWN(ErrBitsKnown_A, err_bits)
 
   // Incoming key must be valid (other inputs go via prim modules that handle the X checks).
   `ASSERT_KNOWN(KeyMgrKeyValid_A, keymgr_key_i.valid)

diff --git a/hw/ip/otbn/rtl/otbn_core.sv b/hw/ip/otbn/rtl/otbn_core.sv
@@ -906,6 +906,7 @@ module otbn_core
   `ASSERT_KNOWN(EdnRndReqOKnown_A, edn_rnd_req_o)
   `ASSERT_KNOWN(EdnUrndReqOKnown_A, edn_urnd_req_o)
   `ASSERT_KNOWN(InsnCntOKnown_A, insn_cnt_o)
+  `ASSERT_KNOWN(ErrBitsKnown_A, err_bits_o)
 
   // Keep the EDN requests active until they are acknowledged.
   `ASSERT(EdnRndReqStable_A, edn_rnd_req_o & ~edn_rnd_ack_i |=> edn_rnd_req_o)