github-mirrors/ibex
1
0
Fork 0
mirror of https://github.com/lowRISC/ibex.git synced 2025-06-27 17:00:41 -04:00
Code Issues Projects Releases Packages Wiki Activity Actions

[ibex_core] Fix assertion when SecureIbex is false

Browse source 
This assertion wasn't quite correct if SecureIbex is false because it
was checking for the magic IbexMuBiOn value instead of just looking at
the bottom bit.

Fixes #2249.
This commit is contained in:
Rupert Swarbrick 2025-01-23 18:45:18 +00:00
parent cecf4fd2df
commit 78739562ce
1 changed files with 10 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

14
rtl/ibex_core.sv
View file

@ -1020,13 +1020,19 @@ module ibex_core import ibex_pkg::*; #(
end
end
// When fetch is disabled no instructions should be executed. Once fetch is disabled either the
// A 1-bit encoding of fetch_enable_i to avoid polluting the NoExecWhenFetchEnableNotOn assertion
// with notes about SecureIbex and mubi values.
logic fetch_enable_raw;
assign fetch_enable_raw = SecureIbex ? (fetch_enable_i == IbexMuBiOn) : fetch_enable_i[0];
// When fetch is disabled, no instructions should be executed. Once fetch is disabled either the
// ID/EX stage is not valid or the PC of the ID/EX stage must remain as it was at disable. The
// ID/EX valid should not ressert once it has been cleared.
`ASSERT(NoExecWhenFetchEnableNotOn, fetch_enable_i != IbexMuBiOn |=>
(~instr_valid_id || (pc_id == pc_at_fetch_disable)) && ~$rose(instr_valid_id))
`ASSERT(NoExecWhenFetchEnableNotOn,
!fetch_enable_raw |=>
(~instr_valid_id || (pc_id == pc_at_fetch_disable)) && ~$rose(instr_valid_id))
`endif
`endif // INC_ASSERT
////////////////////////
// RF (Register File) //