Gate timers and MSI on an enabled CLINT.

Author: pmundkur

model/core/interrupt_regs.sail

@@ -208,17 +208,23 @@ function read_mip(read_type : XipReadType) -> Minterrupts =
 function update_mip() -> unit = {
   let old_mip = mip.bits;
 
-  // This updates `mip` for any timer interrupts that may now have fired,
-  // and for any machine-level software interrupts arising from the
-  // CLINT.
+  // This updates `mip` for any timer interrupts that may now have
+  // fired, and for any machine-level software interrupts arising from
+  // the CLINT.  Currently, the only timer support is from the CLINT;
+  // so without a CLINT, no timer interrupts can fire.  This may need
+  // to change when we support other or multiple interrupt
+  // controllers.
+
+  let platform_has_timer = plat_have_clint;
+
   let cur_mtime = get_mtime();
   let hart_mtimecmp = get_hart_mtimecmp();
 
   mip[MSI] = get_machine_software_interrupt_pending();
-  mip[MTI] = bool_to_bit(hart_mtimecmp <=_u cur_mtime);
+  mip[MTI] = bool_to_bit(platform_has_timer & (hart_mtimecmp <=_u cur_mtime));
 
   if currentlyEnabled(Ext_Sstc) & menvcfg[STCE] == 0b1 then {
-    mip[STI] = bool_to_bit(stimecmp <=_u cur_mtime);
+    mip[STI] = bool_to_bit(platform_has_timer & (stimecmp <=_u cur_mtime));
   };
 
   if currentlyEnabled(Ext_H) then {
@@ -240,7 +246,7 @@ function update_mip() -> unit = {
     var VSTI : bits(1) = hvip[VSTI];
 
     if currentlyEnabled(Ext_Sstc) & read_henvcfg()[STCE] == 0b1 then {
-      VSTI = VSTI | bool_to_bit(vstimecmp <=_u (cur_mtime + htimedelta));
+      VSTI = VSTI | bool_to_bit(platform_has_timer & (vstimecmp <=_u (cur_mtime + htimedelta)));
     };
     mip[VSTI] = VSTI;
   };

model/sys/platform.sail

@@ -73,12 +73,14 @@ private register mtimecmp : bits(64)
 // number of cycles from the system clock.
 private register mtime : bits(64)
 
-function get_mtime() -> bits(64) = mtime
+function get_mtime() -> bits(64) =
+  if plat_have_clint then mtime else zeros()
 
-function get_hart_mtimecmp() -> bits(64) = mtimecmp
+function get_hart_mtimecmp() -> bits(64) =
+  if plat_have_clint then mtimecmp else zeros()
 
 function get_machine_software_interrupt_pending() -> bits(1) =
-  msip[0]
+  if plat_have_clint then msip[0] else 0b0
 
 // CLINT memory-mapped IO