Implement fetch to properly handle RVC and address translation, and add a step function for execution.

4 files changed, 93 insertions, 1 deletions

diff --git a/riscv/Makefile b/riscv/Makefile
index 8695e42e..781ec354 100644
--- a/riscv/Makefile
+++ b/riscv/Makefile
@@ -1,4 +1,4 @@
-SAIL_SRCS = prelude.sail riscv_types.sail riscv_mem.sail riscv_sys.sail riscv_vmem.sail riscv.sail
+SAIL_SRCS = prelude.sail riscv_types.sail riscv_mem.sail riscv_sys.sail riscv_vmem.sail riscv.sail riscv_step.sail
 SAIL_DIR ?= $(realpath ..)
 
 export SAIL_DIR
diff --git a/riscv/riscv_step.sail b/riscv/riscv_step.sail
new file mode 100644
index 00000000..ca0e102a
--- /dev/null
+++ b/riscv/riscv_step.sail
@@ -0,0 +1,84 @@
+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))
+                }
+              }
+            }
+          }
+        }
+      }
+    }
+  }
+}
+
+val step : unit -> unit effect {barr, eamem, escape, exmem, rmem, rreg, wmv, wreg}
+function step() = {
+  tick_clock();
+
+  match curInterrupt(mip, mie, mideleg) {
+    Some(intr, priv) => {
+      ()
+    },
+    None() => {
+      match fetch() {
+        F_Error(e, addr) => handle_mem_exception(addr, e),
+        F_RVC(h) => {
+          match decodeCompressed(h) {
+            None() => {
+              print(BitStr(h) ^ " :  <no-decode>");
+              handle_decode_exception(EXTZ(h))
+            },
+            Some(ast) => {
+              print(BitStr(h) ^ " :  " ^ ast);
+              nextPC = PC + 2;
+              execute(ast)
+            }
+          }
+        },
+        F_Base(w) => {
+          match decode(w) {
+            None() => {
+              print(BitStr(w) ^ " :  <no-decode>");
+              handle_decode_exception(EXTZ(w))
+            },
+            Some(ast) => {
+              print(BitStr(w) ^ " :  " ^ ast);
+              nextPC = PC + 4;
+              execute(ast)
+            }
+          }
+        }
+      }
+    }
+  }
+}
diff --git a/riscv/riscv_sys.sail b/riscv/riscv_sys.sail
index e32836c7..e692e62d 100644
--- a/riscv/riscv_sys.sail
+++ b/riscv/riscv_sys.sail
@@ -687,6 +687,11 @@ function handle_mem_exception(addr : xlenbits, e : ExceptionType) -> unit = {
   nextPC = handle_exception_ctl(cur_privilege, CTL_TRAP(t), PC)
 }
 
+function handle_decode_exception(instbits : xlenbits) -> unit = {
+  let t : sync_exception = struct { trap = E_Illegal_Instr,
+                                    excinfo = Some(instbits) };
+  nextPC = handle_exception_ctl(cur_privilege, CTL_TRAP(t), PC)
+}
 
 function init_sys() -> unit = {
   cur_privilege = Machine;
diff --git a/riscv/riscv_types.sail b/riscv/riscv_types.sail
index 2bba652f..5d602d61 100644
--- a/riscv/riscv_types.sail
+++ b/riscv/riscv_types.sail
@@ -6,6 +6,9 @@ let xlen_max_unsigned = 2 ^ xlen - 1
 let xlen_max_signed = 2 ^ (xlen - 1) - 1
 let xlen_min_signed = 0 - 2 ^ (xlen - 1)
 
+type half = bits(16)
+type word = bits(32)
+
 type regno ('n : Int), 0 <= 'n < 32 = atom('n)
 type regbits = bits(5)
 type cregbits = bits(3)