Cheri-research/Toooba
1
0
Fork 0
Code Issues 1 Pull Requests Actions Packages Projects Releases Wiki Activity

performed corrections for CONTRACTS_VERIFY

Browse Source
This commit is contained in:
Franz Fuchs
2021-09-07 08:15:03 +01:00
parent e58000c82d
commit b25d70a8cc
4 changed files with 11 additions and 20 deletions
Download Patch File Download Diff File Expand all files Collapse all files

19
src_Core/CPU/Core.bsv
View File

@@ -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;

1
src_Core/RISCY_OOO/procs/RV64G_OOO/AluExePipeline.bsv
View File

@@ -61,6 +61,7 @@ import CHERICC_Fat::*;
import ISA_Decls_CHERI::*;
`ifdef PERFORMANCE_MONITORING
import BlueUtils::*;
import StatCounters::*;
`endif

3
src_Core/RISCY_OOO/procs/RV64G_OOO/RenameStage.bsv
View File

@@ -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

8
src_Core/RISCY_OOO/procs/lib/ProcTypes.bsv
View File

@@ -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)));