diff options
| -rw-r--r-- | riscv/riscv.sail | 26 | ||||
| -rw-r--r-- | riscv/riscv_sys.sail | 61 | ||||
| -rw-r--r-- | riscv/riscv_types.sail | 8 |
3 files changed, 69 insertions, 26 deletions
diff --git a/riscv/riscv.sail b/riscv/riscv.sail index e5380bd2..0747d077 100644 --- a/riscv/riscv.sail +++ b/riscv/riscv.sail @@ -502,30 +502,6 @@ function clause decode csr : bits(12) @ rs1 : regbits @ 0b101 @ rd : regbits @ 0 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 - - // for riscv-tests - 0x180 => true, // satp - _ => false - } function readCSR csr: bits(12) -> xlenbits = match csr { @@ -611,7 +587,7 @@ function clause execute CSR(csr, rs1, rd, is_imm, op) = CSRRW => true, _ => if is_imm then unsigned(rs1_val) != 0 else unsigned(rs1) != 0 } in - if ~ (isCSRImplemented(csr) & haveCSRPriv(csr, isWrite)) then { + if ~ (check_CSR(csr, cur_privilege, isWrite)) then { let instr : xlenbits = EXTZ(__RISCV_read(PC, 4)); let t : sync_exception = struct { trap = E_Illegal_Instr, diff --git a/riscv/riscv_sys.sail b/riscv/riscv_sys.sail index dfad6f51..b3ded01e 100644 --- a/riscv/riscv_sys.sail +++ b/riscv/riscv_sys.sail @@ -196,6 +196,67 @@ register scause : Mcause register stval : xlenbits register satp : xlenbits +/* csr access control */ + +function csrAccess(csr : csreg) -> csrRW = csr[11..10] +function csrPriv(csr : csreg) -> priv_level = csr[9..8] + +function is_CSR_defined (csr : bits(12), p : Privilege) -> bool = + match (csr) { + /* machine mode: informational */ + 0xf11 => p == Machine, // mvendorid + 0xf12 => p == Machine, // marchdid + 0xf13 => p == Machine, // mimpid + 0xf14 => p == Machine, // mhartid + /* machine mode: trap setup */ + 0x300 => p == Machine, // mstatus + 0x301 => p == Machine, // misa + 0x302 => p == Machine, // medeleg + 0x303 => p == Machine, // mideleg + 0x304 => p == Machine, // mie + 0x305 => p == Machine, // mtvec + 0x306 => p == Machine, // mcounteren + /* machine mode: trap handling */ + 0x340 => p == Machine, // mscratch + 0x341 => p == Machine, // mepc + 0x342 => p == Machine, // mcause + 0x343 => p == Machine, // mtval + 0x344 => p == Machine, // mip + + /* supervisor mode: trap setup */ + 0x100 => p == Machine | p == Supervisor, // sstatus + 0x102 => p == Machine | p == Supervisor, // sedeleg + 0x103 => p == Machine | p == Supervisor, // sideleg + 0x104 => p == Machine | p == Supervisor, // sie + 0x105 => p == Machine | p == Supervisor, // stvec + 0x106 => p == Machine | p == Supervisor, // scounteren + + /* supervisor mode: trap handling */ + 0x140 => p == Machine | p == Supervisor, // sscratch + 0x141 => p == Machine | p == Supervisor, // sepc + 0x142 => p == Machine | p == Supervisor, // scause + 0x143 => p == Machine | p == Supervisor, // stval + 0x144 => p == Machine | p == Supervisor, // sip + + /* supervisor mode: address translation */ + 0x180 => p == Machine | p == Supervisor, // satp + + _ => false + } + +val check_CSR_access : (csrRW, priv_level, Privilege, bool) -> bool +function check_CSR_access(csrrw, csrpr, p, isWrite) = + (~ (isWrite == true & csrrw == 0b11)) /* read/write */ + & (privLevel_to_bits(p) >=_u csrpr) /* privilege */ + +function check_TVM_SATP(csr : csreg, p : Privilege) -> bool = + ~ (csr == 0x180 & p == Supervisor & mstatus.TVM() == true) + +function check_CSR(csr : csreg, p : Privilege, isWrite : bool) -> bool = + is_CSR_defined(csr, p) + & check_CSR_access(csrAccess(csr), csrPriv(csr), p, isWrite) + & check_TVM_SATP(csr, p) + /* instruction control flow */ struct sync_exception = { diff --git a/riscv/riscv_types.sail b/riscv/riscv_types.sail index a858c317..f64eb5a9 100644 --- a/riscv/riscv_types.sail +++ b/riscv/riscv_types.sail @@ -9,6 +9,7 @@ let xlen_min_signed = 0 - 2 ^ (xlen - 1) type regno ('n : Int), 0 <= 'n < 32 = atom('n) type regbits = bits(5) type cregbits = bits(3) +type csreg = bits(12) val cast regbits_to_regno : bits(5) -> {'n, 0 <= 'n < 32. regno('n)} function regbits_to_regno b = let 'r = unsigned(b) in r @@ -55,7 +56,6 @@ enum Architecture = {RV32, RV64, RV128} /* privilege levels */ type priv_level = bits(2) - enum Privilege = {User, Supervisor, Machine} val cast privLevel_to_bits : Privilege -> priv_level @@ -85,6 +85,10 @@ function privLevel_to_str (p) = { } } +/* access types */ +enum AccessType = {Read, Write, ReadWrite, Execute} +enum ReadType = {Instruction, Data} + /* architectural exception and interrupt definitions */ type exc_code = bits(4) @@ -323,6 +327,8 @@ val MEM_fence_r_r = {ocaml: "skip", lem: "MEM_fence_r_r"} : unit -> unit eff val MEM_fence_rw_w = {ocaml: "skip", lem: "MEM_fence_rw_w"} : unit -> unit effect {barr} val MEM_fence_w_w = {ocaml: "skip", lem: "MEM_fence_w_w"} : unit -> unit effect {barr} val MEM_fence_i = {ocaml: "skip", lem: "MEM_fence_i"} : unit -> unit effect {barr} +/* CSR access control bits (from CSR addresses) */ +type csrRW = bits(2) /* read/write */ enum uop = {RISCV_LUI, RISCV_AUIPC} /* upper immediate ops */ enum bop = {RISCV_BEQ, RISCV_BNE, RISCV_BLT, RISCV_BGE, RISCV_BLTU, RISCV_BGEU} /* branch ops */ |