Make riscv pte dirty-bit update handling configurable via a platform cli option.

Fix a redundant clock tick.

6 files changed, 21 insertions, 8 deletions

diff --git a/riscv/platform.ml b/riscv/platform.ml
index 0aac4884..1b3ecf5d 100644
--- a/riscv/platform.ml
+++ b/riscv/platform.ml
@@ -52,6 +52,9 @@ open Sail_lib;;
 module P = Platform_impl;;
 module Elf = Elf_loader;;
 
+(* Platform configuration *)
+let config_enable_dirty_update = ref false
+
 (* Mapping to Sail externs *)
 
 let bits_of_int i =
@@ -75,6 +78,8 @@ let make_rom start_pc =
      *)
     rom )
 
+let enable_dirty_update () = !config_enable_dirty_update
+
 let rom_base () = bits_of_int64 P.rom_base
 let rom_size () = bits_of_int   !rom_size_ref
 
diff --git a/riscv/platform_main.ml b/riscv/platform_main.ml
index e0032bf8..a087e90c 100644
--- a/riscv/platform_main.ml
+++ b/riscv/platform_main.ml
@@ -51,7 +51,8 @@
 open Elf_loader
 open Sail_lib
 open Riscv
-module P = Platform_impl
+module PI = Platform_impl
+module P = Platform
 
 (* OCaml driver for generated RISC-V model. *)
 
@@ -66,6 +67,9 @@ let options = Arg.align ([("-dump-dts",
                           ("-dump-dtb",
                            Arg.Set opt_dump_dtb,
                            " dump the *binary* platform device-tree blob to stdout");
+                          ("-enable-dirty-update",
+                           Arg.Set P.config_enable_dirty_update,
+                           " enable dirty-bit update during page-table walks")
                          ])
 
 let usage_msg = "RISC-V platform options:"
@@ -73,8 +77,8 @@ let usage_msg = "RISC-V platform options:"
 let elf_arg =
   Arg.parse options (fun s -> opt_file_arguments := !opt_file_arguments @ [s])
             usage_msg;
-  if !opt_dump_dts then (P.dump_dts (); exit 0);
-  if !opt_dump_dtb then (P.dump_dtb (); exit 0);
+  if !opt_dump_dts then (PI.dump_dts (); exit 0);
+  if !opt_dump_dtb then (PI.dump_dtb (); exit 0);
   ( match !opt_file_arguments with
       | f :: _ -> prerr_endline ("Sail/RISC-V: running ELF file " ^ f); f
       | _ -> (prerr_endline "Please provide an ELF file."; exit 0)
diff --git a/riscv/riscv_extras.lem b/riscv/riscv_extras.lem
index 60f5dde9..60d9852a 100644
--- a/riscv/riscv_extras.lem
+++ b/riscv/riscv_extras.lem
@@ -68,6 +68,10 @@ val plat_clint_size : forall 'a. Size 'a => unit -> bitvector 'a
 let plat_clint_size () = wordFromInteger 0
 declare ocaml target_rep function plat_clint_size = `Platform.clint_size`
 
+val plat_enable_dirty_update : unit -> bool
+let plat_enable_dirty_update () = false
+declare ocaml target_rep function plat_enable_dirty_update = `Platform.enable_dirty_update`
+
 val plat_insns_per_tick : unit -> integer
 let plat_insns_per_tick () = 1
 declare ocaml target_rep function plat_insns_per_tick = `Platform.insns_per_tick`
diff --git a/riscv/riscv_platform.sail b/riscv/riscv_platform.sail
index c6786ff7..27c774cc 100644
--- a/riscv/riscv_platform.sail
+++ b/riscv/riscv_platform.sail
@@ -10,6 +10,9 @@
 val plat_ram_base = {ocaml: "Platform.dram_base", lem: "plat_ram_base"} : unit -> xlenbits
 val plat_ram_size = {ocaml: "Platform.dram_size", lem: "plat_ram_size"} : unit -> xlenbits
 
+/* whether the MMU should update dirty bits in PTEs */
+val plat_enable_dirty_update = {ocaml: "Platform.enable_dirty_update", lem: "plat_enable_dirty_update"} : unit -> bool
+
 /* ROM holding reset vector and device-tree DTB */
 val plat_rom_base = {ocaml: "Platform.rom_base", lem: "plat_rom_base"} : unit -> xlenbits
 val plat_rom_size = {ocaml: "Platform.rom_size", lem: "plat_rom_size"} : unit -> xlenbits
diff --git a/riscv/riscv_step.sail b/riscv/riscv_step.sail
index acbab1f6..fe9d7e84 100644
--- a/riscv/riscv_step.sail
+++ b/riscv/riscv_step.sail
@@ -95,7 +95,6 @@ function loop () = {
   i : int = 0;
   step_no : int = 0;
   while true do {
-    tick_clock();
     minstret_written = false;     /* see note for minstret */
     let retired = step(step_no);
     PC = nextPC;
diff --git a/riscv/riscv_vmem.sail b/riscv/riscv_vmem.sail
index d5efe252..9d0f42d1 100644
--- a/riscv/riscv_vmem.sail
+++ b/riscv/riscv_vmem.sail
@@ -257,8 +257,6 @@ union TR39_Result = {
   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, do_sum, level) = {
   let asid = curAsid64();
@@ -271,7 +269,7 @@ function translate39(vAddr, ac, priv, mxr, do_sum, level) = {
         match update_PTE_Bits(pteBits, ac) {
           None() => TR39_Address(ent.pAddr | EXTZ(vAddr & ent.vAddrMask)),
           Some(pbits) => {
-            if ~ (enable_dirty_update)
+            if ~ (plat_enable_dirty_update ())
             then {
               /* pte needs dirty/accessed update but that is not enabled */
               TR39_Failure(PTW_PTE_Update)
@@ -301,7 +299,7 @@ function translate39(vAddr, ac, priv, mxr, do_sum, level) = {
               TR39_Address(pAddr)
             },
             Some(pbits) =>
-              if ~ (enable_dirty_update)
+              if ~ (plat_enable_dirty_update ())
               then {
                 /* pte needs dirty/accessed update but that is not enabled */
                 TR39_Failure(PTW_PTE_Update)