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 · Mar 28, 2024 · b1c746a · b1c746a
1 parent 0ecece3
commit b1c746a
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
@@ -6,6 +6,9 @@
 /*  SPDX-License-Identifier: BSD-2-Clause                                                */
 /*=======================================================================================*/
 
+/* Zicfilp : Update ELP state */
+val zicfilp_update_elp : (regidx) -> unit
+
 /* The definition for the memory model. */
 
 function clause execute (RISCV_JALR(imm, rs1, rd)) = {
@@ -14,5 +17,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
@@ -6,6 +6,9 @@
 /*  SPDX-License-Identifier: BSD-2-Clause                                                */
 /*=======================================================================================*/
 
+/* Zicfilp : Update ELP state */
+val zicfilp_update_elp : (regidx) -> unit
+
 /* The definition for the sequential model. */
 
 function clause execute (RISCV_JALR(imm, rs1, rd)) = {
@@ -30,6 +33,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
@@ -53,14 +53,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);
@@ -69,8 +75,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
@@ -315,6 +315,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))
@@ -340,6 +342,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()
@@ -365,6 +368,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()
@@ -385,6 +389,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()
@@ -395,6 +400,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) {
@@ -414,6 +423,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()
@@ -431,6 +443,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()