From a799a92e5eef5fbaa7b2a3054c88e5e48260f04f Mon Sep 17 00:00:00 2001 From: Pirmin Vogel Date: Tue, 6 Apr 2021 15:12:47 +0200 Subject: [PATCH] [rtl] Add SVA to ensure valid_i in compressed decoder is known This signal is used to gate several assertions related to unknown/invalid selector signals. We want to be sure to catch any X values entering the compressed decoder and ultimately ID. This is related to lowRISC/Ibex#540. Signed-off-by: Pirmin Vogel --- rtl/ibex_compressed_decoder.sv | 3 +++ 1 file changed, 3 insertions(+) diff --git a/rtl/ibex_compressed_decoder.sv b/rtl/ibex_compressed_decoder.sv index 12a487fe..ec694f51 100644 --- a/rtl/ibex_compressed_decoder.sv +++ b/rtl/ibex_compressed_decoder.sv @@ -282,6 +282,9 @@ module ibex_compressed_decoder ( // Assertions // //////////////// + // The valid_i signal used to gate below assertions must be known. + `ASSERT_KNOWN(IbexInstrValidKnown, valid_i) + // Selectors must be known/valid. `ASSERT(IbexInstrLSBsKnown, valid_i |-> !$isunknown(instr_i[1:0]))