Skip to content

Commit

Permalink
Implement a Wait state in the Sail stepper.
Browse files Browse the repository at this point in the history 
The Wait state is exited on interrupts or if requested by the C
emulator.  The current implementation requests an immediate exit.
  • Loading branch information
@pmundkur
pmundkur committed Feb 27, 2025
1 parent 4e2242a commit 1147192
Show file tree
Hide file tree
Showing 2 changed files with 90 additions and 78 deletions.
154 changes: 76 additions & 78 deletions model/riscv_step.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -40,6 +40,78 @@ union Step = {
Step_Waiting : unit
}

function step_wait_state(step_no : int, exit_wait : bool) -> (Step, bool) = {
if wakeForInterrupt() then {
if get_config_print_instr()
then print_instr("interrupt exit from WAIT state at PC " ^ BitStr(PC));

step_state = STEP_ACTIVE;
// The waiting instruction retires successfully. The
// pending interrupts will be handled in the next step.
(Step_Execute(RETIRE_OK()), true)
} else if exit_wait then {
// There are no pending interrupts; transition out of the Wait
// as instructed.
if get_config_print_instr()
then print_instr("forced exit from WAIT state at PC " ^ BitStr(PC));

step_state = STEP_ACTIVE;
// "When TW=1, then if WFI is executed in any
// less-privileged mode, and it does not complete within an
// implementation-specific, bounded time limit, the WFI
// instruction causes an illegal-instruction exception."
if (cur_privilege == Machine | mstatus[TW] == 0b0)
then (Step_Execute(RETIRE_OK()), true)
else (Step_Execute(RETIRE_FAIL(Illegal_Instruction())), true)
} else {
if get_config_print_instr()
then print_instr("remaining in WAIT state at PC " ^ BitStr(PC));
(Step_Waiting(), false)
}
}

function step_active_state(step_no: int, exit_wait : bool) -> ((Step, bool), option(xlenbits)) = {
match dispatchInterrupt(cur_privilege) {
Some(intr, priv) => ((Step_Pending_Interrupt(intr, priv), false), None()),
None() => match ext_fetch_hook(fetch()) {
/* extension error */
F_Ext_Error(e) => ((Step_Ext_Fetch_Failure(e), false), None()),
/* standard error */
F_Error(e, addr) => (((Step_Execute(RETIRE_FAIL(Memory_Exception(virtaddr(addr), e)))), false), None()),
/* non-error cases: */
F_RVC(h) => {
sail_instr_announce(h);
let instbits : option(xlenbits) = Some(zero_extend(h));
let ast = ext_decode_compressed(h);
if get_config_print_instr()
then {
print_instr("[" ^ dec_str(step_no) ^ "] [" ^ to_str(cur_privilege) ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(h) ^ ") " ^ to_str(ast));
};
/* check for RVC once here instead of every RVC execute clause. */
if extensionEnabled(Ext_Zca) then {
nextPC = PC + 2;
let r = execute(ast);
((Step_Execute(r), does_executed_retire_step(r)), instbits)
} else {
((Step_Execute(RETIRE_FAIL(Illegal_Instruction())), true), instbits)
}
},
F_Base(w) => {
sail_instr_announce(w);
let instbits : option(xlenbits) = Some(zero_extend(w));
let ast = ext_decode(w);
if get_config_print_instr()
then {
print_instr("[" ^ dec_str(step_no) ^ "] [" ^ to_str(cur_privilege) ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(w) ^ ") " ^ to_str(ast));
};
nextPC = PC + 4;
let r = execute(ast);
((Step_Execute(r), does_executed_retire_step(r)), instbits)
}
}
}
}

// The `step` function is the main interface to the non-Sail
// harness. It receives the current step number (which numbers the
// active or wait step), and whether it should exit a wait state.
Expand All @@ -60,84 +132,10 @@ function step(step_no : int, exit_wait : bool) -> step_result = {
*/
minstret_increment = should_inc_minstret(cur_privilege);

/* instruction bits for faulting instructions */
var instbits : option(xlenbits) = None();

let (step_val, stepped) : (Step, bool) =
match (dispatchInterrupt(cur_privilege), step_state) {
(Some(_, _), STEP_WAIT) => {
if get_config_print_instr()
then print_instr("interrupt exit from WAIT state at PC " ^ BitStr(PC));

step_state = STEP_ACTIVE;
// The waiting instruction retires successfully. The
// pending interrupts will be handled in the next step, which
// will match the next clause.
(Step_Execute(RETIRE_OK()), true)
},
(Some(intr, priv), STEP_ACTIVE) => {
(Step_Pending_Interrupt(intr, priv), false)
},
(None(), STEP_WAIT) => {
// There are no pending interrupts; transition out of the Wait
// if instructed.
if exit_wait then {
if get_config_print_instr()
then print_instr("forced exit from WAIT state at PC " ^ BitStr(PC));

step_state = STEP_ACTIVE;
// "When TW=1, then if WFI is executed in any
// less-privileged mode, and it does not complete within an
// implementation-specific, bounded time limit, the WFI
// instruction causes an illegal-instruction exception."
if (cur_privilege == Machine | mstatus[TW] == 0b0)
then (Step_Execute(RETIRE_OK()), true)
else (Step_Execute(RETIRE_FAIL(Illegal_Instruction())), true)
} else {
if get_config_print_instr()
then print_instr("remaining in WAIT state at PC " ^ BitStr(PC));
(Step_Waiting(), false)
}
},
(None(), STEP_ACTIVE) => {
/* the extension hook interposes on the fetch result */
match ext_fetch_hook(fetch()) {
/* extension error */
F_Ext_Error(e) => (Step_Ext_Fetch_Failure(e), false),
/* standard error */
F_Error(e, addr) => (Step_Execute(RETIRE_FAIL(Memory_Exception(virtaddr(addr), e))), false),
/* non-error cases: */
F_RVC(h) => {
sail_instr_announce(h);
instbits = Some(zero_extend(h));
let ast = ext_decode_compressed(h);
if get_config_print_instr()
then {
print_instr("[" ^ dec_str(step_no) ^ "] [" ^ to_str(cur_privilege) ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(h) ^ ") " ^ to_str(ast));
};
/* check for RVC once here instead of every RVC execute clause. */
if extensionEnabled(Ext_Zca) then {
nextPC = PC + 2;
let r = execute(ast);
(Step_Execute(r), does_executed_retire_step(r))
} else {
(Step_Execute(RETIRE_FAIL(Illegal_Instruction())), true)
}
},
F_Base(w) => {
sail_instr_announce(w);
instbits = Some(zero_extend(w));
let ast = ext_decode(w);
if get_config_print_instr()
then {
print_instr("[" ^ dec_str(step_no) ^ "] [" ^ to_str(cur_privilege) ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(w) ^ ") " ^ to_str(ast));
};
nextPC = PC + 4;
let r = execute(ast);
(Step_Execute(r), does_executed_retire_step(r))
}
}
}
let ((step_val, stepped), instbits) : ((Step, bool), option(xlenbits)) =
match step_state {
STEP_WAIT => (step_wait_state(step_no, exit_wait), None()),
STEP_ACTIVE => step_active_state(step_no, exit_wait)
};

match step_val {
Expand Down
14 changes: 14 additions & 0 deletions model/riscv_sys_control.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -129,6 +129,8 @@ function findPendingInterrupt(ip : xlenbits) -> option(InterruptType) = {
*
* We don't use the lowered views of {xie,xip} here, since the spec
* allows for example the M_Timer to be delegated to the S-mode.
*
* This is used when the hart is in the Active state.
*/
function getPendingSet(priv : Privilege) -> option((xlenbits, Privilege)) = {
// mideleg can only be non-zero if we support Supervisor mode.
Expand All @@ -145,6 +147,18 @@ function getPendingSet(priv : Privilege) -> option((xlenbits, Privilege)) = {
else None()
}

/* Check if a locally enabled interrupt is pending.
*
* This does not examine the global enable bits (MIE and SIE in
* mstatus) and their delegation in mideleg. It does honor the
* local interrupt enables in mie.
*
* This is used when the hart is in the Waiting state.
*/
function wakeForInterrupt() -> bool = {
(mip.bits & mie.bits) != zeros()
}

/* Examine the current interrupt state and return an interrupt to be *
* handled (if any), and the privilege it should be handled at.
*/
Expand Down

0 comments on commit 1147192

Please sign in to comment.