work in progress riscv CSR implementation.

3 files changed, 89 insertions, 1 deletions

diff --git a/riscv/main.sail b/riscv/main.sail
new file mode 100644
index 00000000..f7099398
--- /dev/null
+++ b/riscv/main.sail
@@ -0,0 +1,24 @@
+val fetch_and_execute : unit -> unit effect {barr, eamem, escape, exmem, rmem, rreg, wmv, wreg}
+
+function break () : unit -> unit = ()
+
+function fetch_and_execute () = while true do {
+  let instr = __RISCV_read(PC, 4);
+  nextPC = PC + 4;
+  let instr_ast = decode(instr);
+  break ();
+  match instr_ast {
+    Some(ast) => execute(ast),
+    None      => exit (())
+  };
+  PC = nextPC
+}
+
+val elf_entry = "Elf_loader.elf_entry" : unit -> int
+
+val main : unit -> unit effect {barr, eamem, escape, exmem, rmem, rreg, wmv, wreg}
+
+function main () = {
+  PC = __GetSlice_int(64, elf_entry(), 0);
+  fetch_and_execute()
+}
diff --git a/riscv/riscv.sail b/riscv/riscv.sail
index f05bb2be..333eae94 100644
--- a/riscv/riscv.sail
+++ b/riscv/riscv.sail
@@ -382,6 +382,70 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
   };
 }
 
+union clause ast = CSR  : (bits(12), regbits, regbits, bool, csrop)
+
+function clause decode csr : bits(12) @ rs1 : regbits @ 0b001 @ rd : regbits @ 0b1110011 = Some(CSR (csr, rs1, rd, false, CSRRW))
+function clause decode csr : bits(12) @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b1110011 = Some(CSR (csr, rs1, rd, false, CSRRS))
+function clause decode csr : bits(12) @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b1110011 = Some(CSR (csr, rs1, rd, false, CSRRC))
+function clause decode csr : bits(12) @ rs1 : regbits @ 0b101 @ rd : regbits @ 0b1110011 = Some(CSR (csr, rs1, rd, true,  CSRRW))
+function clause decode csr : bits(12) @ rs1 : regbits @ 0b110 @ rd : regbits @ 0b1110011 = Some(CSR (csr, rs1, rd, true,  CSRRS))
+function clause decode csr : bits(12) @ rs1 : regbits @ 0b111 @ rd : regbits @ 0b1110011 = Some(CSR (csr, rs1, rd, true,  CSRRC))
+
+val isCSRImplemented : bits(12) -> bool
+function isCSRImplemented csr : bits(12) -> bool =
+  match csr {
+    0xf11 => true, // mvendorid
+    0xf12 => true, // marchdid
+    0xf13 => true, // mimpid
+    0xf14 => true, // mhartid
+    0x300 => true, // mstatus
+    0x301 => true, // misa
+    0x302 => true, // medeleg
+    0x303 => true, // mideleg
+    0x304 => true, // mie
+    0x305 => true, // mtvec
+    0x306 => true, // mcounteren
+    0x340 => true, // mscratch
+    0x341 => true, // mepc
+    0x342 => true, // mcause
+    0x343 => true, // mtval
+    0x344 => true, // mip
+    _     => false
+  }
+
+function readCSR csr: bits(12) -> bits(64) = 0x0000_0000_0000_0000
+
+function writeCSR (csr : bits(12), value : bits(64)) -> unit = ()
+
+function haveCSRPriv (csr : bits(12), isWrite : bool) -> bool =
+  let isRO = csr[11..10] == 0b11 in
+  ~ (isRO & isWrite) /* XXX TODO check priv */
+
+val signalIllegalInstruction : unit -> unit effect {escape}
+function signalIllegalInstruction () = not_implemented ("illegal instruction")
+
+function clause execute CSR(csr, rs1, rd, is_imm, op) =
+  let rs1_val : bits(64) = if is_imm then EXTZ(rs1) else rGPR(rs1) in
+  let isWrite : bool = match op {
+    CSRRW  => true,
+    CSRRWI => true,
+    _      => if is_imm then unsigned(rs1_val) != 0 else unsigned(rs1) != 0
+  } in
+  if ~ (isCSRImplemented(csr) & haveCSRPriv(csr, isWrite)) then
+    signalIllegalInstruction ()
+  else {
+    let csr_val = readCSR(csr); /* could have side-effects, so technically shouldn't perform for CSRW[I] with rd == 0 */
+    if isWrite then {
+      let new_val : bits(64) = match op {
+        CSRRW => rs1_val,
+        CSRRS => csr_val | rs1_val,
+        CSRRC => csr_val & ~(rs1_val)
+      } in
+      writeCSR(csr, new_val)
+    };
+    wGPR(rd, csr_val)
+  }
+
 /* ****************************************************************** */
 
 function clause decode _ = None
diff --git a/riscv/riscv_types.sail b/riscv/riscv_types.sail
index d338bab9..dbec6266 100644
--- a/riscv/riscv_types.sail
+++ b/riscv/riscv_types.sail
@@ -180,7 +180,7 @@ enum sop = {RISCV_SLLI, RISCV_SRLI, RISCV_SRAI} /* shift ops */
 enum rop = {RISCV_ADD, RISCV_SUB, RISCV_SLL, RISCV_SLT, RISCV_SLTU, RISCV_XOR, RISCV_SRL, RISCV_SRA, RISCV_OR, RISCV_AND} /* reg-reg ops */
 enum ropw = {RISCV_ADDW, RISCV_SUBW, RISCV_SLLW, RISCV_SRLW, RISCV_SRAW} /* reg-reg 32-bit ops */
 enum amoop = {AMOSWAP, AMOADD, AMOXOR, AMOAND, AMOOR, AMOMIN, AMOMAX, AMOMINU, AMOMAXU} /* AMO ops */
-
+enum csrop = {CSRRW, CSRRS, CSRRC}
 enum word_width = {BYTE, HALF, WORD, DOUBLE}
 
 /* Ideally these would be sail builtin */