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.

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

Removed todo in controller related to dummies and forward progress. #445

Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
2 changes: 1 addition & 1 deletion rtl/cv32e40s_controller_fsm.sv
Original file line number Diff line number Diff line change
Expand Up @@ -299,7 +299,7 @@ module cv32e40s_controller_fsm import cv32e40s_pkg::*;
////////////////////////////////////////////////////////////////////
// - Blocking dummy instructions during single stepping and in debug mode.
// - Blocking dummies if there is a non-first op in IF (sequencer is in the middle of a sequence)
// Todo: Use allow_dummy_instr to guarantee progress (ensure there are never two dummies in a row in any pipeline stage)
// a_no_back_to_back_dummy in if_stage_sva checks that dummies can't come back-to-back with no other instructions in between.
assign ctrl_fsm_o.allow_dummy_instr = !dcsr_i.step && // Valid in IF because it can only be written in debug mode
!debug_mode_q && // Valid in IF because pipeline is killed when entering and exiting debug
(first_op_nondummy_if_i && prefetch_valid_if_i);
Expand Down
10 changes: 6 additions & 4 deletions sva/cv32e40s_if_stage_sva.sv
Original file line number Diff line number Diff line change
Expand Up @@ -114,13 +114,15 @@ module cv32e40s_if_stage_sva
dummy_insert && prefetch_resp_valid && !ctrl_fsm_i.kill_if |=> (ctrl_fsm_i.kill_if || (pc_if_o === $past(pc_if_o))))
else `uvm_error("if_stage", "Prefetcher popped during dummy instruction")

// Assert that we do not trigger dummy instructions multiple cycles in a row
// Assert that we do not trigger dummy instructions multiple instructions in a row (guarantees forward progress)
// Dummies may have to wait for id_ready, or even if_valid in case of halting IF.
// Todo: When/if we use allow_dummy_instr from controller_fsm to guarantee progress,
// this assertion should be updated to check for guaranteed progress
a_no_back_to_back_dummy_instructions :
assert property (@(posedge clk) disable iff (!rst_n)
dummy_insert && (if_valid_o && id_ready_i) |=> !dummy_insert)
dummy_insert && (if_valid_o && id_ready_i) // Dummy inserted and propagated to ID
##1 // One cycle later
(if_valid_o && id_ready_i)[->1] // Find next IF->ID transition
|->
!dummy_insert) // Must NOT be a dummy
else `uvm_error("if_stage", "Two dummy instructions in a row")

// Assert that we do not trigger dummy instructions when the sequencer is in the middle of a sequence
Expand Down