diff options
Diffstat (limited to 'riscv')
| -rw-r--r-- | riscv/Makefile | 6 | ||||
| -rw-r--r-- | riscv/main.sail | 61 | ||||
| -rw-r--r-- | riscv/riscv.sail | 355 | ||||
| -rw-r--r-- | riscv/riscv_duopod.sail | 6 | ||||
| -rw-r--r-- | riscv/riscv_step.sail | 92 | ||||
| -rw-r--r-- | riscv/riscv_sys.sail | 86 | ||||
| -rw-r--r-- | riscv/riscv_types.sail | 26 | ||||
| -rw-r--r-- | riscv/riscv_vmem.sail | 240 |
8 files changed, 648 insertions, 224 deletions
diff --git a/riscv/Makefile b/riscv/Makefile index 27d9e4b1..d9c3f901 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 ..) SAIL ?= $(SAIL_DIR)/sail @@ -35,6 +35,10 @@ Riscv.thy: riscv.lem riscv_extras.lem riscv.lem: $(SAIL_SRCS) Makefile $(SAIL) $(SAIL_FLAGS) -lem -o riscv -lem_mwords -lem_lib Riscv_extras $(SAIL_SRCS) +# we exclude prelude.sail here, most code there should move to sail lib +LOC_FILES:=$(SAIL_SRCS) main.sail +include ../etc/loc.mk + clean: -rm -rf riscv _sbuild -rm -f riscv.lem riscv_types.lem diff --git a/riscv/main.sail b/riscv/main.sail index b6484755..28afe5ac 100644 --- a/riscv/main.sail +++ b/riscv/main.sail @@ -5,50 +5,18 @@ val elf_tohost = { c: "elf_tohost" } : unit -> int -function fetch_and_execute () = - let tohost = __GetSlice_int(64, elf_tohost(), 0) in +val loop : unit -> unit effect {barr, eamem, escape, exmem, rmem, rreg, wmv, wreg} +function loop () = { + let tohost = __GetSlice_int(64, elf_tohost(), 0); + i : int = 0; while true do { - print_bits("\nPC: ", PC); + tick_clock(); + print_int("\nstep: ", i); + let retired : bool = step(); + PC = nextPC; + if retired then i = i + 1; - /* for now, always fetch a 32-bit value. this would need to - change with privileged mode, since we could cross a page - boundary with PC only 16-bit aligned in C mode. */ - let irdval = checked_mem_read(Instruction, PC, 4); - match (irdval) { - MemValue(instr) => { - let (instr_ast, instr_sz) : (option(ast), int) = - match (instr[1 .. 0]) { - 0b11 => { cur_inst = EXTZ(instr); - (decode(instr), 4) - }, - _ => { cur_inst = EXTZ(instr[15 .. 0]); - (decodeCompressed(instr[15 .. 0]), 2) - } - }; - match (instr_ast, instr_sz) { - (Some(ast), 4) => print(BitStr(instr) ^ ": " ^ ast), - (Some(ast), 2) => print(BitStr(instr[15 .. 0]) ^ ": " ^ ast), - (_, _) => print(BitStr(instr) ^ ": no-decode") - }; - /* check whether a compressed instruction is legal. */ - if (misa.C() == 0b0 & (instr_sz == 2)) then { - let t : sync_exception = struct { trap = E_Illegal_Instr, - excinfo = Some(cur_inst) } in - nextPC = handle_exception_ctl(cur_privilege, CTL_TRAP(t), PC) - } else { - nextPC = PC + instr_sz; - match instr_ast { - Some(ast) => execute(ast), - None() => {print("Decode failed"); exit()} - } - } - }, - MemException(e) => { - let t : sync_exception = struct { trap = e, - excinfo = Some(PC) } in - nextPC = handle_exception_ctl(cur_privilege, CTL_TRAP(t), PC) - } - }; + /* check htif exit */ let tohost_val = __ReadRAM(64, 4, 0x0000_0000_0000_0000, tohost); if unsigned(tohost_val) != 0 then { let exit_val = unsigned(tohost_val >> 0b1) in @@ -56,9 +24,9 @@ function fetch_and_execute () = print("SUCCESS") else print_int("FAILURE: ", exit_val); - exit (()); - }; - PC = nextPC + exit(()); + } + } } val elf_entry = { @@ -72,10 +40,9 @@ function main () = { PC = __GetSlice_int(64, elf_entry(), 0); try { init_sys (); - fetch_and_execute() + loop () } catch { Error_not_implemented(s) => print_string("Error: Not implemented: ", s), - Error_misaligned_access() => print("Error: misaligned_access"), Error_EBREAK() => print("EBREAK"), Error_internal_error() => print("Error: internal error") } diff --git a/riscv/riscv.sail b/riscv/riscv.sail index a40ec53f..ed640ad3 100644 --- a/riscv/riscv.sail +++ b/riscv/riscv.sail @@ -293,12 +293,16 @@ function process_load(rd, addr, value, is_unsigned) = } function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = - let addr : xlenbits = X(rs1) + EXTS(imm) in - match width { - BYTE => process_load(rd, addr, mem_read(addr, 1, aq, rl, false), is_unsigned), - HALF => process_load(rd, addr, mem_read(addr, 2, aq, rl, false), is_unsigned), - WORD => process_load(rd, addr, mem_read(addr, 4, aq, rl, false), is_unsigned), - DOUBLE => process_load(rd, addr, mem_read(addr, 8, aq, rl, false), is_unsigned) + let vaddr : xlenbits = X(rs1) + EXTS(imm) in + match translateAddr(vaddr, Read, Data) { + TR_Failure(e) => handle_mem_exception(vaddr, e), + TR_Address(addr) => + match width { + BYTE => process_load(rd, vaddr, mem_read(addr, 1, aq, rl, false), is_unsigned), + HALF => process_load(rd, vaddr, mem_read(addr, 2, aq, rl, false), is_unsigned), + WORD => process_load(rd, vaddr, mem_read(addr, 4, aq, rl, false), is_unsigned), + DOUBLE => process_load(rd, vaddr, mem_read(addr, 8, aq, rl, false), is_unsigned) + } } /* FIXME: aq/rl are getting dropped */ @@ -311,7 +315,8 @@ function clause print_insn (LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = (HALF, true) => "lhu ", (WORD, false) => "lw ", (WORD, true) => "lwu ", - (_, _) => "ld.bad " + (DOUBLE, false) => "ld ", + (DOUBLE, true) => "ldu " } in insn ^ rd ^ ", " ^ rs1 ^ ", " ^ BitStr(imm) @@ -323,29 +328,35 @@ function clause decode imm7 : bits(7) @ rs2 : regbits @ rs1 : regbits @ 0b001 @ function clause decode imm7 : bits(7) @ rs2 : regbits @ rs1 : regbits @ 0b010 @ imm5 : bits(5) @ 0b0100011 = Some(STORE(imm7 @ imm5, rs2, rs1, WORD, false, false)) function clause decode imm7 : bits(7) @ rs2 : regbits @ rs1 : regbits @ 0b011 @ imm5 : bits(5) @ 0b0100011 = Some(STORE(imm7 @ imm5, rs2, rs1, DOUBLE, false, false)) +/* NOTE: Currently, we only EA if address translation is successful. + This may need revisiting. */ function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) = - let addr : xlenbits = X(rs1) + EXTS(imm) in - let eares : MemoryOpResult(unit) = match width { - BYTE => mem_write_ea(addr, 1, aq, rl, false), - HALF => mem_write_ea(addr, 2, aq, rl, false), - WORD => mem_write_ea(addr, 4, aq, rl, false), - DOUBLE => mem_write_ea(addr, 8, aq, rl, false) - } in - match (eares) { - MemException(e) => handle_mem_exception(addr, e), - MemValue(_) => { - let rs2_val = X(rs2) in - let res : MemoryOpResult(unit) = match width { - BYTE => mem_write_value(addr, 1, rs2_val[7..0], aq, rl, false), - HALF => mem_write_value(addr, 2, rs2_val[15..0], aq, rl, false), - WORD => mem_write_value(addr, 4, rs2_val[31..0], aq, rl, false), - DOUBLE => mem_write_value(addr, 8, rs2_val, aq, rl, false) + let vaddr : xlenbits = X(rs1) + EXTS(imm) in + match translateAddr(vaddr, Write, Data) { + TR_Failure(e) => handle_mem_exception(vaddr, e), + TR_Address(addr) => + let eares : MemoryOpResult(unit) = match width { + BYTE => mem_write_ea(addr, 1, aq, rl, false), + HALF => mem_write_ea(addr, 2, aq, rl, false), + WORD => mem_write_ea(addr, 4, aq, rl, false), + DOUBLE => mem_write_ea(addr, 8, aq, rl, false) } in - match (res) { - MemValue(_) => (), - MemException(e) => handle_mem_exception(addr, e) + match (eares) { + MemException(e) => handle_mem_exception(addr, e), + MemValue(_) => { + let rs2_val = X(rs2) in + let res : MemoryOpResult(unit) = match width { + BYTE => mem_write_value(addr, 1, rs2_val[7..0], aq, rl, false), + HALF => mem_write_value(addr, 2, rs2_val[15..0], aq, rl, false), + WORD => mem_write_value(addr, 4, rs2_val[31..0], aq, rl, false), + DOUBLE => mem_write_value(addr, 8, rs2_val, aq, rl, false) + } in + match (res) { + MemValue(_) => (), + MemException(e) => handle_mem_exception(addr, e) + } + } } - } } /* FIXME: aq/rl are getting dropped */ @@ -581,7 +592,7 @@ function clause execute ECALL() = Machine => E_M_EnvCall }, excinfo = (None() : option(xlenbits)) } in - nextPC = handle_exception_ctl(cur_privilege, CTL_TRAP(t), PC) + nextPC = handle_exception(cur_privilege, CTL_TRAP(t), PC) function clause print_insn (ECALL()) = "ecall" @@ -591,8 +602,12 @@ union clause ast = MRET : unit function clause decode 0b0011000 @ 0b00010 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 = Some(MRET()) -function clause execute MRET() = - nextPC = handle_exception_ctl(cur_privilege, CTL_MRET(), PC) +function clause execute MRET() = { + if cur_privilege == Machine then + nextPC = handle_exception(cur_privilege, CTL_MRET(), PC) + else + handle_illegal() +} function clause print_insn (MRET()) = "mret" @@ -600,10 +615,16 @@ function clause print_insn (MRET()) = /* ****************************************************************** */ union clause ast = SRET : unit -function clause decode 0b0001000 @ 0b00010 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 = Some(MRET()) +function clause decode 0b0001000 @ 0b00010 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 = Some(SRET()) function clause execute SRET() = - nextPC = handle_exception_ctl(cur_privilege, CTL_SRET(), PC) + match cur_privilege { + User => handle_illegal(), + Supervisor => if mstatus.TSR() == true + then handle_illegal() + else nextPC = handle_exception(cur_privilege, CTL_SRET(), PC), + Machine => nextPC = handle_exception(cur_privilege, CTL_SRET(), PC) + } function clause print_insn (SRET()) = "sret" @@ -619,6 +640,48 @@ function clause print_insn (EBREAK()) = "ebreak" /* ****************************************************************** */ +union clause ast = WFI : unit + +function clause decode 0b000100000101 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 = Some(WFI()) + +function clause execute WFI() = { + match cur_privilege { + Machine => (), + Supervisor => if mstatus.TW() == true + then handle_illegal() + else (), + User => handle_illegal() + } +} + +function clause print_insn (WFI()) = + "wfi" + +/* ****************************************************************** */ +union clause ast = SFENCE_VMA : (regbits, regbits) + +function clause decode 0b0001001 @ rs2 : regbits @ rs1 : regbits @ 0b000 @ 0b00000 @ 0b1110011 = Some(SFENCE_VMA(rs1, rs2)) + +function clause execute SFENCE_VMA(rs1, rs2) = { + /* FIXME: spec leaves unspecified what happens if this is executed in M-mode. + We assume it is the same as S-mode, which is definitely wrong. + */ + if cur_privilege == User then handle_illegal() + else match (architecture(mstatus.SXL()), mstatus.TVM()) { + (Some(RV64), true) => handle_illegal(), + (Some(RV64), false) => { + let addr : option(vaddr39) = if rs1 == 0 then None() else Some(X(rs1)[38 .. 0]); + let asid : option(asid64) = if rs2 == 0 then None() else Some(X(rs2)[15 .. 0]); + flushTLB(asid, addr) + }, + (_, _) => internal_error("unimplemented sfence architecture") + } +} + +function clause print_insn (SFENCE_VMA(rs1, rs2)) = + "sfence.vma " ^ rs1 ^ ", " ^ rs2 + +/* ****************************************************************** */ union clause ast = LOADRES : (bool, bool, regbits, word_width, regbits) function clause decode 0b00010 @ [aq] @ [rl] @ 0b00000 @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0101111 = Some(LOADRES(aq, rl, rs1, WORD, rd)) @@ -627,11 +690,15 @@ function clause decode 0b00010 @ [aq] @ [rl] @ 0b00000 @ rs1 : regbits @ 0b011 @ val process_loadres : forall 'n, 0 < 'n <= 8. (regbits, xlenbits, MemoryOpResult(bits(8 * 'n)), bool) -> unit function clause execute(LOADRES(aq, rl, rs1, width, rd)) = - let addr : xlenbits = X(rs1) in - match width { - WORD => process_load(rd, addr, mem_read(addr, 4, aq, rl, true), false), - DOUBLE => process_load(rd, addr, mem_read(addr, 8, aq, rl, true), false), - _ => internal_error("LOADRES expected WORD or DOUBLE") + let vaddr : xlenbits = X(rs1) in + match translateAddr(vaddr, Read, Data) { + TR_Failure(e) => handle_mem_exception(vaddr, e), + TR_Address(addr) => + match width { + WORD => process_load(rd, addr, mem_read(addr, 4, aq, rl, true), false), + DOUBLE => process_load(rd, addr, mem_read(addr, 8, aq, rl, true), false), + _ => internal_error("LOADRES expected WORD or DOUBLE") + } } /* FIXME */ @@ -650,29 +717,36 @@ union clause ast = STORECON : (bool, bool, regbits, regbits, word_width, regbits function clause decode 0b00011 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0101111 = Some(STORECON(aq, rl, rs2, rs1, WORD, rd)) function clause decode 0b00011 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0101111 = Some(STORECON(aq, rl, rs2, rs1, DOUBLE, rd)) +/* NOTE: Currently, we only EA if address translation is successful. + This may need revisiting. */ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = { status : bits(1) = if speculate_conditional_success() then 0b0 else 0b1; X(rd) = EXTZ(status); if status == 0b1 then () else { - addr : xlenbits = X(rs1); - let eares : MemoryOpResult(unit) = match width { - WORD => mem_write_ea(addr, 4, aq, rl, true), - DOUBLE => mem_write_ea(addr, 8, aq, rl, true), - _ => internal_error("STORECON expected word or double") - }; - match (eares) { - MemException(e) => handle_mem_exception(addr, e), - MemValue(_) => { - rs2_val = X(rs2); - let res : MemoryOpResult(unit) = match width { - WORD => mem_write_value(addr, 4, rs2_val[31..0], aq, rl, true), - DOUBLE => mem_write_value(addr, 8, rs2_val, aq, rl, true), + vaddr : xlenbits = X(rs1); + match translateAddr(vaddr, Write, Data) { + TR_Failure(e) => handle_mem_exception(vaddr, e), + TR_Address(addr) => { + let eares : MemoryOpResult(unit) = match width { + WORD => mem_write_ea(addr, 4, aq, rl, true), + DOUBLE => mem_write_ea(addr, 8, aq, rl, true), _ => internal_error("STORECON expected word or double") - } in - match (res) { - MemValue(_) => (), - MemException(e) => handle_mem_exception(addr, e) + }; + match (eares) { + MemException(e) => handle_mem_exception(addr, e), + MemValue(_) => { + rs2_val = X(rs2); + let res : MemoryOpResult(unit) = match width { + WORD => mem_write_value(addr, 4, rs2_val[31..0], aq, rl, true), + DOUBLE => mem_write_value(addr, 8, rs2_val, aq, rl, true), + _ => internal_error("STORECON expected word or double") + } in + match (res) { + MemValue(_) => (), + MemException(e) => handle_mem_exception(addr, e) + } + } } } } @@ -711,49 +785,55 @@ function clause decode 0b11000 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0 function clause decode 0b11100 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0101111 = Some(AMO(AMOMAXU, aq, rl, rs2, rs1, WORD, rd)) function clause decode 0b11100 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0101111 = Some(AMO(AMOMAXU, aq, rl, rs2, rs1, DOUBLE, rd)) +/* NOTE: Currently, we only EA if address translation is successful. + This may need revisiting. */ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = { - addr : xlenbits = X(rs1); - - let eares : MemoryOpResult(unit) = match width { - WORD => mem_write_ea(addr, 4, aq & rl, rl, true), - DOUBLE => mem_write_ea(addr, 8, aq & rl, rl, true), - _ => internal_error ("AMO expected WORD or DOUBLE") - }; - match (eares) { - MemException(e) => handle_mem_exception(addr, e), - MemValue(_) => { - let rval : MemoryOpResult(xlenbits) = match width { - WORD => extend_value(false, mem_read(addr, 4, aq, aq & rl, true)), - DOUBLE => extend_value(false, mem_read(addr, 8, aq, aq & rl, true)), - _ => internal_error ("AMO expected WORD or DOUBLE") + vaddr : xlenbits = X(rs1); + match translateAddr(vaddr, ReadWrite, Data) { + TR_Failure(e) => handle_mem_exception(vaddr, e), + TR_Address(addr) => { + let eares : MemoryOpResult(unit) = match width { + WORD => mem_write_ea(addr, 4, aq & rl, rl, true), + DOUBLE => mem_write_ea(addr, 8, aq & rl, rl, true), + _ => internal_error ("AMO expected WORD or DOUBLE") }; - match (rval) { + match (eares) { MemException(e) => handle_mem_exception(addr, e), - MemValue(loaded) => { - rs2_val : xlenbits = X(rs2); - result : xlenbits = - match op { - AMOSWAP => rs2_val, - AMOADD => rs2_val + loaded, - AMOXOR => rs2_val ^ loaded, - AMOAND => rs2_val & loaded, - AMOOR => rs2_val | loaded, - - /* Have to convert number to vector here. Check this */ - AMOMIN => vector64(min(signed(rs2_val), signed(loaded))), - AMOMAX => vector64(max(signed(rs2_val), signed(loaded))), - AMOMINU => vector64(min(unsigned(rs2_val), unsigned(loaded))), - AMOMAXU => vector64(max(unsigned(rs2_val), unsigned(loaded))) - }; - - let wval : MemoryOpResult(unit) = match width { - WORD => mem_write_value(addr, 4, result[31..0], aq & rl, rl, true), - DOUBLE => mem_write_value(addr, 8, result, aq & rl, rl, true), - _ => internal_error("AMO expected WORD or DOUBLE") + MemValue(_) => { + let rval : MemoryOpResult(xlenbits) = match width { + WORD => extend_value(false, mem_read(addr, 4, aq, aq & rl, true)), + DOUBLE => extend_value(false, mem_read(addr, 8, aq, aq & rl, true)), + _ => internal_error ("AMO expected WORD or DOUBLE") }; - match (wval) { - MemValue(_) => X(rd) = loaded, - MemException(e) => handle_mem_exception(addr, e) + match (rval) { + MemException(e) => handle_mem_exception(addr, e), + MemValue(loaded) => { + rs2_val : xlenbits = X(rs2); + result : xlenbits = + match op { + AMOSWAP => rs2_val, + AMOADD => rs2_val + loaded, + AMOXOR => rs2_val ^ loaded, + AMOAND => rs2_val & loaded, + AMOOR => rs2_val | loaded, + + /* Have to convert number to vector here. Check this */ + AMOMIN => vector64(min(signed(rs2_val), signed(loaded))), + AMOMAX => vector64(max(signed(rs2_val), signed(loaded))), + AMOMINU => vector64(min(unsigned(rs2_val), unsigned(loaded))), + AMOMAXU => vector64(max(unsigned(rs2_val), unsigned(loaded))) + }; + + let wval : MemoryOpResult(unit) = match width { + WORD => mem_write_value(addr, 4, result[31..0], aq & rl, rl, true), + DOUBLE => mem_write_value(addr, 8, result, aq & rl, rl, true), + _ => internal_error("AMO expected WORD or DOUBLE") + }; + match (wval) { + MemValue(_) => X(rd) = loaded, + MemException(e) => handle_mem_exception(addr, e) + } + } } } } @@ -796,7 +876,7 @@ 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)) -function readCSR csr: bits(12) -> xlenbits = +function readCSR csr : csreg -> xlenbits = match csr { /* machine mode */ 0xF11 => mvendorid, @@ -804,6 +884,7 @@ function readCSR csr: bits(12) -> xlenbits = 0xF13 => mimpid, 0xF14 => mhartid, 0x300 => mstatus.bits(), + 0x301 => misa.bits(), 0x302 => medeleg.bits(), 0x303 => mideleg.bits(), 0x304 => mie.bits(), @@ -832,60 +913,60 @@ function readCSR csr: bits(12) -> xlenbits = 0xC01 => mtime, 0xC02 => minstret, + /* trigger/debug */ + 0x7a0 => ~(tselect), /* this indicates we don't have any trigger support */ + _ => { print_bits("unhandled read to CSR ", csr); 0x0000_0000_0000_0000 } } -function writeCSR (csr : bits(12), value : xlenbits) -> unit = +function writeCSR (csr : csreg, value : xlenbits) -> unit = + let res : option(xlenbits) = match csr { /* machine mode */ - 0x300 => mstatus = legalize_mstatus(mstatus, value), - 0x302 => medeleg = legalize_medeleg(medeleg, value), - 0x303 => mideleg = legalize_mideleg(mideleg, value), - 0x304 => mie = legalize_mie(mie, value), - 0x305 => mtvec = legalize_tvec(mtvec, value), - 0x340 => mscratch = value, - 0x341 => mepc = legalize_xepc(value), - 0x342 => mcause->bits() = value, - 0x343 => mtval = value, - 0x344 => mip = legalize_mip(mip, value), + 0x300 => { mstatus = legalize_mstatus(mstatus, value); Some(mstatus.bits()) }, + 0x302 => { medeleg = legalize_medeleg(medeleg, value); Some(medeleg.bits()) }, + 0x303 => { mideleg = legalize_mideleg(mideleg, value); Some(mideleg.bits()) }, + 0x304 => { mie = legalize_mie(mie, value); Some(mie.bits()) }, + 0x305 => { mtvec = legalize_tvec(mtvec, value); Some(mtvec.bits()) }, + 0x340 => { mscratch = value; Some(mscratch) }, + 0x341 => { mepc = legalize_xepc(value); Some(mepc) }, + 0x342 => { mcause->bits() = value; Some(mcause.bits()) }, + 0x343 => { mtval = value; Some(mtval) }, + 0x344 => { mip = legalize_mip(mip, value); Some(mip.bits()) }, /* supervisor mode */ - 0x100 => mstatus = legalize_sstatus(mstatus, value), - 0x102 => sedeleg = legalize_sedeleg(sedeleg, value), - 0x103 => sideleg->bits() = value, /* TODO: does this need legalization? */ - 0x104 => mie = legalize_sie(mie, mideleg, value), - 0x105 => stvec = legalize_tvec(stvec, value), - 0x140 => sscratch = value, - 0x141 => sepc = legalize_xepc(value), - 0x142 => scause->bits() = value, - 0x143 => stval = value, - 0x144 => mip = legalize_sip(mip, mideleg, value), - 0x180 => satp = legalize_satp(cur_Architecture(), satp, value), - - _ => print_bits("unhandled write to CSR ", csr) + 0x100 => { mstatus = legalize_sstatus(mstatus, value); Some(mstatus.bits()) }, + 0x102 => { sedeleg = legalize_sedeleg(sedeleg, value); Some(sedeleg.bits()) }, + 0x103 => { sideleg->bits() = value; Some(sideleg.bits()) }, /* TODO: does this need legalization? */ + 0x104 => { mie = legalize_sie(mie, mideleg, value); Some(mie.bits()) }, + 0x105 => { stvec = legalize_tvec(stvec, value); Some(stvec.bits()) }, + 0x140 => { sscratch = value; Some(sscratch) }, + 0x141 => { sepc = legalize_xepc(value); Some(sepc) }, + 0x142 => { scause->bits() = value; Some(scause.bits()) }, + 0x143 => { stval = value; Some(stval) }, + 0x144 => { mip = legalize_sip(mip, mideleg, value); Some(mip.bits()) }, + 0x180 => { satp = legalize_satp(cur_Architecture(), satp, value); Some(satp) }, + + /* trigger/debug */ + 0x7a0 => { tselect = value; Some(tselect) }, + + _ => None() + } in + match res { + Some(v) => print("CSR " ^ csr ^ " <- " ^ BitStr(v) ^ " (input: " ^ BitStr(value) ^ ")"), + None() => print_bits("unhandled write to CSR ", csr) } -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 : xlenbits = if is_imm then EXTZ(rs1) else X(rs1) in let isWrite : bool = match op { CSRRW => true, _ => if is_imm then unsigned(rs1_val) != 0 else unsigned(rs1) != 0 } in - if ~ (check_CSR(csr, cur_privilege, isWrite)) then { - let instr : xlenbits = cur_inst; - let t : sync_exception = - struct { trap = E_Illegal_Instr, - excinfo = Some (instr) } in - nextPC = handle_exception_ctl(cur_privilege, CTL_TRAP(t), PC) - } else { + if ~ (check_CSR(csr, cur_privilege, isWrite)) + then handle_illegal() + 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 : xlenbits = match op { @@ -908,7 +989,8 @@ function clause print_insn (CSR(csr, rs1, rd, is_imm, op)) = (CSRRC, true) => "csrrci ", (CSRRC, false) => "csrrc " } in - insn ^ rd ^ ", " ^ rs1 ^ ", " ^ csr_name(csr) + let rs1_str : string = if is_imm then BitStr(rs1) else reg_name_abi(rs1) in + insn ^ rd ^ ", " ^ rs1_str ^ ", " ^ csr_name(csr) /* ****************************************************************** */ union clause ast = NOP : unit @@ -928,12 +1010,7 @@ union clause ast = ILLEGAL : unit function clause decodeCompressed (0b0000 @ 0b00000 @ 0b00000 @ 0b00) : bits(16) = Some(ILLEGAL()) -function clause execute ILLEGAL() = { - let t : sync_exception = - struct { trap = E_Illegal_Instr, - excinfo = Some (EXTZ(0b0)) } in - nextPC = handle_exception_ctl(cur_privilege, CTL_TRAP(t), PC) -} +function clause execute ILLEGAL() = handle_illegal () function clause print_insn (ILLEGAL()) = "illegal" diff --git a/riscv/riscv_duopod.sail b/riscv/riscv_duopod.sail index 687c7e64..ddb4f6e5 100644 --- a/riscv/riscv_duopod.sail +++ b/riscv/riscv_duopod.sail @@ -5,6 +5,9 @@ type xlen_t = bits(64) type regno ('n : Int), 0 <= 'n < 32 = atom('n) type regbits = bits(5) +val zeros : forall 'n. atom('n) -> bits('n) +function zeros n = replicate_bits(0b0, n) + val cast regbits_to_regno : bits(5) -> {'n, 0 <= 'n < 32. regno('n)} function regbits_to_regno b = let r as atom(_) = unsigned(b) in r @@ -33,7 +36,8 @@ overload X = {rX, wX} /* Accessors for memory */ val MEMr : forall 'n. (xlen_t, atom('n)) -> bits(8 * 'n) effect {rmem} -function MEMr (addr, width) = __RISCV_read(addr, width) +function MEMr (addr, width) = + match __RISCV_read(addr, width) { Some(v) => v, None() => zeros(8 * width) } /* Instruction decode and execute */ enum iop = {RISCV_ADDI, RISCV_SLTI, RISCV_SLTIU, RISCV_XORI, RISCV_ORI, RISCV_ANDI} /* immediate ops */ 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 + } + } + } + } + } + } +} diff --git a/riscv/riscv_sys.sail b/riscv/riscv_sys.sail index e9428448..803531bd 100644 --- a/riscv/riscv_sys.sail +++ b/riscv/riscv_sys.sail @@ -218,7 +218,7 @@ function tvec_addr(m : Mtvec, c : Mcause) -> option(xlenbits) = { let base : xlenbits = m.Base() @ 0b00; match (trapVectorMode_of_bits(m.Mode())) { TV_Direct => Some(base), - TV_Vector => if mcause.IsInterrupt() == 0b1 /* FIXME: Why not already boolean? */ + TV_Vector => if c.IsInterrupt() == true then Some(base + (EXTZ(c.Cause()) << 0b10)) else Some(base), TV_Reserved => None() @@ -392,8 +392,9 @@ register satp : xlenbits function legalize_satp(a : Architecture, o : xlenbits, v : xlenbits) -> xlenbits = { let s = Mk_Satp64(v); match satpMode_of_bits(a, s.Mode()) { - None() => o, - Some(_) => s.bits() + None() => o, + Some(Sv32) => o, /* Sv32 is unsupported for now */ + Some(_) => s.bits() } } @@ -403,6 +404,9 @@ register sepc : xlenbits register scause : Mcause register stval : xlenbits +/* disabled trigger/debug module */ +register tselect : xlenbits + /* csr name printer */ val cast csr_name : csreg -> string @@ -465,6 +469,8 @@ function csr_name(csr) = { 0xB80 => "mcycleh", 0xB82 => "minstreth", /* TODO: other hpm counters and events */ + /* trigger/debug */ + 0x7a0 => "tselect", _ => "UNKNOWN" } } @@ -514,6 +520,9 @@ function is_CSR_defined (csr : bits(12), p : Privilege) -> bool = /* supervisor mode: address translation */ 0x180 => p == Machine | p == Supervisor, // satp + /* disabled trigger/debug module */ + 0x7a0 => p == Machine, + _ => false } @@ -609,47 +618,50 @@ function tval(excinfo : option(xlenbits)) -> xlenbits = { union ctl_result = { CTL_TRAP : sync_exception, -/* TODO: CTL_URET */ CTL_SRET : unit, CTL_MRET : unit +/* TODO: CTL_URET */ } -/* handle exceptional ctl flow by updating nextPC */ +/* handle exceptional ctl flow by updating nextPC and operating privilege */ -function handle_trap(curp : Privilege, e : sync_exception, - pc : xlenbits) -> xlenbits = { - let priv = exception_delegatee(e.trap, curp); - cur_privilege = priv; - match (priv) { +function handle_trap(del_priv : Privilege, intr : bool, c : exc_code, pc : xlenbits, info : option(xlenbits)) + -> xlenbits = { + print("handling " ^ (if intr then "int#" else "exc#") ^ BitStr(c) ^ " at priv " ^ del_priv ^ " with tval " ^ BitStr(tval(info))); + match (del_priv) { Machine => { - mcause->IsInterrupt() = false; - mcause->Cause() = EXTZ(exceptionType_to_bits(e.trap)); + mcause->IsInterrupt() = intr; + mcause->Cause() = EXTZ(c); mstatus->MPIE() = mstatus.MIE(); mstatus->MIE() = false; - mstatus->MPP() = privLevel_to_bits(curp); - mtval = tval(e.excinfo); + mstatus->MPP() = privLevel_to_bits(cur_privilege); + mtval = tval(info); mepc = pc; + cur_privilege = del_priv; + match tvec_addr(mtvec, mcause) { Some(epc) => epc, None() => internal_error("Invalid mtvec mode") } }, Supervisor => { - scause->IsInterrupt() = false; - scause->Cause() = EXTZ(exceptionType_to_bits(e.trap)); + scause->IsInterrupt() = intr; + scause->Cause() = EXTZ(c); mstatus->SPIE() = mstatus.SIE(); mstatus->SIE() = false; - mstatus->SPP() = match (curp) { + mstatus->SPP() = match (cur_privilege) { User => false, Supervisor => true, Machine => internal_error("invalid privilege for s-mode trap") }; - stval = tval(e.excinfo); + stval = tval(info); sepc = pc; + cur_privilege = del_priv; + match tvec_addr(stvec, scause) { Some(epc) => epc, None() => internal_error("Invalid stvec mode") @@ -657,35 +669,59 @@ function handle_trap(curp : Privilege, e : sync_exception, }, User => internal_error("the N extension is currently unsupported") - } + }; } -function handle_exception_ctl(cur_priv : Privilege, ctl : ctl_result, - pc: xlenbits) -> xlenbits = +function handle_exception(cur_priv : Privilege, ctl : ctl_result, + pc: xlenbits) -> xlenbits = { match (cur_priv, ctl) { - (_, CTL_TRAP(e)) => handle_trap(cur_priv, e, pc), + (_, CTL_TRAP(e)) => { + let del_priv = exception_delegatee(e.trap, cur_priv); + print("trapping from " ^ cur_priv ^ " to " ^ del_priv + ^ " to handle " ^ e.trap); + handle_trap(del_priv, false, e.trap, pc, e.excinfo) + }, (_, CTL_MRET()) => { + let prev_priv = cur_privilege; mstatus->MIE() = mstatus.MPIE(); mstatus->MPIE() = true; cur_privilege = privLevel_of_bits(mstatus.MPP()); mstatus->MPP() = privLevel_to_bits(User); + print("ret-ing from " ^ prev_priv ^ " to " ^ cur_privilege); mepc }, (_, CTL_SRET()) => { + let prev_priv = cur_privilege; mstatus->SIE() = mstatus.SPIE(); mstatus->SPIE() = true; cur_privilege = if mstatus.SPP() == true then Supervisor else User; mstatus->SPP() = false; + print("ret-ing from " ^ prev_priv ^ " to " ^ cur_privilege); sepc } } +} function handle_mem_exception(addr : xlenbits, e : ExceptionType) -> unit = { let t : sync_exception = struct { trap = e, excinfo = Some(addr) } in - nextPC = handle_exception_ctl(cur_privilege, CTL_TRAP(t), PC) + nextPC = handle_exception(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(cur_privilege, CTL_TRAP(t), PC) } +function handle_interrupt(i : InterruptType, del_priv : Privilege) -> unit = + nextPC = handle_trap(del_priv, true, i, PC, None()) + +function handle_illegal() -> unit = { + let t : sync_exception = struct { trap = E_Illegal_Instr, + excinfo = None() }; + nextPC = handle_exception(cur_privilege, CTL_TRAP(t), PC) +} function init_sys() -> unit = { cur_privilege = Machine; @@ -701,3 +737,7 @@ function init_sys() -> unit = { mhartid = EXTZ(0b0); } + +function tick_clock() -> unit = { + mcycle = mcycle + 1 +} diff --git a/riscv/riscv_types.sail b/riscv/riscv_types.sail index 2bba652f..ee0eb94d 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) @@ -191,6 +194,28 @@ function exceptionType_to_bits(e) = { } } +val cast exceptionType_to_str : ExceptionType -> string +function exceptionType_to_str(e) = { + match (e) { + E_Fetch_Addr_Align => "fisaligned-fetch", + E_Fetch_Access_Fault => "fetch-access-fault", + E_Illegal_Instr => "illegal-instruction", + E_Breakpoint => "breakpoint", + E_Load_Addr_Align => "misaligned-load", + E_Load_Access_Fault => "load-access-fault", + E_SAMO_Addr_Align => "misaliged-store/amo", + E_SAMO_Access_Fault => "store/amo-access-fault", + E_U_EnvCall => "u-call", + E_S_EnvCall => "s-call", + E_Reserved_10 => "reserved-0", + E_M_EnvCall => "m-call", + E_Fetch_Page_Fault => "fetch-page-fault", + E_Load_Page_Fault => "load-page-fault", + E_Reserved_14 => "reserved-1", + E_SAMO_Page_Fault => "store/amo-page-fault" + } +} + enum InterruptType = { I_U_Software, I_S_Software, @@ -234,7 +259,6 @@ function trapVectorMode_of_bits (m) = { union exception = { Error_not_implemented : string, - Error_misaligned_access : unit, Error_EBREAK : unit, Error_internal_error : unit } diff --git a/riscv/riscv_vmem.sail b/riscv/riscv_vmem.sail index 4419d5ac..7fddb047 100644 --- a/riscv/riscv_vmem.sail +++ b/riscv/riscv_vmem.sail @@ -27,7 +27,7 @@ function isInvalidPTE(p : pteAttribs) -> bool = { a.V() == false | (a.W() == true & a.R() == false) } -function checkPTEPermissions(ac : AccessType, priv : Privilege, mxr : bool, sum : bool, p : PTE_Bits) -> bool = { +function checkPTEPermission(ac : AccessType, priv : Privilege, mxr : bool, sum : bool, p : PTE_Bits) -> bool = { match (ac, priv) { (Read, User) => p.U() == true & (p.R() == true | (p.X() == true & mxr)), (Write, User) => p.U() == true & p.W() == true, @@ -103,6 +103,15 @@ bitfield SV39_PTE : pte39 = { BITS : 7 .. 0 } +/* ASID */ + +type asid64 = bits(16) + +function curAsid64() -> asid64 = { + let satp64 = Mk_Satp64(satp); + satp64.Asid() +} + /* Current page table base from satp */ function curPTB39() -> paddr39 = { let satp64 = Mk_Satp64(satp); @@ -119,7 +128,7 @@ union PTW_Result = { val walk39 : (vaddr39, AccessType, Privilege, bool, bool, paddr39, nat, bool) -> PTW_Result effect {rmem, escape} function walk39(vaddr, ac, priv, mxr, sum, ptb, level, global) -> PTW_Result = { let va = Mk_SV39_Vaddr(vaddr); - let pt_ofs : paddr39 = shiftl(EXTZ(shiftr(va.VPNi(), (level * SV39_LEVEL_BITS))[SV39_LEVEL_BITS .. 0]), + let pt_ofs : paddr39 = shiftl(EXTZ(shiftr(va.VPNi(), (level * SV39_LEVEL_BITS))[(SV39_LEVEL_BITS - 1) .. 0]), PTE39_LOG_SIZE); let pte_addr = ptb + pt_ofs; match (checked_mem_read(Data, EXTZ(pte_addr), 8)) { @@ -133,25 +142,232 @@ function walk39(vaddr, ac, priv, mxr, sum, ptb, level, global) -> PTW_Result = { PTW_Failure(PTW_Invalid_PTE) } else { if isPTEPtr(pbits) then { - if level == 0 then PTW_Failure(PTW_Invalid_PTE) - else walk39(vaddr, ac, priv, mxr, sum, EXTZ(pte.PPNi()), level - 1, is_global) + if level == 0 then { + /* last-level PTE contains a pointer instead of a leaf */ + PTW_Failure(PTW_Invalid_PTE) + } else { + /* walk down the pointer to the next level */ + walk39(vaddr, ac, priv, mxr, sum, EXTZ(shiftl(pte.PPNi(), PAGESIZE_BITS)), level - 1, is_global) + } } else { /* leaf PTE */ - if ~ (checkPTEPermissions(ac, priv, mxr, sum, pattr)) then + if ~ (checkPTEPermission(ac, priv, mxr, sum, pattr)) then { PTW_Failure(PTW_No_Permission) - else { + } else { if level > 0 then { /* superpage */ - let masked = pte.PPNi() & EXTZ(shiftl(0b1, level * SV39_LEVEL_BITS) - 1); - if masked != EXTZ(0b0) then + /* fixme hack: to get a mask of appropriate size */ + let mask = shiftl(pte.PPNi() ^ pte.PPNi() ^ EXTZ(0b1), level * SV39_LEVEL_BITS) - 1; + if (pte.PPNi() & mask) != EXTZ(0b0) then { + /* misaligned superpage mapping */ PTW_Failure(PTW_Misaligned) - else { - let ppn = pte.PPNi() | (EXTZ(va.VPNi()) & EXTZ(shiftl(0b1, level * SV39_LEVEL_BITS) - 1)); + } else { + /* add the appropriate bits of the VPN to the superpage PPN */ + let ppn = pte.PPNi() | (EXTZ(va.VPNi()) & mask); PTW_Success(append(ppn, va.PgOfs()), pte, pte_addr, level, is_global) } - } else - PTW_Success(append(pa, va.PgOfs()), pte, pte_addr, level, is_global) + } else { + /* normal leaf PTE */ + PTW_Success(append(pte.PPNi(), va.PgOfs()), pte, pte_addr, level, is_global) + } + } + } + } + } + } +} + +/* idealized TLB to model fence.vm and also speed up simulation. */ + +struct TLB39_Entry = { + asid : asid64, + global : bool, + vAddr : vaddr39, /* VPN */ + pAddr : paddr39, /* PPN */ + vMatchMask : vaddr39, /* matching mask for superpages */ + vAddrMask : vaddr39, /* selection mask for superpages */ + pte : SV39_PTE, /* permissions */ + pteAddr : paddr39, /* for dirty writeback */ + age : xlenbits +} + +/* the rreg effect is an artifact of using the cycle counter to provide the age */ +val make_TLB39_Entry : (asid64, bool, vaddr39, paddr39, SV39_PTE, nat, paddr39) -> TLB39_Entry effect {rreg} + +function make_TLB39_Entry(asid, global, vAddr, pAddr, pte, level, pteAddr) = { + let shift : nat = PAGESIZE_BITS + (level * SV39_LEVEL_BITS); + /* fixme hack: use a better idiom for masks */ + let vAddrMask : vaddr39 = shiftl(vAddr ^ vAddr ^ EXTZ(0b1), shift) - 1; + let vMatchMask : vaddr39 = ~ (vAddrMask); + struct { + asid = asid, + global = global, + pte = pte, + pteAddr = pteAddr, + vAddrMask = vAddrMask, + vMatchMask = vMatchMask, + vAddr = vAddr & vMatchMask, + pAddr = shiftl(shiftr(pAddr, shift), shift), + age = mcycle + } +} + +/* TODO: make this a vector or array of entries */ +let TLBEntries = 32 +register tlb39 : option(TLB39_Entry) + +val lookupTLB39 : (asid64, vaddr39) -> option((int, TLB39_Entry)) effect {rreg} +function lookupTLB39(asid, vaddr) = { + match tlb39 { + None() => None(), + Some(e) => if (e.global | (e.asid == asid)) + & (e.vAddr == (e.vMatchMask & vaddr)) + then Some((0, e)) + else None() + } +} + +val addToTLB39 : (asid64, vaddr39, paddr39, SV39_PTE, paddr39, nat, bool) -> unit effect {wreg, rreg} +function addToTLB39(asid, vAddr, pAddr, pte, pteAddr, level, global) = { + let ent = make_TLB39_Entry(asid, global, vAddr, pAddr, pte, level, pteAddr); + tlb39 = Some(ent) +} + +function writeTLB39(idx : int, ent : TLB39_Entry) -> unit = + tlb39 = Some(ent) + +val flushTLB : (option(asid64), option(vaddr39)) -> unit effect {rreg, wreg} +function flushTLB(asid, addr) = { + let ent : option(TLB39_Entry) = + match (tlb39, asid, addr) { + (None(), _, _) => None(), + (Some(e), None(), None()) => None(), + (Some(e), None(), Some(a)) => if e.vAddr == (e.vMatchMask & a) + then None() else Some(e), + (Some(e), Some(i), None()) => if (e.asid == i) & (~ (e.global)) + then None() else Some(e), + (Some(e), Some(i), Some(a)) => if (e.asid == i) & (e.vAddr == (a & e.vMatchMask)) + & (~ (e.global)) + then None() else Some(e) + }; + tlb39 = ent +} + +union TR39_Result = { + TR39_Address : paddr39, + TR39_Failure : PTW_Error +} + +let enable_dirty_update = false + +val translate39 : (vaddr39, AccessType, Privilege, bool, bool, nat) -> TR39_Result effect {rreg, wreg, wmv, escape, rmem} +function translate39(vAddr, ac, priv, mxr, sum, level) = { + let asid = curAsid64(); + match lookupTLB39(asid, vAddr) { + Some(idx, ent) => { + let pteBits = Mk_PTE_Bits(ent.pte.BITS()); + if ~ (checkPTEPermission(ac, priv, mxr, sum, pteBits)) + then TR39_Failure(PTW_No_Permission) + else { + match update_PTE_Bits(pteBits, ac) { + None() => TR39_Address(ent.pAddr | EXTZ(vAddr & ent.vAddrMask)), + Some(pbits) => { + if ~ (enable_dirty_update) + then { + /* pte needs dirty/accessed update but that is not enabled */ + TR39_Failure(PTW_PTE_Update) + } else { + /* update PTE entry and TLB */ + n_ent : TLB39_Entry = ent; + n_ent.pte = update_BITS(ent.pte, pbits.bits()); + writeTLB39(idx, n_ent); + /* update page table */ + match checked_mem_write(EXTZ(ent.pteAddr), 8, ent.pte.bits()) { + MemValue(_) => (), + MemException(e) => internal_error("invalid physical address in TLB") + }; + TR39_Address(ent.pAddr | EXTZ(vAddr & ent.vAddrMask)) + } + } + } + } + }, + None() => { + match walk39(vAddr, ac, priv, mxr, sum, curPTB39(), level, false) { + PTW_Failure(f) => TR39_Failure(f), + PTW_Success(pAddr, pte, pteAddr, level, global) => { + match update_PTE_Bits(Mk_PTE_Bits(pte.BITS()), ac) { + None() => { + addToTLB39(asid, vAddr, pAddr, pte, pteAddr, level, global); + TR39_Address(pAddr) + }, + Some(pbits) => + if ~ (enable_dirty_update) + then { + /* pte needs dirty/accessed update but that is not enabled */ + TR39_Failure(PTW_PTE_Update) + } else { + w_pte : SV39_PTE = update_BITS(pte, pbits.bits()); + match checked_mem_write(EXTZ(pteAddr), 8, w_pte.bits()) { + MemValue(_) => { + addToTLB39(asid, vAddr, pAddr, w_pte, pteAddr, level, global); + TR39_Address(pAddr) + }, + MemException(e) => { + /* pte is not in valid memory */ + TR39_Failure(PTW_Access) + } + } + } } } } } } } + +/* Address translation mode */ + +val translationMode : (Privilege) -> SATPMode effect {rreg, escape} +function translationMode(priv) = { + if priv == Machine then Sbare + else { + let arch = architecture(mstatus.SXL()); + match arch { + Some(RV64) => { + let mbits : satp_mode = Mk_Satp64(satp).Mode(); + match satpMode_of_bits(RV64, mbits) { + Some(m) => m, + None() => internal_error("invalid RV64 translation mode in satp") + } + }, + _ => internal_error("unsupported address translation arch") + } + } +} + +union TR_Result = { + TR_Address : xlenbits, + TR_Failure : ExceptionType +} + +/* Top-level address translation dispatcher */ + +val translateAddr : (xlenbits, AccessType, ReadType) -> TR_Result effect {escape, rmem, rreg, wmv, wreg} +function translateAddr(vAddr, ac, rt) = { + let effPriv : Privilege = match rt { + Instruction => cur_privilege, + Data => if mstatus.MPRV() == true + then privLevel_of_bits(mstatus.MPP()) + else cur_privilege + }; + let mxr : bool = mstatus.MXR() == true; + let sum : bool = mstatus.SUM() == true; + let mode : SATPMode = translationMode(effPriv); + match mode { + Sbare => TR_Address(vAddr), + SV39 => match translate39(vAddr[38 .. 0], ac, effPriv, mxr, sum, SV39_LEVELS - 1) { + TR39_Address(pa) => TR_Address(EXTZ(pa)), + TR39_Failure(f) => TR_Failure(translationException(ac, f)) + }, + _ => internal_error("unsupported address translation scheme") + } +} |