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

[rtl] Remove low utility assertions

Browse source 
This removes several assertions from `ibex_controller`. They aimed to
ensure that controller behaviour was correct on exception behaviour
(e.g. ensuring that a pending interrupt will actually trigger an
interrupt). However they've proved to be flaky and hard to maintain with
multiple edge cases needing to be accounted for.

The co-simulation checking in functional verification will catch the
same issues these assertions catch. The assertions (when working
correctly) would cause a failure directly when the bug happens which
makes debugging easier. However they've added significant effort in
regression triage due to their many false failures so it's not worth the
maintenance burden.

Within formal they don't really add any value now we have the full
end-to-end formal flow.
This commit is contained in:
Greg Chadwick 2025-02-14 10:01:22 +00:00
parent 78739562ce
commit 2bb3fc7be4
1 changed files with 8 additions and 82 deletions
Download patch file Download diff file Expand all files Collapse all files

90
rtl/ibex_controller.sv
View file

@ -925,88 +925,14 @@ module ibex_controller #(
RESET, BOOT_SET, WAIT_SLEEP, SLEEP, FIRST_FETCH, DECODE, FLUSH,
IRQ_TAKEN, DBG_TAKEN_IF, DBG_TAKEN_ID})
`ifdef INC_ASSERT
// If something that causes a jump into an exception handler is seen that jump must occur before
// the next instruction executes. The logic tracks whether a jump into an exception handler is
// expected. Assertions check the jump occurs.
logic exception_req, exception_req_pending, exception_req_accepted, exception_req_done;
logic exception_pc_set, seen_exception_pc_set, expect_exception_pc_set;
logic exception_req_needs_pc_set;
assign exception_req = (special_req | enter_debug_mode | handle_irq);
// Any exception rquest will cause a transition out of DECODE, once the controller transitions
// back into DECODE we're done handling the request.
assign exception_req_done =
exception_req_pending & (ctrl_fsm_cs != DECODE) & (ctrl_fsm_ns == DECODE);
assign exception_req_needs_pc_set = enter_debug_mode | handle_irq | special_req_pc_change;
// An exception PC set uses specific PC types
assign exception_pc_set =
exception_req_pending & (pc_set_o & (pc_mux_o inside {PC_EXC, PC_ERET, PC_DRET}));
always @(posedge clk_i or negedge rst_ni) begin
if (!rst_ni) begin
exception_req_pending <= 1'b0;
exception_req_accepted <= 1'b0;
expect_exception_pc_set <= 1'b0;
seen_exception_pc_set <= 1'b0;
end else begin
// Keep `exception_req_pending` asserted once an exception_req is seen until it is done
exception_req_pending <= (exception_req_pending | exception_req) & ~exception_req_done;
// The exception req has been accepted once the controller transitions out of decode
exception_req_accepted <= (exception_req_accepted & ~exception_req_done) |
(exception_req & ctrl_fsm_ns != DECODE);
// Set `expect_exception_pc_set` if exception req needs one and keep it asserted until
// exception req is done
expect_exception_pc_set <= (expect_exception_pc_set | exception_req_needs_pc_set) &
~exception_req_done;
// Keep `seen_exception_pc_set` asserted once an exception PC set is seen until the
// exception req is done
seen_exception_pc_set <= (seen_exception_pc_set | exception_pc_set) & ~exception_req_done;
end
end
// Once an exception request has been accepted it must be handled before controller goes back to
// DECODE
`ASSERT(IbexNoDoubleExceptionReq, exception_req_accepted |-> ctrl_fsm_cs != DECODE)
// Only signal ready, allowing a new instruction into ID, if there is no exception request
// pending or it is done this cycle.
`ASSERT(IbexDontSkipExceptionReq,
id_in_ready_o |-> !exception_req_pending || exception_req_done)
// Once a PC set has been performed for an exception request there must not be any other
// excepting those to move into debug mode.
`ASSERT(IbexNoDoubleSpecialReqPCSet,
seen_exception_pc_set &&
!((ctrl_fsm_cs inside {DBG_TAKEN_IF, DBG_TAKEN_ID}) &&
(pc_mux_o == PC_EXC) && (exc_pc_mux_o == EXC_PC_DBD))
|-> !pc_set_o)
// When an exception request is done there must have been an appropriate PC set (either this
// cycle or a previous one).
`ASSERT(IbexSetExceptionPCOnSpecialReqIfExpected,
exception_req_pending && expect_exception_pc_set && exception_req_done |->
seen_exception_pc_set || exception_pc_set)
// 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
// 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)
`ifdef RVFI
// Workaround for internal verilator error when using hierarchical refers to calcuate this