Fixes for Sv39 TLB.

- fix and simplify model initialization, to enable generic TLB initialization
- re-enable sfence.vma

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 ()
           )