aboutsummaryrefslogtreecommitdiff
path: root/model
diff options
context:
space:
mode:
authorPrashanth Mundkur <prashanth.mundkur@gmail.com>2019-05-24 14:22:18 -0700
committerPrashanth Mundkur <prashanth.mundkur@gmail.com>2019-05-24 14:22:18 -0700
commit4799f996fc5b27f53a93a521db7ff2f54a5d3558 (patch)
tree50c08636282e19f57e7a6b7bd6c9616c9752f610 /model
parente49783404e8139b7a7bb2974af13b3d8a72da48d (diff)
downloadsail-riscv-4799f996fc5b27f53a93a521db7ff2f54a5d3558.zip
sail-riscv-4799f996fc5b27f53a93a521db7ff2f54a5d3558.tar.gz
sail-riscv-4799f996fc5b27f53a93a521db7ff2f54a5d3558.tar.bz2
Make xret hooks differentiate between just reading xret target values and getting the value when transferring control to the xret target.
Diffstat (limited to 'model')
-rw-r--r--model/riscv_sys_control.sail6
-rw-r--r--model/riscv_sys_exceptions.sail12
2 files changed, 14 insertions, 4 deletions
diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail
index 6bee610..e866986 100644
--- a/model/riscv_sys_control.sail
+++ b/model/riscv_sys_control.sail
@@ -366,7 +366,7 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result,
print_platform("ret-ing from " ^ prev_priv ^ " to " ^ cur_privilege);
cancel_reservation();
- get_xret_target(Machine) & pc_alignment_mask()
+ prepare_xret_target(Machine) & pc_alignment_mask()
},
(_, CTL_SRET()) => {
let prev_priv = cur_privilege;
@@ -380,7 +380,7 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result,
print_platform("ret-ing from " ^ prev_priv ^ " to " ^ cur_privilege);
cancel_reservation();
- get_xret_target(Supervisor) & pc_alignment_mask()
+ prepare_xret_target(Supervisor) & pc_alignment_mask()
},
(_, CTL_URET()) => {
let prev_priv = cur_privilege;
@@ -392,7 +392,7 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result,
print_platform("ret-ing from " ^ prev_priv ^ " to " ^ cur_privilege);
cancel_reservation();
- get_xret_target(User) & pc_alignment_mask()
+ prepare_xret_target(User) & pc_alignment_mask()
}
}
}
diff --git a/model/riscv_sys_exceptions.sail b/model/riscv_sys_exceptions.sail
index d2be25f..94d869e 100644
--- a/model/riscv_sys_exceptions.sail
+++ b/model/riscv_sys_exceptions.sail
@@ -17,7 +17,13 @@ function prepare_trap_vector(p : Privilege, cause : Mcause) -> xlenbits = {
}
}
-/* used for xRET */
+/* xRET handling involves three functions:
+ *
+ * get_xret_target: used to read the value of the xret target (no control flow transfer)
+ * set_xret_target: used to write a value of the xret target (no control flow transfer)
+ * prepare_xret_target: used to get the value for control transfer to the xret target
+ */
+
val get_xret_target : Privilege -> xlenbits effect {rreg}
function get_xret_target(p) =
match p {
@@ -37,6 +43,10 @@ function set_xret_target(p, value) = {
target
}
+val prepare_xret_target : (Privilege) -> xlenbits effect {rreg, wreg}
+function prepare_xret_target(p) =
+ get_xret_target(p)
+
/* other trap-related CSRs */
function get_mtvec() -> xlenbits =