Collect all architectural jump targets (the first 16) in a bag to enable verifying properties

src_Core/CPU/Core.bsv

@@ -101,6 +101,8 @@ import CommitStage::*;
 import Bypass::*;
 import CHERICap::*;
 import CHERICC_Fat::*;
+import Bag::*;
+import VnD :: *;
 
 `ifdef RVFI_DII
 import Toooba_RVFI_DII_Bridge::*;
@@ -303,6 +305,10 @@ module mkCore#(CoreId coreId)(Core);
     EpochManager epochManager <- mkEpochManager;
     SpecTagManager specTagManager <- mkSpecTagManager;
     ReorderBufferSynth rob <- mkReorderBufferSynth;
+    Vector#(SupSize, Bag#(16, CapMem, CapMem)) bags;
+    for(Integer i = 0; i < valueof(SupSize); i=i+1) begin
+        bags[i] <- mkSmallBag;
+    end
 
     // We have two scoreboards: one conservative and other aggressive
     // - Aggressive sb is checked at rename stage, so inst after rename may be issued early
@@ -423,6 +429,13 @@ module mkCore#(CoreId coreId)(Core);
                 endmethod
                 method correctSpec = globalSpecUpdate.correctSpec[finishAluCorrectSpecPort(i)].put;
                 method doStats = doStatsReg._read;
+                method Bool checkTarget(CapMem ppc);
+                    Bool ret = False;
+                    for(Integer j = 0; j < valueof(SupSize); j=j+1) begin
+                        ret = ret || bags[j].isMember(ppc).v;
+                    end
+                    return ret;
+                endmethod
             endinterface);
             aluExe[i] <- mkAluExePipeline(aluExeInput);
             // truly call fetch method to train branch predictor
@@ -675,6 +688,14 @@ module mkCore#(CoreId coreId)(Core);
 `endif
         endmethod
 
+        method Action updateTargets(Vector#(SupSize, Maybe#(CapMem)) targets);
+            for(Integer i = 0; i < valueof(SupSize); i=i+1) begin
+                if(targets[i] matches tagged Valid .tar) begin
+                    bags[i].insert(tar, tar);
+                end
+            end
+        endmethod
+
 `ifdef INCLUDE_TANDEM_VERIF
        interface v_to_TV = map (toPut, v_f_to_TV);
 `endif

src_Core/RISCY_OOO/procs/RV64G_OOO/AluExePipeline.bsv

@@ -194,6 +194,9 @@ interface AluExeInput;
 
     // performance
     method Bool doStats;
+
+    // check previous branch targets
+    method Bool checkTarget(CapMem ppc);
 endinterface
 
 interface AluExePipeline;
@@ -282,6 +285,8 @@ module mkAluExePipeline#(AluExeInput inIfc)(AluExePipeline);
         let ppc = inIfc.rob_getPredPC(x.tag);
         let orig_inst = inIfc.rob_getOrig_Inst (x.tag);
 
+        let res = inIfc.checkTarget(ppc);
+
         // go to next stage
         regToExeQ.enq(ToSpecFifo {
             data: AluRegReadToExe {

src_Core/RISCY_OOO/procs/RV64G_OOO/CommitStage.bsv

@@ -132,6 +132,9 @@ interface CommitInput;
     // deadlock check
     method Bool checkDeadlock;
 
+    // update branch targets
+    method Action updateTargets(Vector#(SupSize, Maybe#(CapMem)) targets);
+
 `ifdef INCLUDE_TANDEM_VERIF
     interface Vector #(SupSize, Put #(Trace_Data2)) v_to_TV;
 `endif
@@ -1087,8 +1090,12 @@ module mkCommitStage#(CommitInput inIfc)(CommitStage);
        Bit #(5) po_fflags  = ?;
        Data     po_mstatus = ?;
 `endif
+
+        // update targets vector
+        Vector#(SupSize, Maybe#(CapMem)) targets;
         // compute what actions to take
         for(Integer i = 0; i < valueof(SupSize); i = i+1) begin
+            Maybe#(CapMem) tar = tagged Invalid;
             if(!stop && rob.deqPort[i].canDeq) begin
                 let x = rob.deqPort[i].deq_data;
                 let inst_tag = rob.deqPort[i].getDeqInstTag;
@@ -1132,6 +1139,11 @@ module mkCommitStage#(CommitInput inIfc)(CommitStage);
                     // inst can be committed, deq it
                     rob.deqPort[i].deq;
 
+                    // update target
+                    if(x.iType == CJALR || x.iType == Jr) begin
+                        tar = tagged Valid x.ppc_vaddr_csrData.PPC;
+                    end
+
                     // every inst here should have been renamed, commit renaming
                     regRenamingTable.commit[i].commit;
                     doAssert(x.claimed_phy_reg, "should have renamed");
@@ -1207,6 +1219,7 @@ module mkCommitStage#(CommitInput inIfc)(CommitStage);
                     if (opcode == opcMiscMem && funct3 == fnFENCE) fenceCnt = fenceCnt + 1;
                 end
             end
+            targets[i] = tar;
         end
         rg_serial_num <= rg_serial_num + instret;
 
@@ -1270,6 +1283,9 @@ module mkCommitStage#(CommitInput inIfc)(CommitStage);
         events.evt_FENCE = fenceCnt;
         events_reg <= events;
 `endif
+
+        inIfc.updateTargets(targets);
+
 `ifdef RVFI
         rvfiQ.enq(rvfis);
         traceCnt <= traceCnt + zeroExtend(whichTrace);