Expected Landing Pad (ELP) state management

- JALR updates ELP to LP expected on indirect call/jump - Traps preserve ELP state in mstatus.xPELP on trap delivery priv x - xRET restores ELP from mstatus.xPELP - If instruction fetched not LPAD when ELP is LP_EXPECTED cause SW check fault
riscv · Feb 7, 2024 · 85217d5 · 85217d5
1 parent 1719a31
commit 85217d5
Show file tree

Hide file tree

Showing 4 changed files with 46 additions and 9 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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()