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

2 files changed, 12 insertions, 12 deletions

diff --git a/mips/mips_insts.sail b/mips/mips_insts.sail
index 028665c9..885608d1 100644
--- a/mips/mips_insts.sail
+++ b/mips/mips_insts.sail
@@ -884,8 +884,7 @@ function clause decode (0b000010 @ offset : bits(26)) =
   Some(J(offset))
 function clause execute (J(offset)) =
   {
-    delayedPC     = (PC + 4)[63..28] @ offset @ 0b00;
-    branchPending = 0b1
+    execute_branch((PC + 4)[63..28] @ offset @ 0b00);
   }
 
 /* JAL    - jump and link */
@@ -894,8 +893,7 @@ function clause decode (0b000011 @ offset : bits(26)) =
   Some(JAL(offset))
 function clause execute (JAL(offset)) =
   {
-    delayedPC     = (PC + 4)[63..28] @ offset @ 0b00;
-    branchPending = 0b1;
+    execute_branch((PC + 4)[63..28] @ offset @ 0b00);
     wGPR(0b11111) = PC + 8;
   }
 
@@ -905,8 +903,7 @@ function clause decode (0b000000 @ rs : regno @ 0b00000 @ 0b00000 @ hint : regno
   Some(JR(rs)) /* hint is ignored */
 function clause execute (JR(rs)) =
   {
-    delayedPC     = rGPR(rs);
-    branchPending = 0b1;
+    execute_branch(rGPR(rs));
   }
 
 /* JALR -- jump via register with link */
@@ -915,8 +912,7 @@ function clause decode (0b000000 @ rs : regno @ 0b00000 @ rd : regno @ hint : re
   Some(JALR(rs, rd)) /* hint is ignored */
 function clause execute (JALR(rs, rd)) =
   {
-    delayedPC     = rGPR(rs);
-    branchPending = 0b1;
+    execute_branch(rGPR(rs));
     wGPR(rd)      = PC + 8;
   }
 
@@ -939,8 +935,7 @@ function clause execute (BEQ(rs, rd, imm, ne, likely)) =
     if ((rGPR(rs) == rGPR(rd)) ^ ne) then
       {
         let offset : bits(64) = (sign_extend(imm @ 0b00) + 4) in
-        delayedPC     = PC + offset;
-        branchPending = 0b1;
+        execute_branch(PC + offset);
       }
     else
       {
@@ -996,8 +991,7 @@ function clause execute (BCMPZ(rs, imm, cmp, link, likely)) =
     if (condition) then
       {
         let offset : bits(64) = (sign_extend(imm @ 0b00) + 4) in
-        delayedPC     =  PC + offset;
-        branchPending = 0b1;
+        execute_branch(PC + offset);
       }
     else if (likely) then
       {
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 */