diff --git a/model/riscv_jalr_rmem.sail b/model/riscv_jalr_rmem.sail index 216cbfd11..1c810dfad 100644 --- a/model/riscv_jalr_rmem.sail +++ b/model/riscv_jalr_rmem.sail @@ -68,6 +68,9 @@ /* SUCH DAMAGE. */ /*=======================================================================================*/ +/* Zicfilp : Update ELP state */ +val zicfilp_update_elp : (regidx) -> unit + /* The definition for the memory model. */ function clause execute (RISCV_JALR(imm, rs1, rd)) = { @@ -76,5 +79,7 @@ function clause execute (RISCV_JALR(imm, rs1, rd)) = { X(rd) = nextPC; /* compatible with JALR, C.JR and C.JALR */ let newPC : xlenbits = X(rs1) + sign_extend(imm); nextPC = [newPC with 0 = bitzero]; /* Clear newPC[0] */ + /* update ELP if Zicfilp is active */ + zicfilp_update_elp(rs1); RETIRE_SUCCESS } diff --git a/model/riscv_jalr_seq.sail b/model/riscv_jalr_seq.sail index 35d370b5e..ffc27f064 100644 --- a/model/riscv_jalr_seq.sail +++ b/model/riscv_jalr_seq.sail @@ -68,6 +68,9 @@ /* SUCH DAMAGE. */ /*=======================================================================================*/ +/* Zicfilp : Update ELP state */ +val zicfilp_update_elp : (regidx) -> unit + /* The definition for the sequential model. */ function clause execute (RISCV_JALR(imm, rs1, rd)) = { @@ -92,6 +95,8 @@ function clause execute (RISCV_JALR(imm, rs1, rd)) = { } else { X(rd) = get_next_pc(); set_next_pc(target); + /* update ELP if Zicfilp is active */ + zicfilp_update_elp(rs1); RETIRE_SUCCESS } } diff --git a/model/riscv_step.sail b/model/riscv_step.sail index ec7d58e3a..771ad17cf 100644 --- a/model/riscv_step.sail +++ b/model/riscv_step.sail @@ -115,14 +115,20 @@ function step(step_no : int) -> bool = { 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 haveRVC() then { - nextPC = PC + 2; - (execute(ast), true) - } else { - handle_illegal(); + /* Zicfilp requires a landing pad (a base inst) if ELP is LP_EXPECTED */ + if elp != ElpState_to_bits(LP_EXPECTED) then { + handle_sw_check_exception(LANDING_PAD_FAULT); (RETIRE_FAIL, true) - } + } else { + /* check for RVC once here instead of every RVC execute clause. */ + if haveRVC() then { + nextPC = PC + 2; + (execute(ast), true) + } else { + handle_illegal(); + (RETIRE_FAIL, true) + } + } }, F_Base(w) => { instbits = zero_extend(w); @@ -131,8 +137,14 @@ function step(step_no : int) -> bool = { then { print_instr("[" ^ dec_str(step_no) ^ "] [" ^ to_str(cur_privilege) ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(w) ^ ") " ^ to_str(ast)); }; - nextPC = PC + 4; - (execute(ast), true) + /* Zicfilp requires a aligned lpad if elp is LP_EXPECTED */ + if zicfilp_is_elp_violated() then { + handle_sw_check_exception(LANDING_PAD_FAULT); + (RETIRE_FAIL, true) + } else { + nextPC = PC + 4; + (execute(ast), true) + } } } } diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index a8b2000b6..16971bddc 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -377,6 +377,8 @@ val rvfi_trap : unit -> unit function rvfi_trap () = () $endif +val zicfilp_preserve_elp : (Privilege) -> unit + /* handle exceptional ctl flow by updating nextPC and operating privilege */ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlenbits, info : option(xlenbits), ext : option(ext_exception)) @@ -402,6 +404,7 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen cur_privilege = del_priv; + zicfilp_preserve_elp(del_priv); handle_trap_extension(del_priv, pc, ext); if get_config_print_reg() @@ -427,6 +430,7 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen cur_privilege = del_priv; + zicfilp_preserve_elp(del_priv); handle_trap_extension(del_priv, pc, ext); if get_config_print_reg() @@ -447,6 +451,7 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen cur_privilege = del_priv; + zicfilp_preserve_elp(del_priv); handle_trap_extension(del_priv, pc, ext); if get_config_print_reg() @@ -457,6 +462,10 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen }; } +/* Zicfilp : extension to restore elp */ +val zicfilp_set_elp_to_mpelp : (unit) -> unit +val zicfilp_set_elp_to_spelp : (unit) -> unit + function exception_handler(cur_priv : Privilege, ctl : ctl_result, pc: xlenbits) -> xlenbits = { match (cur_priv, ctl) { @@ -476,6 +485,9 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result, if cur_privilege != Machine then mstatus[MPRV] = 0b0; + /* Zicfilp: extension to restore ELP */ + zicfilp_set_elp_to_mpelp(); + if get_config_print_reg() then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits)); if get_config_print_platform() @@ -493,6 +505,9 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result, if cur_privilege != Machine then mstatus[MPRV] = 0b0; + /* Zicfilp: extension to restore ELP */ + zicfilp_set_elp_to_spelp(); + if get_config_print_reg() then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits)); if get_config_print_platform()