From b25d70a8cc0e652d631114a7c95804a54b18156f Mon Sep 17 00:00:00 2001
From: Franz Fuchs <franz.fuchs@cl.cam.ac.uk>
Date: Tue, 7 Sep 2021 08:15:03 +0100
Subject: [PATCH] performed corrections for CONTRACTS_VERIFY

---
 src_Core/CPU/Core.bsv                         | 19 ++++++++-----------
 .../procs/RV64G_OOO/AluExePipeline.bsv        |  1 +
 .../RISCY_OOO/procs/RV64G_OOO/RenameStage.bsv |  3 ++-
 src_Core/RISCY_OOO/procs/lib/ProcTypes.bsv    |  8 --------
 4 files changed, 11 insertions(+), 20 deletions(-)

diff --git a/src_Core/CPU/Core.bsv b/src_Core/CPU/Core.bsv
index 6b7c624..2de4196 100644
--- a/src_Core/CPU/Core.bsv
+++ b/src_Core/CPU/Core.bsv
@@ -1162,15 +1162,13 @@ module mkCore#(CoreId coreId)(Core);
      EventsL1D dmem_evts = unpack(pack(dMem.events) | pack(dTlb.events));
      EventsCacheCore tgc_evts = events_tgc_reg;
      EventsLL llmem_evts = unpack(pack(events_llc_reg) | pack(l2Tlb.events));
+     Maybe#(EventsTransExe) mab_trans_exe = tagged Invalid;
 
-     let ev_struct = HPMEvents{mab_EventsCore: tagged Valid core_evts, mab_EventsL1I: tagged Valid imem_evts,
-                               mab_EventsL1D: tagged Valid dmem_evts, mab_EventsLL: tagged Valid llmem_evts,
-                               mab_EventsCacheCore: tagged Valid tgc_evts};
 
 `ifdef CONTRACTS_VERIFY
      EventsTransExe texe_evts = renameStage.events;
-     SupCnt wildJumps = 0;
-     SupCnt wildExceptions = texe_evts.evt_WILD_EXCEPTION;
+     Bit#(Report_Width) wildJumps = 0;
+     Bit#(Report_Width) wildExceptions = texe_evts.evt_WILD_EXCEPTION;
      for(Integer i = 0; i < valueof(AluExeNum); i = i+1) begin
           let alu_events = coreFix.aluExeIfc[i].events;
           wildJumps = wildJumps + alu_events.evt_WILD_JUMP;
@@ -1179,15 +1177,14 @@ module mkCore#(CoreId coreId)(Core);
 
      texe_evts.evt_WILD_JUMP = wildJumps;
      texe_evts.evt_WILD_EXCEPTION = wildExceptions;
-     ev_struct = HPMEvents{mab_EventsCore: tagged Valid core_evts, mab_EventsL1I: tagged Valid imem_evts,
-                               mab_EventsL1D: tagged Valid dmem_evts, mab_EventsLL: tagged Valid llmem_evts,
-                               mab_EventsCacheCore: tagged Valid tgc_evts, mab_EventsTransExe: tagged Valid texe_evts};
+     mab_trans_exe = tagged Valid texe_evts;
 `endif
 
+     let ev_struct = HPMEvents{mab_EventsCore: tagged Valid core_evts, mab_EventsL1I: tagged Valid imem_evts,
+                               mab_EventsL1D: tagged Valid dmem_evts, mab_EventsLL: tagged Valid llmem_evts,
+                               mab_EventsCacheCore: tagged Valid tgc_evts, mab_EventsTransExe: mab_trans_exe};
+
      let events = generateHPMVector(ev_struct);
-`ifdef CONTRACTS_VERIFY
-     events = append (events, trans_exe_evts_vec);
-`endif
 
      (* fire_when_enabled, no_implicit_conditions *)
      rule rl_send_perf_evts;
diff --git a/src_Core/RISCY_OOO/procs/RV64G_OOO/AluExePipeline.bsv b/src_Core/RISCY_OOO/procs/RV64G_OOO/AluExePipeline.bsv
index b3b19df..25eedd8 100755
--- a/src_Core/RISCY_OOO/procs/RV64G_OOO/AluExePipeline.bsv
+++ b/src_Core/RISCY_OOO/procs/RV64G_OOO/AluExePipeline.bsv
@@ -61,6 +61,7 @@ import CHERICC_Fat::*;
 import ISA_Decls_CHERI::*;
 `ifdef PERFORMANCE_MONITORING
 import BlueUtils::*;
+import StatCounters::*;
 `endif
 
 
diff --git a/src_Core/RISCY_OOO/procs/RV64G_OOO/RenameStage.bsv b/src_Core/RISCY_OOO/procs/RV64G_OOO/RenameStage.bsv
index 126b0bb..800e221 100644
--- a/src_Core/RISCY_OOO/procs/RV64G_OOO/RenameStage.bsv
+++ b/src_Core/RISCY_OOO/procs/RV64G_OOO/RenameStage.bsv
@@ -67,6 +67,7 @@ import SplitLSQ::*;
 import CHERICap::*;
 import CHERICC_Fat::*;
 import ISA_Decls_CHERI::*;
+import StatCounters::*;
 
 import Cur_Cycle :: *;
 
@@ -1186,7 +1187,7 @@ module mkRenameStage#(RenameInput inIfc)(RenameStage);
 `endif
 `ifdef PERFORMANCE_MONITORING
         EventsTransExe events = unpack(0);
-        events.evt_RENAMED_INST = renameCnt;
+        events.evt_RENAMED_INST = zeroExtend(renameCnt);
         events_reg <= events;
 `endif
 
diff --git a/src_Core/RISCY_OOO/procs/lib/ProcTypes.bsv b/src_Core/RISCY_OOO/procs/lib/ProcTypes.bsv
index c0c1e33..84909a2 100755
--- a/src_Core/RISCY_OOO/procs/lib/ProcTypes.bsv
+++ b/src_Core/RISCY_OOO/procs/lib/ProcTypes.bsv
@@ -1054,14 +1054,6 @@ typedef  64 Counter_Width;
 typedef  29 No_Of_Ctrs;
 
 
-typedef struct {
-   SupCnt evt_RENAMED_INST;
-   SupCnt evt_WILD_JUMP;
-   SupCnt evt_WILD_EXCEPTION;
-} EventsTransExe deriving (Bits, FShow);
-typedef TDiv#(SizeOf#(EventsTransExe),SizeOf#(SupCnt)) EventsTransExeElements;
-`endif
-
 function Bit#(outWidth) hash(Bit#(inWidth) in)
     provisos(Add#(a__, inWidth, TMul#(TDiv#(inWidth, outWidth), outWidth)),
              Add#(1, b__, TDiv#(inWidth, outWidth)));