diff options
Diffstat (limited to 'model/postlude')
| -rw-r--r-- | model/postlude/step.sail | 111 |
1 files changed, 56 insertions, 55 deletions
diff --git a/model/postlude/step.sail b/model/postlude/step.sail index f78acfd..33d04d5 100644 --- a/model/postlude/step.sail +++ b/model/postlude/step.sail @@ -88,63 +88,64 @@ private function run_hart_waiting(_step_no : int, wr: WaitReason, instbits : ins private function run_hart_active(step_no: nat) -> Step = { match dispatchInterrupt(cur_privilege) { - Some(intr, priv) => Step_Pending_Interrupt(intr, priv), - None() => match ext_fetch_hook(fetch()) { - // extension error - F_Ext_Error(e) => Step_Ext_Fetch_Failure(e), - // standard error - F_Error(e, addr) => Step_Fetch_Failure(Virtaddr(addr), e), - // non-error cases: - F_RVC(h) => { - sail_instr_announce(h); - fetch_callback(h); - let instbits : instbits = zero_extend(h); - let instruction = ext_decode_compressed(h); - if get_config_print_instr() - then { - print_log_instr("[" ^ dec_str(step_no) ^ "] [" ^ to_str(cur_privilege) ^ "]: " ^ bits_str(PC) ^ " (" ^ bits_str(h) ^ ") " ^ to_str(instruction), zero_extend(PC)); + Some(intr, priv) => return Step_Pending_Interrupt(intr, priv), + None() => (), + }; + match ext_fetch_hook(fetch()) { + // extension error + F_Ext_Error(e) => Step_Ext_Fetch_Failure(e), + // standard error + F_Error(e, addr) => Step_Fetch_Failure(Virtaddr(addr), e), + // non-error cases: + F_RVC(h) => { + sail_instr_announce(h); + fetch_callback(h); + let instbits : instbits = zero_extend(h); + let instruction = ext_decode_compressed(h); + if get_config_print_instr() + then { + print_log_instr("[" ^ dec_str(step_no) ^ "] [" ^ to_str(cur_privilege) ^ "]: " ^ bits_str(PC) ^ " (" ^ bits_str(h) ^ ") " ^ to_str(instruction), zero_extend(PC)); + }; + // When ELP is set to LP_EXPECTED, the next instruction needs to be + // the non-RVC `LPAD` instruction. + if is_landing_pad_expected() then { + let r = Trap(cur_privilege, CTL_TRAP(make_landing_pad_exception()), PC); + Step_Execute(r, instbits) + } + // check for RVC once here instead of every RVC execute clause. + else if currentlyEnabled(Ext_Zca) then { + nextPC = PC + 2; + let result : ExecutionResult = match execute(instruction) { + ExecuteAs(other_inst) => execute(other_inst), + result => result, }; - // When ELP is set to LP_EXPECTED, the next instruction needs to be - // the non-RVC `LPAD` instruction. - if is_landing_pad_expected() then { - let r = Trap(cur_privilege, CTL_TRAP(make_landing_pad_exception()), PC); - Step_Execute(r, instbits) - } - // check for RVC once here instead of every RVC execute clause. - else if currentlyEnabled(Ext_Zca) then { - nextPC = PC + 2; - let result : ExecutionResult = match execute(instruction) { - ExecuteAs(other_inst) => execute(other_inst), - result => result, - }; - Step_Execute(result, instbits) - } else { - Step_Execute(Illegal_Instruction(), instbits) - } - }, - F_Base(w) => { - sail_instr_announce(w); - fetch_callback(w); - let instbits : instbits = zero_extend(w); - let instruction = ext_decode(w); - if get_config_print_instr() - then { - print_log_instr("[" ^ dec_str(step_no) ^ "] [" ^ to_str(cur_privilege) ^ "]: " ^ bits_str(PC) ^ " (" ^ bits_str(w) ^ ") " ^ to_str(instruction), zero_extend(PC)); + Step_Execute(result, instbits) + } else { + Step_Execute(Illegal_Instruction(), instbits) + } + }, + F_Base(w) => { + sail_instr_announce(w); + fetch_callback(w); + let instbits : instbits = zero_extend(w); + let instruction = ext_decode(w); + if get_config_print_instr() + then { + print_log_instr("[" ^ dec_str(step_no) ^ "] [" ^ to_str(cur_privilege) ^ "]: " ^ bits_str(PC) ^ " (" ^ bits_str(w) ^ ") " ^ to_str(instruction), zero_extend(PC)); + }; + // When ELP is set to LP_EXPECTED, if the next instruction in + // the instruction stream is not LPAD, then a software check + // exception with a landing pad fault code is thrown. + if is_landing_pad_expected() & not(is_lpad_instruction(instruction)) then { + let r = Trap(cur_privilege, CTL_TRAP(make_landing_pad_exception()), PC); + Step_Execute(r, instbits) + } else { + nextPC = PC + 4; + let result : ExecutionResult = match execute(instruction) { + ExecuteAs(other_inst) => execute(other_inst), + result => result, }; - // When ELP is set to LP_EXPECTED, if the next instruction in - // the instruction stream is not LPAD, then a software check - // exception with a landing pad fault code is thrown. - if is_landing_pad_expected() & not(is_lpad_instruction(instruction)) then { - let r = Trap(cur_privilege, CTL_TRAP(make_landing_pad_exception()), PC); - Step_Execute(r, instbits) - } else { - nextPC = PC + 4; - let result : ExecutionResult = match execute(instruction) { - ExecuteAs(other_inst) => execute(other_inst), - result => result, - }; - Step_Execute(result, instbits) - } + Step_Execute(result, instbits) } } } |