github-mirrors/ibex
1
0
Fork 0
mirror of https://github.com/lowRISC/ibex.git synced 2025-04-22 21:07:34 -04:00
Code Issues Projects Releases Packages Wiki Activity Actions

[controller] Add assertion on pipeline flush when entering debug mode

Browse source 
Signed-off-by: Andreas Kurth <adk@lowrisc.org>
This commit is contained in:
Andreas Kurth 2024-12-16 11:22:28 +00:00
parent 88d27a0944
commit 8b82e89719
1 changed files with 9 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

9
rtl/ibex_controller.sv
View file

@ -997,6 +997,15 @@ module ibex_controller #(
// If there's a pending exception req that doesn't need a PC set we must not see one
`ASSERT(IbexNoPCSetOnSpecialReqIfNotExpected,
exception_req_pending && !expect_exception_pc_set |-> ~pc_set_o)
// If entering or exiting debug mode, the pipeline must be flushed. This is because Ibex
// currently does not support some of the pipeline stages being in debug mode; either all or
// none of the pipeline stages must be in debug mode. As `flush_id_o` only affects the ID/EX
// stage but does not prevent a fetched instruction from proceeding to ID/EX the next cycle, the
// assertion additionally requires `pc_set_o`, which sets the PC in the IF stage to a new value,
// hence preventing a fetched instruction from proceeding to the ID/EX stage in the next cycle.
`ASSERT(IbexPipelineFlushOnChangingDebugMode,
debug_mode_d != debug_mode_q |-> flush_id_o & pc_set_o)
`endif
`ifdef RVFI