Add and use execute_branch and execute_branch_pcc functions to align code with existing MIPS and CHERI specs.

1 files changed, 6 insertions, 0 deletions

diff --git a/mips/mips_prelude.sail b/mips/mips_prelude.sail
index b672d993..3c3c45f4 100644
--- a/mips/mips_prelude.sail
+++ b/mips/mips_prelude.sail
@@ -289,6 +289,12 @@ register branchPending : bits(1)      /* Set by branch instructions to implement
 register inBranchDelay : bits(1)      /* Needs to be set by outside world when in branch delay slot */
 register delayedPC : bits(64)          /* Set by branch instructions to implement branch delay */
 
+val execute_branch : bits(64) -> unit effect {wreg}
+function execute_branch(pc) = {
+  delayedPC = pc;
+  branchPending = 0b1;
+}
+
 /* General purpose registers */