RTS/Main: tweaking cycle counter handling

3 files changed, 22 insertions, 12 deletions

diff --git a/aarch64/elfmain.sail b/aarch64/elfmain.sail
index aaa76d21..cb3edacc 100644
--- a/aarch64/elfmain.sail
+++ b/aarch64/elfmain.sail
@@ -13,7 +13,7 @@ let CNT_IRQ  = [0x0000_000d,       0x0000_000a,        0x0000_03ff,        0x000
 // SGI Interrupts are 0-15, PPI interrupts are 16-31, so SPI interrupts have an offset of 32.
 let SPI_OFFSET = 32
 
-register cycle_counter : int
+val get_cycle_count = { c: "get_cycle_count" } : unit -> int effect {escape, undef, wreg, rreg, rmem, wmem}
 
 // Advance CPU by one cycle
 val Step_CPU : unit -> unit effect {escape, undef, wreg, rreg, rmem, wmem}
@@ -43,7 +43,7 @@ function Step_CPU() = {
       fetch_ok = true;
   } catch {
       Error_ExceptionTaken() => {
-        print(concat_str("Exception taken during IFetch from PC=", concat_str(HexStr(UInt(aget_PC())), "\n")));
+        print(concat_str("Exception taken during IFetch from PC=", concat_str(HexStr(UInt(aget_PC())), concat_str(" in cycle=", concat_str(DecStr(get_cycle_count()), "\n")))));
       },
       _ => {
         print("Exiting due to unhandled exception during fetch\n");
@@ -62,12 +62,12 @@ function Step_CPU() = {
           Error_See(_)              => try { AArch64_UndefinedFault() } catch { _ => print("Exception during SEE recovery\n") },
           Error_ReservedEncoding(_) => try { AArch64_UndefinedFault() } catch { _ => print("Exception during ReservedEncoding recovery\n") },
           Error_ExceptionTaken() => {
-            print(concat_str("ExceptionTaken during Decode/Execute from PC=", concat_str(HexStr(UInt(aget_PC())), concat_str(" opcode=", concat_str(HexStr(UInt(__currentInstr)), "\n")))));
+            print(concat_str("ExceptionTaken during Decode/Execute from PC=", concat_str(HexStr(UInt(aget_PC())), concat_str(" opcode=", concat_str(HexStr(UInt(__currentInstr)), concat_str(" in cycle ", concat_str(DecStr(get_cycle_count()), "\n")))))));
             // print("  This might just be a HINT like 0xd50320df\n");
             ()
           },
           Error_Implementation_Defined(s) => {
-            print(concat_str("Ignoring IMPLEMENTATION_DEFINED", concat_str(s, "\n")));
+            print(concat_str("Ignoring IMPLEMENTATION_DEFINED ", concat_str(s, "\n")));
           }
       }
   };
@@ -158,7 +158,7 @@ function fetch_and_execute () = {
       };
       if prevI != PSTATE.I then {
 	prerr_bits("[Sail] PSTATE.I changed to: ", PSTATE.I);
-        print(concat_str("   at PC=", concat_str(HexStr(UInt(aget_PC())), concat_str(" in cycle=", concat_str(DecStr(cycle_counter), "\n")))));
+        print(concat_str("   at PC=", concat_str(HexStr(UInt(aget_PC())), concat_str(" in cycle=", concat_str(DecStr(get_cycle_count()), "\n")))));
       };
       if prevCNTKCTL_EL1 != CNTKCTL_EL1 then {
         prerr_bits("[Clock] CNTKCTL_EL1 changed to ", CNTKCTL_EL1);
@@ -179,7 +179,6 @@ function fetch_and_execute () = {
       }
     };
     __EndCycle(); // advance state of non-sleeping parts of the system
-    cycle_counter = cycle_counter + 1;
 }
 
 let COLD_RESET : bool = true
@@ -191,15 +190,16 @@ val init : unit -> unit effect {escape, undef, rreg, wreg}
 function init() = {
   __currentInstrLength = 4;
   TakeReset(COLD_RESET);
-  _PC = CFG_RVBAR;
 }
 
 val main : unit -> unit effect {escape, undef, wreg, rreg, rmem, wmem}
 
+val check_cycle_count = { c: "cycle_count" } : unit -> unit
+
 function main() = {
   init();
-  cycle_counter = 0;
   while true do {
-    fetch_and_execute()
+    fetch_and_execute();
+    check_cycle_count();
   }
 }
diff --git a/lib/rts.c b/lib/rts.c
index 51c99af0..d42eebe3 100644
--- a/lib/rts.c
+++ b/lib/rts.c
@@ -7,6 +7,8 @@
 #include"elf.h"
 
 static uint64_t g_elf_entry;
+static uint64_t g_cycle_count = 0;
+static uint64_t g_cycle_limit;
 
 void sail_match_failure(sail_string msg)
 {
@@ -23,6 +25,7 @@ unit sail_assert(bool b, sail_string msg)
 
 unit sail_exit(unit u)
 {
+  fprintf(stderr, "[Sail] Exiting after %lld cycles\n", g_cycle_count);
   exit(EXIT_SUCCESS);
   return UNIT;
 }
@@ -344,9 +347,6 @@ void elf_tohost(mpz_t *rop, const unit u)
 
 /* ***** Cycle limit ***** */
 
-static uint64_t g_cycle_count = 0;
-static uint64_t g_cycle_limit;
-
 /* NB Also increments cycle_count */
 bool cycle_limit_reached(const unit u)
 {
@@ -362,6 +362,11 @@ unit cycle_count(const unit u)
   return UNIT;
 }
 
+void get_cycle_count(sail_int *rop, const unit u)
+{
+    mpz_init_set_ui(*rop, g_cycle_count);
+}
+
 /* ***** Argument Parsing ***** */
 
 static struct option options[] = {
diff --git a/lib/rts.h b/lib/rts.h
index 032d48b8..b4f0d695 100644
--- a/lib/rts.h
+++ b/lib/rts.h
@@ -109,10 +109,15 @@ void trace_end(void);
  * Functions for counting and limiting cycles
  */
 
+// increment cycle count and test if over limit
 bool cycle_limit_reached(const unit);
 
+// increment cycle count and abort if over
 unit cycle_count(const unit);
 
+// read cycle count
+void get_cycle_count(sail_int *rop, const unit);
+
 /*
  * Functions to get info from ELF files.
  */