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

Signed-off-by: Andreas Kurth <[email protected]>

Author: andreaskurth

rtl/ibex_controller.sv

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