aboutsummaryrefslogtreecommitdiff
path: root/model/extensions
diff options
context:
space:
mode:
Diffstat (limited to 'model/extensions')
-rw-r--r--model/extensions/cfi/zicfilp_regs.sail4
1 files changed, 4 insertions, 0 deletions
diff --git a/model/extensions/cfi/zicfilp_regs.sail b/model/extensions/cfi/zicfilp_regs.sail
index ee8d3cf..6d15680 100644
--- a/model/extensions/cfi/zicfilp_regs.sail
+++ b/model/extensions/cfi/zicfilp_regs.sail
@@ -32,6 +32,10 @@ function get_xLPE(p : Privilege) -> bool =
VirtualUser => internal_error(__FILE__, __LINE__, "Hypervisor extension not supported"),
}
+// This measure needs to be > currentlyEnabled_measure(Ext_S), currently equal
+// to 1, see currentlyEnabled_measure in extensions.sail
+termination_measure get_xLPE(_) = 2
+
function clause currentlyEnabled(Ext_Zicfilp) =
currentlyEnabled(Ext_Zicsr) & hartSupports(Ext_Zicfilp) & get_xLPE(cur_privilege)