1 files changed, 92 insertions, 0 deletions
diff --git a/riscv/riscv_step.sail b/riscv/riscv_step.sail
new file mode 100644
index 00000000..7ddd8a44
--- /dev/null
+++ b/riscv/riscv_step.sail
@@ -0,0 +1,92 @@
+union FetchResult = {
+  F_Base : word,                       /* Base ISA */
+  F_RVC : half,                        /* Compressed ISA */
+  F_Error : (ExceptionType, xlenbits)  /* exception and PC */
+}
+
+function isRVC(h : half) -> bool =
+ ~ (h[1 .. 0] == 0b11)
+
+val fetch : unit -> FetchResult effect {escape, rmem, rreg, wmv, wreg}
+function fetch() -> FetchResult = {
+  /* check for legal PC */
+  if (PC[0] != 0b0 | (PC[1] != 0b0 & (~ (haveRVC()))))
+  then F_Error(E_Fetch_Addr_Align, PC)
+  else match translateAddr(PC, Execute, Instruction) {
+    TR_Failure(e)  => F_Error(e, PC),
+    TR_Address(ppclo) => {
+      /* split instruction fetch into 16-bit granules to handle RVC, as
+       * well as to generate precise fault addresses in any fetch
+       * exceptions.
+       */
+      match checked_mem_read(Instruction, ppclo, 2) {
+        MemException(e) => F_Error(E_Fetch_Access_Fault, PC),
+        MemValue(ilo) => {
+          if isRVC(ilo) then F_RVC(ilo)
+          else {
+            PChi : xlenbits = PC + 2;
+            match translateAddr(PChi, Execute, Instruction) {
+              TR_Failure(e) => F_Error(e, PChi),
+              TR_Address(ppchi) => {
+                match checked_mem_read(Instruction, ppchi, 2) {
+                  MemException(e) => F_Error(E_Fetch_Access_Fault, PChi),
+                  MemValue(ihi) => F_Base(append(ihi, ilo))
+                }
+              }
+            }
+          }
+        }
+      }
+    }
+  }
+}
+
+/* returns whether an instruction was executed */
+val step : unit -> bool effect {barr, eamem, escape, exmem, rmem, rreg, wmv, wreg}
+function step() = {
+  match curInterrupt(mip, mie, mideleg) {
+    Some(intr, priv) => {
+      print_bits("Handling interrupt: ", intr);
+      handle_interrupt(intr, priv);
+      false
+    },
+    None() => {
+      match fetch() {
+        F_Error(e, addr) => {
+          handle_mem_exception(addr, e);
+          false
+        },
+        F_RVC(h) => {
+          match decodeCompressed(h) {
+            None() => {
+              print("PC: " ^ BitStr(PC) ^ " instr: " ^ BitStr(h) ^ " :  <no-decode>");
+              handle_decode_exception(EXTZ(h));
+              false
+            },
+            Some(ast) => {
+              print("PC: " ^ BitStr(PC) ^ " instr: " ^ BitStr(h) ^ " :  " ^ ast);
+              nextPC = PC + 2;
+              execute(ast);
+              true
+            }
+          }
+        },
+        F_Base(w) => {
+          match decode(w) {
+            None() => {
+              print("PC: " ^ BitStr(PC) ^ " instr: " ^ BitStr(w) ^ " :  <no-decode>");
+              handle_decode_exception(EXTZ(w));
+              false
+            },
+            Some(ast) => {
+              print("PC: " ^ BitStr(PC) ^ " instr: " ^ BitStr(w) ^ " :  " ^ ast);
+              nextPC = PC + 4;
+              execute(ast);
+              true
+            }
+          }
+        }
+      }
+    }
+  }
+}