Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[rtl] Remove low utility assertions #2255

Merged
merged 1 commit into from
Feb 18, 2025
Merged

[rtl] Remove low utility assertions #2255

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
90 changes: 8 additions & 82 deletions rtl/ibex_controller.sv
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Loading