From e6e7443dd59c8cb7a325c6239fd1e4a4141f77eb Mon Sep 17 00:00:00 2001 From: Prashanth Mundkur Date: Mon, 11 Mar 2019 12:31:20 -0700 Subject: Fixes for Sv39 TLB. - fix and simplify model initialization, to enable generic TLB initialization - re-enable sfence.vma --- c_emulator/riscv_sail.h | 3 +-- c_emulator/riscv_sim.c | 3 +-- model/main.sail | 3 +-- model/riscv_insts_base.sail | 15 ++++++++++----- model/riscv_step.sail | 7 +++++++ model/riscv_vmem_rv32.sail | 9 +++++++++ model/riscv_vmem_rv64.sail | 9 +++++++++ model/riscv_vmem_sv39.sail | 5 +++++ ocaml_emulator/riscv_ocaml_sim.ml | 3 +-- 9 files changed, 44 insertions(+), 13 deletions(-) diff --git a/c_emulator/riscv_sail.h b/c_emulator/riscv_sail.h index 721f180..a02482e 100644 --- a/c_emulator/riscv_sail.h +++ b/c_emulator/riscv_sail.h @@ -12,8 +12,7 @@ struct zMisa zmisa; void model_init(void); void model_fini(void); -unit zinit_platform(unit); -unit zinit_sys(unit); +unit zinit_model(unit); bool zstep(sail_int); unit ztick_clock(unit); unit ztick_platform(unit); diff --git a/c_emulator/riscv_sim.c b/c_emulator/riscv_sim.c index 2291ec3..7be7fce 100644 --- a/c_emulator/riscv_sim.c +++ b/c_emulator/riscv_sim.c @@ -413,8 +413,7 @@ void preinit_sail() void init_sail(uint64_t elf_entry) { - zinit_platform(UNIT); - zinit_sys(UNIT); + zinit_model(UNIT); #ifdef RVFI_DII if (rvfi_dii) { rv_ram_base = UINT64_C(0x80000000); diff --git a/model/main.sail b/model/main.sail index e07a31a..a0965f6 100644 --- a/model/main.sail +++ b/model/main.sail @@ -16,8 +16,7 @@ function main () = { PC = sail_zero_extend(0x1000, sizeof(xlen)); print_bits("PC = ", PC); try { - init_platform(); - init_sys(); + init_model(); loop() } catch { Error_not_implemented(s) => print_string("Error: Not implemented: ", s), diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail index d79639a..e6e272c 100644 --- a/model/riscv_insts_base.sail +++ b/model/riscv_insts_base.sail @@ -710,11 +710,16 @@ function clause execute SFENCE_VMA(rs1, rs2) = { else match (architecture(get_mstatus_SXL(mstatus)), mstatus.TVM()) { (Some(_), true) => { handle_illegal(); false }, (Some(_), 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); - */ + if sizeof(xlen) == 64 + then { + 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]); + flush_TLB(asid, addr) + } else { + let addr : option(vaddr32) = if rs1 == 0 then None() else Some(X(rs1)[31 .. 0]); + let asid : option(asid32) = if rs2 == 0 then None() else Some(X(rs2)[8 .. 0]); + flush_TLB(asid, addr) + }; true }, (_, _) => internal_error("unimplemented sfence architecture") diff --git a/model/riscv_step.sail b/model/riscv_step.sail index 78369a8..ca2ca76 100644 --- a/model/riscv_step.sail +++ b/model/riscv_step.sail @@ -128,3 +128,10 @@ function loop () = { } } } + +/* initialize model state */ +function init_model () -> unit = { + init_platform (); /* devices */ + init_sys (); /* processor */ + init_vmem () /* virtual memory */ +} diff --git a/model/riscv_vmem_rv32.sail b/model/riscv_vmem_rv32.sail index ae2b011..6f06f93 100644 --- a/model/riscv_vmem_rv32.sail +++ b/model/riscv_vmem_rv32.sail @@ -50,3 +50,12 @@ function translateAddr(vAddr, ac, rt) = { _ => internal_error("unsupported address translation scheme") } } + +val flush_TLB : (option(asid32), option(vaddr32)) -> unit effect {rreg, wreg} +function flush_TLB(asid, addr) -> unit = { + () +} + +function init_vmem () -> unit = { + () +} diff --git a/model/riscv_vmem_rv64.sail b/model/riscv_vmem_rv64.sail index 9ed3c54..2a415c7 100644 --- a/model/riscv_vmem_rv64.sail +++ b/model/riscv_vmem_rv64.sail @@ -61,3 +61,12 @@ function translateAddr(vAddr, ac, rt) = { _ => internal_error("unsupported address translation scheme") } } + +val flush_TLB : (option(asid64), option(vaddr39)) -> unit effect {rreg, wreg} +function flush_TLB(asid, addr) -> unit = { + flush_TLB39(asid, addr) +} + +function init_vmem() -> unit = { + init_vmem_sv39() +} diff --git a/model/riscv_vmem_sv39.sail b/model/riscv_vmem_sv39.sail index a075254..b349783 100644 --- a/model/riscv_vmem_sv39.sail +++ b/model/riscv_vmem_sv39.sail @@ -110,6 +110,7 @@ val translate39 : (asid64, paddr64, vaddr39, AccessType, Privilege, bool, bool, function translate39(asid, ptb, vAddr, ac, priv, mxr, do_sum, level) = { match lookup_TLB39(asid, vAddr) { Some(idx, ent) => { +/* print("translate39: TLB39 hit for " ^ BitStr(vAddr)); */ let pte = Mk_SV39_PTE(ent.pte); let pteBits = Mk_PTE_Bits(pte.BITS()); if ~ (checkPTEPermission(ac, priv, mxr, do_sum, pteBits)) @@ -172,3 +173,7 @@ function translate39(asid, ptb, vAddr, ac, priv, mxr, do_sum, level) = { } } } + +function init_vmem_sv39() -> unit = { + tlb39 = None() +} diff --git a/ocaml_emulator/riscv_ocaml_sim.ml b/ocaml_emulator/riscv_ocaml_sim.ml index f7b9c0b..319df7a 100644 --- a/ocaml_emulator/riscv_ocaml_sim.ml +++ b/ocaml_emulator/riscv_ocaml_sim.ml @@ -137,8 +137,7 @@ let show_times init_s init_e run_e insts = let run pc = sail_call (fun r -> - try ( zinit_platform (); (* devices *) - zinit_sys (); (* processor *) + try ( zinit_model (); zPC := pc; zloop () ) -- cgit v1.1