github-mirrors/cve2
1
0
Fork 0
mirror of https://github.com/openhwgroup/cve2.git synced 2025-04-22 04:57:25 -04:00
Code Issues Projects Releases Packages Wiki Activity Actions

[rtl] Fix assertion issues

Browse source 
Fixes #548
This commit is contained in:
Greg Chadwick 2020-02-07 14:54:50 +00:00
parent f24ffa5657
commit 24cbc32249
3 changed files with 21 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

5
rtl/ibex_core.sv
View file

@ -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 )
);

4
rtl/ibex_id_stage.sv
View file

@ -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)

17
rtl/ibex_load_store_unit.sv
View file

@ -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 {