Uncomment the clint implementation in riscv_platform.

1 files changed, 5 insertions, 13 deletions

diff --git a/riscv/riscv_platform.sail b/riscv/riscv_platform.sail
index 1c5da1df..b88264dc 100644
--- a/riscv/riscv_platform.sail
+++ b/riscv/riscv_platform.sail
@@ -26,7 +26,7 @@ function phys_mem_segments() =
 
 val plat_insns_per_tick = {ocaml: "Platform.insns_per_tick"} : unit -> int
 
-/* CLINT clock device interface, based on Spike. */
+/* CLINT (Core Local Interruptor), based on Spike. */
 
 // assumes a single hart, since this typically is a vector of per-hart registers.
 register mtimecmp : xlenbits  // memory-mapped internal clint register.
@@ -37,31 +37,25 @@ let MSIP_BASE     : xlenbits = 0x0000000000000000
 let MTIMECMP_BASE : xlenbits = 0x0000000000004000
 let MTIME_BASE    : xlenbits = 0x000000000000bff8
 
-/* 0000 msip hart 0
+/* 0000 msip hart 0         -- memory-mapped software interrupt
  * 0004 msip hart 1
- * 4000 mtimecmp hart 0 lo
+ * 4000 mtimecmp hart 0 lo  -- memory-mapped timer thresholds
  * 4004 mtimecmp hart 0 hi
  * 4008 mtimecmp hart 1 lo
  * 400c mtimecmp hart 1 hi
- * bff8 mtime lo
+ * bff8 mtime lo            -- memory-mapped clocktimer value
  * bffc mtime hi
  */
 
 val clint_load : forall 'n, 'n > 0. (xlenbits, int('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rreg}
 function clint_load(addr, width) = {
-  /* FIXME: For now, only allow exact aligned access.
-     I couldn't make the more general access pass the type-checker.
-   */
+  /* FIXME: For now, only allow exact aligned access. */
   if addr == MSIP_BASE & ('n == 8 | 'n == 4)
   then MemValue(zero_extend(mip.MSI(), sizeof(8 * 'n)))
-  /* FIXME:
   else if addr == MTIMECMP_BASE & ('n == 8)
   then MemValue(mtimecmp)
-  */
-  /* FIXME:
   else if addr == MTIME_BASE & ('n == 8)
   then MemValue(mtime)
-  */
   else MemException(E_Load_Access_Fault)
 }
 
@@ -71,9 +65,7 @@ function clint_store(addr, width, data) = {
     mip->MSI() = data[0] == 0b1;
     MemValue(())
   } else if addr == MTIMECMP_BASE & 'n == 8 then {
-    /* FIXME:
     mtimecmp = data;
-    */
     MemValue(())
   } else MemException(E_SAMO_Access_Fault)
 }