diff --git a/rtl/ibex_core.sv b/rtl/ibex_core.sv index 7291d2bd..b17c25d6 100644 --- a/rtl/ibex_core.sv +++ b/rtl/ibex_core.sv @@ -567,7 +567,10 @@ module ibex_core #( .load_err_o ( lsu_load_err ), .store_err_o ( lsu_store_err ), - .busy_o ( lsu_busy ) + .busy_o ( lsu_busy ), + + .illegal_insn_id_i ( illegal_insn_id ), + .instr_valid_id_i ( instr_valid_id ) ); diff --git a/rtl/ibex_id_stage.sv b/rtl/ibex_id_stage.sv index 99d1b149..c95f19d6 100644 --- a/rtl/ibex_id_stage.sv +++ b/rtl/ibex_id_stage.sv @@ -682,7 +682,9 @@ module ibex_id_stage #( $onehot0({data_req_dec, multdiv_en_dec, branch_in_dec, jump_in_dec})) // Duplicated instruction flops must match - `ASSERT(IbexDuplicateInstrMatch, instr_valid_i |-> instr_rdata_i == instr_rdata_alu_i, clk_i, !rst_ni); + // === as DV environment can produce instructions with Xs in, so must use precise match that + // includes Xs + `ASSERT(IbexDuplicateInstrMatch, instr_valid_i |-> instr_rdata_i === instr_rdata_alu_i); `ifdef CHECK_MISALIGNED `ASSERT(IbexMisalignedMemoryAccess, !lsu_addr_incr_req_i) diff --git a/rtl/ibex_load_store_unit.sv b/rtl/ibex_load_store_unit.sv index 5363888d..33d9ede3 100644 --- a/rtl/ibex_load_store_unit.sv +++ b/rtl/ibex_load_store_unit.sv @@ -51,7 +51,11 @@ module ibex_load_store_unit ( output logic load_err_o, output logic store_err_o, - output logic busy_o + output logic busy_o, + + // used for assertions only + input logic illegal_insn_id_i, // illegal instruciton -> from ID/EX + input logic instr_valid_id_i // valid instruction -> from ID/EX ); logic [31:0] data_addr; @@ -485,9 +489,16 @@ module ibex_load_store_unit ( // Assertions // //////////////// + logic unused_instr_valid_id; + logic unused_illegal_insn_id; + + // Inputs only used for assertions + assign unused_instr_valid_id = instr_valid_id_i; + assign unused_illegal_insn_id = illegal_insn_id_i; + // Selectors must be known/valid. - `ASSERT_KNOWN(IbexDataTypeKnown, data_type_ex_i) - `ASSERT_KNOWN(IbexDataOffsetKnown, data_offset) + `ASSERT(IbexDataTypeKnown, (instr_valid_id_i & ~illegal_insn_id_i) |-> !$isunknown(data_type_ex_i)) + `ASSERT(IbexDataOffsetKnown, (instr_valid_id_i & ~illegal_insn_id_i) |-> !$isunknown(data_offset)) `ASSERT_KNOWN(IbexRDataOffsetQKnown, rdata_offset_q) `ASSERT_KNOWN(IbexDataTypeQKnown, data_type_q) `ASSERT(IbexLsuStateValid, ls_fsm_cs inside {