Add the htif exit command, a top-level function to initialize the riscv platform, and document the artificial wreg effect due to using registers for device state.

2 files changed, 18 insertions, 9 deletions

diff --git a/riscv/platform_main.ml b/riscv/platform_main.ml
index b4a468f9..cb379cdd 100644
--- a/riscv/platform_main.ml
+++ b/riscv/platform_main.ml
@@ -75,7 +75,8 @@ let () =
 
   sail_call
     (fun r ->
-      try ( zinit_sys ();
+      try ( zinit_platform (); (* devices *)
+            zinit_sys ();      (* processor *)
             zPC := pc;
             zloop (Elf_loader.elf_tohost ())
           )
diff --git a/riscv/riscv_platform.sail b/riscv/riscv_platform.sail
index b88264dc..8f4e923a 100644
--- a/riscv/riscv_platform.sail
+++ b/riscv/riscv_platform.sail
@@ -78,24 +78,27 @@ bitfield htif_cmd : bits(64) = {
   payload : 47 .. 0
 }
 
+register htif_done : bool
+register htif_exit_code : xlenbits
+
 // no support yet for terminal input
-val htif_load : forall 'n, 'n > 0. (xlenbits, int('n)) -> MemoryOpResult(bits(8 * 'n))
+val htif_load : forall 'n, 0 < 'n <= 64. (xlenbits, int('n)) -> MemoryOpResult(bits(8 * 'n))
 function htif_load(addr, width) = MemValue(EXTZ(0b0))
 
-val htif_store: forall 'n, 'n > 0. (xlenbits, int('n), bits(8 * 'n)) -> MemoryOpResult(unit)
+/* FIXME: The wreg effect is an artifact of using 'register' to implement device state. */
+val htif_store: forall 'n, 0 < 'n <= 8. (xlenbits, int('n), bits(8 * 'n)) -> MemoryOpResult(unit) effect {wreg}
 function htif_store(addr, width, data) = {
   // since htif is only available at a single address, we'll assume here that physical memory
   // model has correctly dispatched the address.
-  let cbits : xlenbits = /* if 'n == 4 then EXTZ(data) else data */ EXTZ(0b0);
+  let cbits : xlenbits = EXTZ(data);
   let cmd = Mk_htif_cmd(cbits);
   match cmd.device() {
     0x00 => { /* syscall-proxy */
       if cmd.payload()[0] == 0b1
-      then /* TODO: exit command
-            * for e.g. set a flag that's checked by the top-level loop.
-            * but that might appear to be a register write effect triggered by a memory write.
-            */
-           ()
+      then {
+           htif_done = true;
+           htif_exit_code = (zero_extend(cmd.payload(), xlen) >> 0b01) : xlenbits
+      }
       else ()
     },
     0x01 => { /* terminal */
@@ -109,3 +112,8 @@ function htif_store(addr, width, data) = {
   };
   MemValue(())
 }
+
+function init_platform() -> unit = {
+  htif_done = false;
+  htif_exit_code = EXTZ(0b0);
+}