$$$pvs-strategies (defstep simp () (then (flatten)(assert)(simplify)(flatten)) " Flatten, assert, simplify" " ") (defstep LazyGrind () (then (grind$ :if-match nil)(grind$)) " Grind with the instantiation postponed to the end" " ") (defstep MyGrind () (grind$ :if-match nil) " Grind with no instantiation" " ") (defstep grind-best () (grind$ :if-match best) " Grind with best instantiation" " Grind with best instantiation") (defstep expand-rho (&optional (inv nil)) (then (EXPAND "rho_issue")(EXPAND "rho_execute") (EXPAND "rho_writeb")(EXPAND "rho_retire")(EXPAND "rho_extint") (EXPAND inv) (SKOSIMP*) (REPLACE*) (simp)) "Expands out rho, skosimps, replaces and hides" " " ) (defstep expand-issue (&optional (inv1 nil)(inv2 nil)(inv3 nil)(inv4 nil)(inv5 nil)) (then (EXPAND "rho_issue") (EXPAND "dispatch")(EXPAND "succ") (EXPAND inv1) (EXPAND inv2) (EXPAND inv3) (EXPAND inv4) (EXPAND inv5) (SKOSIMP*) (REPLACE*) (simp) (hide -2 -3 -4 -5 -6 -7)) "Expands out rho, skosimps, replaces and hides" " " ) (defstep exp-inv-issue (&optional (inv1 nil)(inv2 nil)(inv3 nil)(inv4 nil)(inv5 nil)(split t)(expocc t)) (then (EXPAND "rho_issue") (EXPAND "dispatch") (EXPAND "wrapWraps") (EXPAND "headTailEq")(EXPAND "occEqual")(EXPAND "freeHeadROBempty") (EXPAND "occBuffBusyRAT")(EXPAND "occRS")(EXPAND "slotUnique")(EXPAND "RATpointsNewestBuff")(EXPAND "busyRAT") (EXPAND "occTailROBfull")(EXPAND "activeRes")(EXPAND "occRSops")(EXPAND "RS_ROB_opsEqual") (EXPAND "busyROBoccRS")(EXPAND "writeBoperandsNearest") (EXPAND "retiredOperandsMatchRF")(EXPAND "activeResOpsNotBusy") (EXPAND "busyOperandsNearest")(EXPAND "opsMatchROB")(EXPAND "intBrMatch")(expand "robeMatchesBr") (EXPAND "robeMatchesProg")(expand "activeResCorrectVal")(EXPAND "completedROBEcorrectVal") (EXPAND "headROBEcorrectVal")(expand "numOcc") (expand "busyOpBusyROB") (EXPAND inv1) (EXPAND inv2) (EXPAND inv3) (EXPAND inv4) (EXPAND inv5) (EXPAND "totalIssued") (EXPAND "issuedBefore")(expand "numOccBuffers")(expand "bufferIndex") (EXPAND "weakPreceed")(expand "preceed") (if (eq expocc 't)(then (expand "occ_buffer"))(skip)) (EXPAND "succ") (SKOSIMP*) (REPLACE*) (simp) (hide -2 -3 -4 -5 -6 -7) (if (eq split 't)(then (split +)(skosimp*)(simp))(skip))) "Expands out rho, skosimps, replaces and hides" " " ) (defstep exp-inv-exec (&optional (inv1 nil)(inv2 nil)(inv3 nil)(inv4 nil)(inv5 nil)(split t)(hideiex f)) (then (EXPAND "rho_execute") (EXPAND "enabled") (EXPAND "wrapWraps") (EXPAND "headTailEq")(EXPAND "occEqual") (EXPAND "occBuffBusyRAT")(EXPAND "occTailROBfull")(EXPAND "freeHeadROBempty") (EXPAND "RATpointsNewestBuff")(EXPAND "busyRAT")(EXPAND "occRS") (EXPAND "slotUnique")(EXPAND "activeRes")(EXPAND "occRSops") (EXPAND "RS_ROB_opsEqual") (EXPAND "busyROBoccRS") (EXPAND "busyROBoccRS")(EXPAND "writeBoperandsNearest") (EXPAND "retiredOperandsMatchRF")(EXPAND "activeResOpsNotBusy")(EXPAND "opsMatchROB")(EXPAND "intBrMatch")(expand "robeMatchesBr") (EXPAND "robeMatchesProg")(expand "activeResCorrectVal")(EXPAND "completedROBEcorrectVal") (EXPAND "headROBEcorrectVal")(expand "numOcc") (expand "busyOpBusyROB") (EXPAND inv1) (EXPAND inv2) (EXPAND inv3) (EXPAND inv4) (EXPAND inv5) (EXPAND "issuedBefore")(expand "numOccBuffers")(expand "bufferIndex") (EXPAND "weakPreceed")(expand "preceed")(expand "occ_buffer") (SKOSIMP*) (REPLACE*) (simp) (hide -1 -2 -4 -5 -6 -7 -8) (if (eq hideiex 't)(hide -1)(skip)) (if (eq split 't)(then (split +)(skosimp*)(simp))(skip))) "Expands out rho, skosimps, replaces and hides" " " ) (defstep exp-inv-writeb (&optional (inv1 nil)(inv2 nil)(inv3 nil)(split t)(expocc t)(res f)(hideiex f)) (then (EXPAND "rho_writeb") (expand "enabled") (EXPAND "wrapWraps") (EXPAND "headTailEq")(EXPAND "occEqual")(EXPAND "occTailROBfull") (EXPAND "freeHeadROBempty") (EXPAND "occBuffBusyRAT")(EXPAND "busyRAT")(EXPAND "RATpointsNewestBuff") (EXPAND "occRS")(EXPAND "slotUnique") (EXPAND "activeRes") (EXPAND "occRSops")(EXPAND "RS_ROB_opsEqual") (EXPAND "busyROBoccRS") (EXPAND "busyOperandsNearest") (EXPAND "writeBoperandsNearest") (EXPAND "retiredOperandsMatchRF")(EXPAND "activeResOpsNotBusy")(EXPAND "opsMatchROB") (EXPAND "robeMatchesProg")(expand "activeResCorrectVal")(EXPAND "completedROBEcorrectVal") (EXPAND "headROBEcorrectVal")(expand "numOcc")(expand "chosenFUunique") (expand "busyOpBusyROB")(EXPAND "intBrMatch")(expand "robeMatchesBr") (EXPAND inv1) (EXPAND inv2) (EXPAND inv3) (EXPAND "issuedBefore")(expand "numOccBuffers")(expand "bufferIndex") (EXPAND "weakPreceed")(expand "preceed") (if (eq expocc 't)(then (expand "occ_buffer"))(skip)) (SKOSIMP*) (replace -1)(replace -2)(replace -5)(replace -6) (replace -7) (replace -8) (hide -1 -2 -5 -6 -7 -8) (simp) (if (eq res 't) (then (replace -2 :hide? t)(simp))(skip)) (if (eq hideiex 't)(then (hide -1))(skip)) (if (eq split 't)(then (split +)(skosimp*)(simp))(skip))) "Expands out rho, skosimps, replaces and hides" " " ) (defstep expand-retire (&optional (inv1 nil)(inv2 nil)(inv3 nil)(inv4 nil)(inv5 nil)(split t)) (then (EXPAND "rho_retire")(expand "succ") (EXPAND inv1) (EXPAND inv2) (EXPAND inv3) (EXPAND inv4) (EXPAND inv5) (SKOSIMP*) (then (split -2) (simp) (REPLACE*) (simp) (hide -1 -2 -3 -4 -5 -6) (if (eq split 't)(then (split 2)(skosimp*)(simp))(skip)))) "Expands out rho, skosimps, replaces and hides" " " ) (defstep exp-inv-retire (&optional (inv1 nil)(inv2 nil)(inv3 nil)(inv4 nil)(inv5 nil)(split t)(expocc t)) (then (EXPAND "rho_retire") (EXPAND "wrapWraps") (EXPAND "headTailEq")(EXPAND "occEqual")(EXPAND "occTailROBfull") (EXPAND "freeHeadROBempty") (EXPAND "occBuffBusyRAT")(EXPAND "busyRAT") (EXPAND "RATpointsNewestBuff")(EXPAND "occRS")(expand "slotUnique") (EXPAND "activeRes")(EXPAND "occRSops")(EXPAND "RS_ROB_opsEqual") (EXPAND "busyROBoccRS")(EXPAND "busyOperandsNearest") (EXPAND "writeBoperandsNearest") (EXPAND "retiredOperandsMatchRF")(EXPAND "activeResOpsNotBusy")(EXPAND "opsMatchROB") (EXPAND "robeMatchesProg")(expand "activeResCorrectVal")(EXPAND "completedROBEcorrectVal") (EXPAND "headROBEcorrectVal")(expand "numOcc") (expand "busyOpBusyROB") (EXPAND "intBrMatch")(expand "robeMatchesBr") (EXPAND inv1) (EXPAND inv2) (EXPAND inv3) (EXPAND inv4) (EXPAND inv5) (EXPAND "issuedBefore")(expand "numOccBuffers")(expand "bufferIndex") (EXPAND "weakPreceed")(expand "preceed") (if (eq expocc 't)(then (expand "occ_buffer"))(skip)) (expand "succ") (SKOSIMP*) (then (split -2) (simp) (REPLACE*) (simp) (hide -1 -2 -3 -4 -5 -6 ) (if (eq split 't)(then (split 2)(skosimp*)(simp))(skip)))) "Expands out rho, skosimps, replaces and hides" " " ) (defstep expand-extint (&optional (inv1 nil)(inv2 nil)(inv3 nil)(inv4 nil)(inv5 nil)) (then (EXPAND "rho_extint") (EXPAND inv1) (EXPAND inv2) (EXPAND inv3) (EXPAND inv4) (EXPAND inv5) (SKOSIMP*) (REPLACE*) (simp) (hide -1 -2 -4 -5 -6)) "Expands out rho, skosimps, replaces and hides" " " ) (defstep exp-inv-extint (&optional (inv1 nil)(inv2 nil)(inv3 nil)(inv4 nil)(inv5 nil)(split t)) (then (EXPAND "rho_extint") (EXPAND "wrapWraps") (EXPAND "headTailEq")(EXPAND "occEqual")(EXPAND "occTailROBfull") (EXPAND "freeHeadROBempty") (EXPAND "occBuffBusyRAT")(EXPAND "busyRAT")(EXPAND "RATpointsNewestBuff") (EXPAND "occRS")(expand "slotUnique") (EXPAND "activeRes") (EXPAND "occRSops")(EXPAND "RS_ROB_opsEqual") (EXPAND "busyROBoccRS") (EXPAND " busyOperandsNearest")(EXPAND "writeBoperandsNearest")(EXPAND "intBrMatch") (EXPAND "retiredOperandsMatchRF")(EXPAND "activeResOpsNotBusy")(EXPAND "opsMatchROB") (EXPAND "robeMatchesProg")(expand "activeResCorrectVal")(EXPAND "completedROBEcorrectVal") (EXPAND "headROBEcorrectVal")(expand "numOcc")(expand "busyOpBusyROB") (EXPAND inv1) (EXPAND inv2) (EXPAND inv3) (EXPAND inv4) (EXPAND inv5) (EXPAND "issuedBefore")(expand "numOccBuffers")(expand "bufferIndex") (EXPAND "weakPreceed")(expand "preceed")(expand "occ_buffer") (SKOSIMP*) (REPLACE*) (simp) (hide -1 -2 -4 -5 ) (if (eq split 't)(then (split +)(skosimp*)(simp))(skip))) "Expands out rho, skosimps, replaces and hides" " " ) (defstep expand-out (&optional (inv nil)) (then (EXPAND "PredInv")(EXPAND "rho")(EXPAND inv) (SKOSIMP*) (REPLACE*) (simp) (HIDE -4 -5 -6 -7) ) "Expands out the definitions, and rho, replaces and hides " " " ) (defstep expand-out-prop (&optional (inv nil)(dir +)) (then (EXPAND "rho")(expand "TomInvariants")(skosimp*) (expand inv dir)(skosimp*)(replace*)(simp)(hide -4 -5 -6 -7)) "Expands out the defintions, and rho, replaces and hides. The optional invariant is only expanded in succeedents, or as specified by dir" " " ) (defstep do-rewrites (&optional (toexpand nil)) (apply (then (AUTO-REWRITE-THEORY "TomPropRewrite") (expand toexpand)(SIMP) (SIMPLIFY-WITH-REWRITES :DEFS T :EXCLUDE "FUn") (auto-rewrite-ante)(assert))) "Rewrites using theory TomPropRewrite, expands an optional statement, simplifies, then SIMPLIFY-WITH-REWRITES" " Rewrites using theory TomPropRewrite, expands an optional statement, simplifies, then SIMPLIFY-WITH-REWRITES" ) (defstep lift-split(&optional (num +)) (then (lift-if +)(split num)(simp)(replace*)(simp)) "Lift, split, replace and simplify " " " ) (defstep instbest (&optional (fnum *)) (then (inst? fnum :if-match best)) "Applies inst? :if-match best to the optional line number (num, +, -)" " " ) (defstep lazy-grind (&optional (if-match t) (defs !) rewrites theories exclude (updates? t)) (then (grind$ :if-match nil :defs defs :rewrites rewrites :theories theories :exclude exclude :updates? updates?) (reduce$ :if-match if-match :updates? updates?)) "Equiv. to (grind) with the instantiations postponed until after simplification." "By skolemization, if-lifting, simplification and instantiation") (defstep stew (&optional lazy-match (if-match t) (defs !) rewrites theories exclude (updates? t) &rest lemmas) (then (if lemmas (let ((lemmata (if (listp lemmas) lemmas (list lemmas))) (x `(then ,@(loop for lemma in lemmata append `((skosimp*)(use ,lemma)))))) x) (skip)) (if lazy-match (then (grind$ :if-match nil :defs defs :rewrites rewrites :theories theories :exclude exclude :updates? updates?) (reduce$ :if-match if-match :updates? updates?)) (grind$ :if-match if-match :defs defs :rewrites rewrites :theories theories :exclude exclude :updates? updates?))) "Does a combination of (lemma) and (grind)." "~%Grinding away with the supplied lemmas,") (defstep split-if (&optional (fnum *)) (then (lift-if) (let ((fnums (gather-fnums (s-forms (current-goal *ps*)) fnum nil #'(lambda (sform) (or (branch? (formula sform)) (and (negation? (formula sform)) (branch? (args1 (formula sform)))))))) (fnum (when fnums (car fnums)))) (if fnum (split fnum) (skip-msg "No IF-THEN-ELSE in the sequent.")))) "Applies LIFT-IF and splits only an IF-THEN-ELSE sequent formula in the result." "Lifting IF-THEN-ELSEs and splitting on an IF-THEN-ELSE") (defstep split-if-new (&optional (fnum *)) (try (lift-if fnum) (let ((newfnum (car *new-fmla-nums*))) (if newfnum (then (split newfnum)(split-if-new$ fnum)) (skip-msg "No IF-THEN-ELSE in the sequent."))) (skip-msg "Nothing to lift-if.")) "Applies LIFT-IF and splits only an IF-THEN-ELSE sequent formula in the result." "Lifting IF-THEN-ELSEs and splitting on an IF-THEN-ELSE") (defstep new-split-if (&optional (fnum +)) (then (split-if fnum)(simp)(replace*)(simp)) "Lift, split, replace and simplify " " " ) (defstep split-if-simp (&optional (fnum +)) (then (lift-if fnum)(then (split fnum)(simp))) "Lift, split and simplify " " " ) (defstep clean-up () (let ( ;(fmla (formula sform)) (fnums (gather-fnums (s-forms (current-goal *ps*)) * nil #'(lambda (sform) (or (and (negation? (formula sform)) (and (implication? (args1 (formula sform))) (tc-eq (args1 (args1 (formula sform))) *false*))) (and (conjunction? (formula sform)) (or (tc-eq (args1 (formula sform)) *false*) (tc-eq (args1 (formula sform)) *false*))))))) (fnum (when fnums (car fnums)))) (if fnum (hide fnums)(skip-msg "No formulae to clean-up"))) "Hide all antecedents of the form FALSE IMPLIES X and consequents FALSE AND Y " "Hide all antecedents of the form FALSE IMPLIES X and consequents FALSE AND Y" ) (defstep reduce-if (&optional (toreplace nil)(exclude nil)) (let ( ;(fmla (formula sform)) (fnums (gather-fnums (s-forms (current-goal *ps*)) * exclude #'(lambda (sform) (and (negation? (formula sform)) (and (branch? (args1 (formula sform))) (or (tc-eq (then-part (args1 (formula sform))) *false*) (tc-eq (else-part (args1 (formula sform))) *false*))))))) (fnum (when fnums (car fnums)))) (if fnum (then (split fnum)(flatten)(replace toreplace)) (skip-msg "Nothing to reduce if"))) "Split an antecedent if-formula if either the then-part or the else-part is false" "Reducing void if-formulae" ) (defstep split-all (&optional (fnum nil)(sko t)) (repeat* (then (split-if$ +)(simp$)(if (eq sko 't)(skosimp*)(skip))(replace*)(simp$)(reduce-if$) (then (split-if$ fnum)(simp$)(replace*)(simp$)))) "Lift, splits consequents and those in fnum, if specified. Antecedents with FALSE then or else-parts also split" "Splitting consequents and antecedents with FALSE then- or else-parts " ) (defstep split-all-sko (&optional (fnum nil)(sko t)) (repeat* (then (split-if$ +)(simp$)(if (eq sko 't) (skosimp*)(skip))(replace*)(simp$)(reduce-if$) (then (split-if$ fnum)(simp$)(replace*)(simp$)))) "Lift, splits consequents and those in fnum, if specified. Antecedents with FALSE then or else-parts also split. Also skolemize" "Splitting consequents and antecedents with FALSE then- or else-parts. Also skolemize " ) (defstep simp-split (&optional (fnum +)) (then (lift-if)(then (split fnum)(simp))) "lift-if, split, simp" "lift-if, split, simp" ) (defstep rewrite-all (fnums) (let ((fnum (car fnums)) (rems (cdr fnums))) (if fnum (then (auto-rewrite fnum)(rewrite-all$ rems)) (skip-msg "Auto-rewrote all formulae"))) " " " " ) (defstep auto-rewrite-ante-new (&optional (exclude nil)) (let ( ;(fmla (formula sform)) ( fnums (gather-fnums (s-forms (current-goal *ps*)) * exclude #'(lambda (sform) (and (negation? (formula sform)) (or (and (forall-expr? (args1 (formula sform))) (implication? (expression (args1 (formula sform))))) (and (implication? (args1 (formula sform))) (not (equality? (args2 (args1 (formula sform) )))))))))) (fnum (when fnums (car fnums)))) (if fnum (rewrite-all$ fnums) (skip-msg "Nothing to auto-rewrite"))) " " " " ) (defstep auto-rewrite-ante (&optional (exclude nil)) (let ( ;(fmla (formula sform)) ( fnums (gather-fnums (s-forms (current-goal *ps*)) * exclude #'(lambda (sform) (and (negation? (formula sform)) (or (and (forall-expr? (args1 (formula sform))) (implication? (expression (args1 (formula sform))))) (implication? (args1 (formula sform)))))))) (fnum (when fnums (car fnums)))) (if fnum (rewrite-all$ fnums) (skip-msg "Nothing to auto-rewrite"))) " " " " ) (defstep hide-all-but (&optional (hidefrom *) keepnums) (let ((fnums (gather-fnums (s-forms (current-goal *ps*)) hidefrom keepnums))) (hide :fnums fnums)) "Hides all sequent formulas from FNUMS except those listed in KEEP-FNUMS. Useful when all but a few formulas need to be hidden." "Hiding ~a but keeping ~a") (defstep my-hide-all-but (keepnums &optional (hidefrom *)) (let ((fnums (gather-fnums (s-forms (current-goal *ps*)) hidefrom keepnums))) (hide :fnums fnums)) "Hides all sequent formulas" "Hiding" ) (defstep prove-rewrites (&optional (prop nil)) (apply (then (EXPAND prop)(skosimp*)(iff)(then (split)(skosimp*)(repeat* (then (split 1)(skosimp*)))))) "Expands out the definitions, and rho, replaces and hides " " " ) (defstep reduce-all (&optional (fnum nil)(sko t)) (repeat* (then (reduce-if$ +)(simp$)(if (eq sko 't)(skosimp*)(skip))(replace*)(simp$))) "Split all antecedent if-formulae where either the then-part or the else-part is false. Skolemizes and replaces" "Splitting all if-then antecedents with false" ) (defstep replace-all (fnums into) (let ((fnum (car fnums)) (rems (cdr fnums))) (if fnum (then (replace fnum into)(replace-all$ rems into)) (skip-msg " "))) " " " " ) (defstep rep-plus(&optional (fnum +)) (let ((fnums (gather-fnums (s-forms (current-goal *ps*)) * +)) (first (when fnums (car fnums)))) (if first (then (replace-all fnums fnum)(simp)) (skip-msg "No IF-THEN-ELSE in the sequent."))) " replace" " replace" ) $$$allTheories.pvs allTheories[R, U, Z: posnat, (IMPORTING more_nat_types[1]) B: greater_one_nat]: THEORY % This is just a dummy file allowing all the proofs to be dumped together. % It imports the three refinements: % Refine : DES refines Seq % Live : DES can always progress ("liveness" proof) % SplitEqual : The Split transition relation can do everything done in % the parallel one % Other files imported indirectly are: % Spec : The speculative design. Called DES in the paper % seq : The sequential design % IOdef : Definitions used in Spec % def : Definitions used in both Spec and Seq % more_nat_types : Definitions used in both Spec and Seq % InvDefs1,2,3 : Definitions of properties of Spec to be proved invariant % Invs1,2,3 : Proof of the invariance of these properties % OneRho : The parallel transition relation % % Note: % The proof of liveness and that the split transition relation does not lose behaviours % is equivalent for both the inductive and the direct proof, modulo some auxiliary % variables. It is included in these dump files for convenience. % BEGIN IMPORTING Refine[R,U,Z,B], live[R, U, Z, B], SplitEqual[R, U, Z, B] END allTheories $$$oneRho.pvs oneRho[R,U,Z: posnat, (IMPORTING more_nat_types[1]) B: greater_one_nat ]: THEORY % As transition relation for the speculative system issuing, executing, and retiring % simultaneously BEGIN IMPORTING IOdef[R,U,Z,B] RF, RF_p: VAR [REG_ID -> RF_TYPE] RAT, RAT_p: VAR [REG_ID -> RAT_TYPE] ROB, ROB_p: VAR ROB_TYPE RS, RS_p: VAR [SLOT_ID -> RS_TYPE] res, res_p: VAR [FU_ID -> result_TYPE] pc, pc_p : VAR posnat numinst, numinst_p : VAR nat FU: VAR FU_ID S: VAR SLOT_ID r: VAR REG_ID rb : VAR ROB_ID rho(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p, res): bool = (EXISTS ( retire: boolean): (retire IMPLIES can_retire(ROB) AND occ_buffer(head(ROB), ROB) AND NOT b(robe(ROB)(head(ROB)))) AND IF (retire AND (int(robe(ROB)(head(ROB))) OR (type_op(op(robe(ROB)(head(ROB)))) = BRANCH AND EXOR(br_pred(robe(ROB)(head(ROB))), v(robe(ROB)(head(ROB))) > 0)))) THEN % flush on internal interrupt of branch mispredict RF_p = IF int(robe(ROB)(head(ROB))) THEN RF ELSE (LAMBDA r: IF r = t(robe(ROB)(head(ROB))) THEN IF v( robe(ROB)(head(ROB))) > 0 THEN (# v := 1#) ELSE (# v := 0#) ENDIF ELSE RF(r) ENDIF) ENDIF AND RAT_p = (LAMBDA r: (# b:= FALSE, al := B #)) AND ROB_p = (# tail := 1, head := 1, wrap := FALSE, robe := (LAMBDA rb: robe(ROB)(rb) WITH [ b := FALSE, oc := FALSE ]) #) AND RS_p = (LAMBDA S: RS(S) with [oc := FALSE]) AND numinst_p = numinst + 1 AND pc_p = IF (int(robe(ROB)(head(ROB)))) THEN Int_interrupt_addr(pc(robe(ROB)(head(ROB))), type_op(op(robe(ROB)(head(ROB))))) ELSIF v(robe(ROB)(head(ROB))) > 0 THEN br_targ(robe(ROB)(head(ROB))) ELSE pc(robe(ROB)(head(ROB))) + 1 ENDIF ELSE % general case of no flush / interrupt (EXISTS (Sn: upto[Z]), (exec: [FU_ID -> boolean]), (iex: [FU_ID -> SLOT_ID]): (Sn > 0 IMPLIES (can_issue(ROB) AND dispatch(RS, ROB, Sn))) AND (FORALL (FU: FU_ID): exec(FU) IMPLIES can_execute(ROB) AND enabled(RS, iex(FU)) AND fu_table(op(RS(iex(FU)))) = FU) AND res = (LAMBDA (FU: FU_ID): IF exec(FU) THEN (# a := TRUE, p := p(RS(iex(FU))), v := IF type_op(op(RS(iex(FU)))) /= BRANCH THEN do_op(op(RS(iex(FU))), v(ss(RS(iex(FU)))(1)), v(ss(RS(iex(FU)))(2))) ELSIF branch_act(pc(robe(ROB)(p(RS(iex(FU))))), issuedBefore(numinst, ROB, p(RS(iex(FU)))) +1) THEN 1 ELSE 0 ENDIF, int := int_interrupt(pc(robe(ROB)(p(RS(iex(FU))))), issuedBefore(numinst, ROB, p(RS(iex(FU)))) +1) #) ELSE (# a:= false, p:= 1, v:= 0, int:= false #) ENDIF) and numinst_p = IF NOT retire THEN numinst ELSE numinst +1 ENDIF AND pc_p = IF Sn > 0 THEN IF type_op(op(prog(pc))) = BRANCH AND branch_pred(pc, totalIssued(numinst, ROB) + 1) THEN br_target(prog(pc)) ELSE 1 + pc ENDIF ELSE pc ENDIF AND RAT_p = (LAMBDA r: IF Sn > 0 AND r = t(prog(pc)) THEN (# b := TRUE , al := tail(ROB) #) ELSIF retire AND al(RAT(r)) = head(ROB) THEN (# b := FALSE, al := al(RAT(r)) #) ELSE RAT(r) ENDIF) AND RF_p = IF NOT retire THEN RF ELSE (LAMBDA r: IF r = t(robe(ROB)(head(ROB))) THEN (# v := v(robe(ROB)(head(ROB))) #) ELSE RF(r) ENDIF) ENDIF AND ROB_p = (# head := IF retire THEN succ(head(ROB)) ELSE head(ROB) ENDIF, tail := IF Sn > 0 THEN succ(tail(ROB)) ELSE tail(ROB) ENDIF, wrap := (wrap(ROB) AND NOT (retire AND succ(head(ROB)) = 1)) OR (Sn > 0 AND succ(tail(ROB)) = 1), robe := (LAMBDA rb: IF (Sn> 0 AND rb = tail(ROB)) THEN %dispatching new instr (# b := TRUE, v := 0, op := op(prog(pc)), int := FALSE, oc := TRUE, br_pred := branch_pred(pc, totalIssued(numinst, ROB) + 1), br_targ := br_target(prog(pc)), t := t(prog(pc)), pc := pc, ss := (LAMBDA (j: TWO): IF b(RAT(src(prog(pc))(j))) THEN IF retire AND al(RAT(src(prog(pc))(j))) = head(ROB) THEN (# st := RETIRED, p := al(RAT(src(prog(pc))(j))), v := v(robe(ROB)(al(RAT(src(prog(pc))(j))))), r := src(prog(pc))(j) #) ELSIF (EXISTS FU: a(res(FU)) AND % writeback al(RAT(src(prog(pc))(j))) = p(res(FU))) THEN (# st := WRITE_B, p := al(RAT(src(prog(pc))(j))), v := v(res(chooseFU(al(RAT(src(prog(pc))(j))), res))), r := src(prog(pc))(j) #) ELSE (# st := IF b(robe(ROB)(al(RAT(src(prog(pc))(j))))) THEN BUSY ELSE WRITE_B ENDIF, p := al(RAT(src(prog(pc))(j))), v := v(robe(ROB)(al(RAT(src(prog(pc))(j))))), r := src(prog(pc))(j) #) ENDIF ELSE % NOT b(RAT(src(prog(pc))(j))) (# st := RETIRED, v := v(RF(src(prog(pc))(j))), r := src(prog(pc))(j), p := al(RAT(src(prog(pc))(j))) #) ENDIF) #) ELSIF rb = head(ROB) and retire THEN robe(ROB)(rb) WITH [oc := FALSE] ELSIF occ_buffer(rb, ROB) AND % this buffer is being written back (EXISTS FU: a(res(FU)) AND p(res(FU)) = rb) THEN (# b := FALSE, v := v(res(chooseFU(rb, res))), int := int(res(chooseFU(rb, res))), t := t(robe(ROB)(rb)), pc := pc(robe(ROB)(rb)), op := op(robe(ROB)(rb)), br_pred := br_pred(robe(ROB)(rb)), br_targ := br_targ(robe(ROB)(rb)), oc := oc(robe(ROB)(rb)), ss := (LAMBDA (j: TWO): IF retire AND p(ss(robe(ROB)(rb))(j)) = head(ROB) THEN (# st := RETIRED, v := v(ss(robe(ROB)(rb))(j)), p := p(ss(robe(ROB)(rb))(j)), r := r(ss(robe(ROB)(rb))(j)) #) ELSE ss(robe(ROB)(rb))(j) ENDIF) #) ELSIF occ_buffer(rb, ROB) THEN robe(ROB)(rb) WITH [ss := (LAMBDA (j: TWO): IF retire AND p(ss(robe(ROB)(rb))(j)) = head(ROB) THEN (# st := RETIRED, v := v(ss(robe(ROB)(rb))(j)), p := p(ss(robe(ROB)(rb))(j)), r := r(ss(robe(ROB)(rb))(j)) #) ELSIF st(ss(robe(ROB)(rb))(j)) = BUSY AND (EXISTS FU: a(res(FU)) AND p(ss(robe(ROB)(rb))(j))= p(res(FU)) AND p(ss(robe(ROB)(rb))(j)) > 0) THEN (# st := WRITE_B, v := v(res(chooseFU(p(ss(robe(ROB)(rb))(j)), res))), p := p(ss(robe(ROB)(rb))(j)), r := r(ss(robe(ROB)(rb))(j)) #) ELSE ss(robe(ROB)(rb))(j) ENDIF)] ELSE robe(ROB)(rb) ENDIF ) #) AND RS_p = (LAMBDA S: IF (EXISTS FU : a(res(FU)) AND S = iex(FU)) THEN RS(S) with [oc := FALSE] ELSIF S = Sn THEN (# oc := TRUE, p := tail(ROB), op := op(prog(pc)), ss := (LAMBDA (j: TWO): IF b(RAT(src(prog(pc))(j))) THEN IF retire AND al(RAT(src(prog(pc))(j))) = head(ROB) THEN (# st := RETIRED, p := al(RAT(src(prog(pc))(j))), v := v(robe(ROB)(al(RAT(src(prog(pc))(j))))), r := src(prog(pc))(j) #) ELSIF (EXISTS FU: a(res(FU)) AND al(RAT(src(prog(pc))(j))) = p(res(FU))) THEN (# st := WRITE_B, p := al(RAT(src(prog(pc))(j))), v := v(res(chooseFU(al(RAT(src(prog(pc))(j))), res))), r := src(prog(pc))(j) #) ELSE (# st := IF b(robe(ROB)(al(RAT(src(prog(pc))(j))))) THEN BUSY ELSE WRITE_B ENDIF, p := al(RAT(src(prog(pc))(j))), v := v(robe(ROB)(al(RAT(src(prog(pc))(j))))), r := src(prog(pc))(j) #) ENDIF ELSE % NOT b(RAT(src(prog(pc))(j))) (# st := RETIRED, v := v(RF(src(prog(pc))(j))), r := src(prog(pc))(j), p := al(RAT(src(prog(pc))(j))) #) ENDIF) #) ELSIF oc(RS(S)) THEN % check for retirement and writeb RS(S) WITH [ ss := (LAMBDA (j: TWO): IF retire AND p(ss(RS(S))(j)) = head(ROB) THEN (# st := RETIRED, p := p(ss(RS(S))(j)), v := v(ss(RS(S))(j)), r := r(ss(RS(S))(j)) #) ELSIF st(ss(RS(S))(j)) = BUSY AND (EXISTS FU: a(res(FU)) AND p(ss(RS(S))(j)) = p(res(FU)) AND p(ss(RS(S))(j)) > 0) THEN (# st := WRITE_B, p := p(ss(RS(S))(j)), v := v(res(chooseFU(p(ss(RS(S))(j)), res))), r := r(ss(RS(S))(j)) #) ELSE ss(RS(S))(j) ENDIF)] ELSE RS(S) ENDIF )) ENDIF ) END oneRho $$$oneRho.prf (|oneRho| (|rho_TCC1| "" (SUBTYPE-TCC) NIL) (|rho_TCC2| "" (SUBTYPE-TCC) NIL) (|rho_TCC3| "" (SUBTYPE-TCC) NIL) (|rho_TCC4| "" (EXPAND "chooseFU") (("" (SKOSIMP*) (("" (NEW-SPLIT-IF -14) (("" (INST? +) (("" (REDUCE-IF) (("" (SIMP) NIL))))))))))) (|rho_TCC5| "" (EXPAND "chooseFU") (("" (SKOSIMP*) (("" (INSTBEST -) (("" (NEW-SPLIT-IF -12) (("" (INSTBEST +) NIL))))))))) (|rho_TCC6| "" (EXPAND "chooseFU") (("" (SKOSIMP*) (("" (NEW-SPLIT-IF -14) (("" (INST?) (("" (SIMP) NIL))))))))) (|rho_TCC7| "" (EXPAND "chooseFU") (("" (SKOSIMP*) (("" (INSTBEST -) (("" (NEW-SPLIT-IF -14) (("" (INSTBEST +) (("" (SIMP) NIL))))))))))) (|rho_TCC8| "" (EXPAND "chooseFU") (("" (SKOSIMP*) (("" (INSTBEST -) (("" (NEW-SPLIT-IF -15) (("" (INST? +) (("" (REDUCE-IF) (("" (SIMP) NIL)))))))))))))) $$$SplitEqual.pvs SplitEqual[R, U, Z: posnat, (IMPORTING more_nat_types[1]) B: greater_one_nat]: THEORY % The proof that any situation reached by one transition of the joint, parallel, % transition relation (oneRho) can also be reached by 3 transition of the split % transition relation (Spec) - first issuing, then executing and writing back % and finally retiring. % Thus by splitting the transition relation we do not "lose" any interesting % behaviours. BEGIN IMPORTING oneRho[R, U, Z, B], Invs3[R, U, Z, B] RF, RF_p: VAR [REG_ID -> RF_TYPE] RAT, RAT_p, RAT_I: VAR [REG_ID -> RAT_TYPE] ROB, ROB_p, ROB_I, ROB_W: VAR ROB_TYPE RS, RS_p, RS_I, RS_E, RS_W: VAR [SLOT_ID -> RS_TYPE] res, res_p, res_E, res_W: VAR [FU_ID -> result_TYPE] pc, pc_p, pc_I: VAR posnat numinst, numinst_p: VAR nat FU: VAR FU_ID S: VAR SLOT_ID r: VAR REG_ID rb: VAR ROB_ID chosenFUnonzero: LEMMA (FORALL res, FU: a(res(FU)) IMPLIES chooseFU(p(res(FU)), res) > 0 AND a(res(chooseFU(p(res(FU)), res)))) splitEquiv: LEMMA rho(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p, res) AND AllInvariants(RF, RS, RAT, ROB, numinst, pc) IMPLIES (EXISTS RS_I, RAT_I, ROB_I, pc_I: rho_issue(pc, RF, RS, RAT, ROB, numinst, pc_I, RF, RS_I, RAT_I, ROB_I, numinst) AND AllInvariants(RF, RS_I, RAT_I, ROB_I, numinst, pc_I) AND (EXISTS res, RS_W, ROB_W: rho_writeb(pc_I, RF, RS_I, RAT_I, ROB_I, numinst, pc_I, RF, RS_W, RAT_I, ROB_W, numinst, res) AND AllInvariants(RF, RS_W, RAT_I, ROB_W, numinst, pc_I) AND rho_retire(pc_I, RF, RS_W, RAT_I, ROB_W, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p) AND AllInvariants(RF_p, RS_p, RAT_p, ROB_p, numinst_p, pc_p))) END SplitEqual $$$SplitEqual.prf (|SplitEqual| (|chosenFUnonzero_TCC1| "" (SUBTYPE-TCC) NIL) (|chosenFUnonzero| "" (EXPAND "chooseFU") (("" (EXPAND "choose") (("" (SKOSIMP*) (("" (NEW-SPLIT-IF) (("1" (USE "epsilon_ax[FU_ID]") (("1" (SPLIT -) (("1" (SIMP) NIL) ("2" (SKOSIMP*) (("2" (INST? +) (("2" (SIMP) NIL))))))))) ("2" (INSTBEST) (("2" (SIMP) NIL))))))))))) (|splitEquiv| "" (SKOSIMP*) (("" (HIDE -1 -2) (("" (REVEAL -1 -2) (("" (EXPAND "rho") (("" (SKOSIMP*) (("" (APPLY (THEN (SPLIT -2) (SIMP))) (("1" (INST? +) (("1" (SIMP) (("1" (SPLIT +) (("1" (EXPAND "rho_issue") (("1" (INST 1 "0") (("1" (SIMP) (("1" (APPLY (THEN (SPLIT +) (SIMP))) (("1" (APPLY-EXTENSIONALITY 1 :HIDE? T) NIL) ("2" (APPLY-EXTENSIONALITY 1 :HIDE? T) NIL))))) ("2" (SIMP) NIL))))) ("2" (INST 1 "(lambda FU : (# a:= false, p:= 1, v:= 0, int:= false #))" "RS!1" "ROB!1") (("2" (SIMP) (("2" (CASE "not rho_writeb(pc!1, RF!1, RS!1, RAT!1, ROB!1, numinst!1, pc!1, RF!1, RS!1, RAT!1, ROB!1, numinst!1, (LAMBDA FU: (# a := FALSE, p := 1, v := 0, int := FALSE #)))") (("1" (HIDE 2) (("1" (EXPAND "rho_writeb") (("1" (INST 1 "(lambda FU : false)" "(lambda FU : Z)") (("1" (SPLIT +) (("1" (SKOSIMP*) (("1" (SIMP) NIL))) ("2" (SIMP) NIL) ("3" (APPLY (THEN (REPEAT* (THEN (APPLY-EXTENSIONALITY 1 :HIDE? T) (NEW-SPLIT-IF))))) NIL) ("4" (APPLY (THEN (REPEAT* (THEN (APPLY-EXTENSIONALITY 1 :HIDE? T) (NEW-SPLIT-IF))))) NIL))) ("2" (SIMP) NIL))))))) ("2" (SIMP) (("2" (CASE "not rho_retire(pc!1, RF!1, RS!1, RAT!1, ROB!1, numinst!1, pc_p!1, RF_p!1, RS_p!1, RAT_p!1, ROB_p!1, numinst_p!1)") (("1" (HIDE 2) (("1" (EXPAND "rho_retire") (("1" (INST 1 "retire!1") (("1" (SIMP) (("1" (SPLIT +) (("1" (SIMP) NIL) ("2" (SIMP) (("2" (REPLACE*) (("2" (SIMP) NIL))))))))))))))) ("2" (SIMP) (("2" (LEMMA "AllInvariants_retire") (("2" (INST?) (("2" (SIMP) NIL))))))))))))))))))))))) ("2" (SKOSIMP*) (("2" (CASE "not (exists (RSI : [SLOT_ID[R, U, Z, B] -> RS_TYPE[R, U, Z, B]]): RSI = (LAMBDA S: IF S /= Sn!1 THEN RS!1(S) ELSE (# oc := TRUE, p := tail(ROB!1), op := op(prog(pc!1)), ss := (LAMBDA (j: TWO): IF b(RAT!1(src(prog(pc!1))(j))) THEN (# st := IF b(robe(ROB!1)(al(RAT!1(src(prog(pc!1))(j))))) THEN BUSY ELSE WRITE_B ENDIF, p := al(RAT!1(src(prog(pc!1))(j))), v := v(robe(ROB!1)(al(RAT!1(src(prog(pc!1))(j))))), r := src(prog(pc!1))(j) #) ELSE (# st := RETIRED, v := v(RF!1(src(prog(pc!1))(j))), r := src(prog(pc!1))(j), p := al(RAT!1(src(prog(pc!1))(j))) #) ENDIF) #) ENDIF ) )") (("1" (INST 1 " (LAMBDA S: IF S /= Sn!1 THEN RS!1(S) ELSE (# oc := TRUE, p := tail(ROB!1), op := op(prog(pc!1)), ss := (LAMBDA (j: TWO): IF b(RAT!1(src(prog(pc!1))(j))) THEN (# st := IF b (robe(ROB!1) (al (RAT!1 (src(prog(pc!1))(j))))) THEN BUSY ELSE WRITE_B ENDIF, p := al(RAT!1(src(prog(pc!1))(j))), v := v (robe(ROB!1) (al (RAT!1 (src(prog(pc!1))(j))))), r := src(prog(pc!1))(j) #) ELSE (# st := RETIRED, v := v (RF!1 (src(prog(pc!1))(j))), r := src(prog(pc!1))(j), p := al (RAT!1 (src(prog(pc!1))(j))) #) ENDIF) #) ENDIF)") NIL) ("2" (CASE "not (exists (RATI : [REG_ID[R] -> RAT_TYPE[R, U, Z, B]]) : RATI = (LAMBDA r: IF Sn!1 > 0 AND r = t(prog(pc!1)) THEN (# b := TRUE , al := tail(ROB!1) #) ELSE RAT!1(r) ENDIF))") (("1" (INST 1 " (LAMBDA r: IF Sn!1 > 0 AND r = t(prog(pc!1)) THEN (# b := TRUE, al := tail(ROB!1) #) ELSE RAT!1(r) ENDIF)") NIL) ("2" (CASE "not (exists (ROBI : ROB_TYPE): ROBI = IF NOT (Sn!1 > 0) THEN ROB!1 ELSE (# head := head(ROB!1), tail := succ(tail(ROB!1)), wrap := wrap(ROB!1) OR succ(tail(ROB!1)) = 1, robe := (LAMBDA rb: IF rb /= tail(ROB!1) THEN robe(ROB!1)(rb) ELSE (# b := TRUE, v := 0, op := op(prog(pc!1)), int := FALSE, oc := TRUE, br_pred := branch_pred(pc!1, totalIssued(numinst!1, ROB!1) + 1), br_targ := br_target(prog(pc!1)), t := t(prog(pc!1)), pc := pc!1, ss := (LAMBDA (j: TWO): IF b(RAT!1(src(prog(pc!1))(j))) THEN (# st := IF b(robe(ROB!1)(al(RAT!1(src(prog(pc!1))(j))))) THEN BUSY ELSE WRITE_B ENDIF, p := al(RAT!1(src(prog(pc!1))(j))), v := v(robe(ROB!1)(al(RAT!1(src(prog(pc!1))(j))))), r := src(prog(pc!1))(j) #) ELSE (# st := RETIRED, v := v(RF!1(src(prog(pc!1))(j))), r := src(prog(pc!1))(j), p := al(RAT!1(src(prog(pc!1))(j))) #) ENDIF) #) ENDIF) #) ENDIF)") (("1" (INST 1 "IF NOT (Sn!1 > 0) THEN ROB!1 ELSE (# head := head(ROB!1), tail := succ(tail(ROB!1)), wrap := wrap(ROB!1) OR succ(tail(ROB!1)) = 1, robe := (LAMBDA rb: IF rb /= tail(ROB!1) THEN robe(ROB!1)(rb) ELSE (# b := TRUE, v := 0, op := op(prog(pc!1)), int := FALSE, oc := TRUE, br_pred := branch_pred(pc!1, totalIssued (numinst!1, ROB!1) + 1), br_targ := br_target(prog(pc!1)), t := t(prog(pc!1)), pc := pc!1, ss := (LAMBDA (j: TWO): IF b(RAT!1(src(prog(pc!1))(j))) THEN (# st := IF b (robe(ROB!1) (al (RAT!1 (src(prog(pc!1))(j))))) THEN BUSY ELSE WRITE_B ENDIF, p := al (RAT!1(src(prog(pc!1))(j))), v := v (robe(ROB!1) (al (RAT!1 (src(prog(pc!1))(j))))), r := src(prog(pc!1))(j) #) ELSE (# st := RETIRED, v := v (RF!1 (src(prog(pc!1))(j))), r := src(prog(pc!1))(j), p := al (RAT!1 (src(prog(pc!1))(j))) #) ENDIF) #) ENDIF) #) ENDIF") NIL) ("2" (CASE "not (exists (pcI : posnat): pcI = IF Sn!1 > 0 THEN IF type_op(op(prog(pc!1))) = BRANCH AND branch_pred(pc!1, totalIssued(numinst!1, ROB!1) + 1) THEN br_target(prog(pc!1)) ELSE 1 + pc!1 ENDIF ELSE pc!1 ENDIF)") (("1" (INST 1 "IF Sn!1 > 0 THEN IF type_op(op(prog(pc!1))) = BRANCH AND branch_pred(pc!1, totalIssued(numinst!1, ROB!1) + 1) THEN br_target(prog(pc!1)) ELSE 1 + pc!1 ENDIF ELSE pc!1 ENDIF") NIL) ("2" (SKOSIMP*) (("2" (INST 2 "RSI!1" "RATI!1" "ROBI!1" "pcI!1") (("2" (CASE "not rho_issue(pc!1, RF!1, RS!1, RAT!1, ROB!1, numinst!1, pcI!1, RF!1, RSI!1, RATI!1, ROBI!1, numinst!1)") (("1" (HIDE 3) (("1" (EXPAND "rho_issue") (("1" (INST 1 "Sn!1") (("1" (EXPAND "dispatch") (("1" (NEW-SPLIT-IF) NIL))))))))) ("2" (LEMMA "AllInvariants_issue") (("2" (INST?) (("2" (SIMP) (("2" (CASE "not (exists (RSW : [SLOT_ID[R, U, Z, B] -> RS_TYPE[R, U, Z, B]]): RSW = (LAMBDA S: IF (EXISTS FU : a(res!1(FU)) AND p(res!1(FU)) = p(RSI!1(S))) THEN RSI!1(S) with [oc := FALSE] ELSIF oc(RSI!1(S)) THEN (# oc := oc(RSI!1(S)), p := p(RSI!1(S)), op := op(RSI!1(S)), ss := (LAMBDA (j: TWO): IF st(ss(RSI!1(S))(j)) = BUSY AND (EXISTS FU: a(res!1(FU)) AND p(ss(RSI!1(S))(j)) = p(res!1(FU)) AND p(ss(RSI!1(S))(j)) > 0) THEN (# st := WRITE_B, p := p(ss(RSI!1(S))(j)), v := v(res!1(chooseFU(p(ss(RSI!1(S))(j)), res!1))), r := r(ss(RSI!1(S))(j)) #) ELSE ss(RSI!1(S))(j) ENDIF) #) ELSE RSI!1(S) ENDIF ))") (("1" (INST 1 "(LAMBDA S: IF (EXISTS FU: a(res!1(FU)) AND p(res!1(FU)) = p(RSI!1(S))) THEN RSI!1(S) WITH [oc := FALSE] ELSIF oc(RSI!1(S)) THEN (# oc := oc(RSI!1(S)), p := p(RSI!1(S)), op := op(RSI!1(S)), ss := (LAMBDA (j: TWO): IF st(ss(RSI!1(S))(j)) = BUSY AND (EXISTS FU: a(res!1(FU)) AND p(ss(RSI!1(S))(j)) = p(res!1(FU)) AND p(ss(RSI!1(S))(j)) > 0) THEN (# st := WRITE_B, p := p(ss(RSI!1(S))(j)), v := v (res!1 (chooseFU (p(ss(RSI!1(S))(j)), res!1))), r := r(ss(RSI!1(S))(j)) #) ELSE ss(RSI!1(S))(j) ENDIF) #) ELSE RSI!1(S) ENDIF)") (("1" (SKOSIMP*) (("1" (LEMMA "chosenFUnonzero") (("1" (INST? -) (("1" (SIMP) NIL))))))))) ("2" (CASE "not (exists (ROBW : ROB_TYPE): ROBW = (# head := head(ROBI!1), tail := tail(ROBI!1), wrap := wrap(ROBI!1), robe := (LAMBDA rb: IF occ_buffer(rb, ROBI!1) AND (EXISTS FU: a(res!1(FU)) AND p(res!1(FU)) = rb) THEN (# b := FALSE, v := v(res!1(chooseFU(rb, res!1))), int := int(res!1(chooseFU(rb, res!1))), t := t(robe(ROBI!1)(rb)), ss := ss(robe(ROBI!1)(rb)), pc := pc(robe(ROBI!1)(rb)), op := op(robe(ROBI!1)(rb)), br_pred := br_pred(robe(ROBI!1)(rb)), br_targ := br_targ(robe(ROBI!1)(rb)), oc := oc(robe(ROBI!1)(rb)) #) ELSIF occ_buffer(rb, ROBI!1) THEN robe(ROBI!1)(rb) WITH [ss := (LAMBDA (j: TWO): IF st(ss(robe(ROBI!1)(rb))(j)) = BUSY AND (EXISTS FU: a(res!1(FU)) AND p(ss(robe(ROBI!1)(rb))(j)) = p(res!1(FU)) AND p(ss(robe(ROBI!1)(rb))(j)) > 0) THEN (# st := WRITE_B, p := p(ss(robe(ROBI!1)(rb))(j)), v := v(res!1(chooseFU(p(ss(robe(ROBI!1)(rb))(j)), res!1))), r := r(ss(robe(ROBI!1)(rb))(j)) #) ELSE ss(robe(ROBI!1)(rb))(j) ENDIF)] ELSE robe(ROBI!1)(rb) ENDIF ) #))") (("1" (INST 1 "(# head := head(ROBI!1), tail := tail(ROBI!1), wrap := wrap(ROBI!1), robe := (LAMBDA rb: IF occ_buffer(rb, ROBI!1) AND (EXISTS FU: a(res!1(FU)) AND p(res!1(FU)) = rb) THEN (# b := FALSE, v := v(res!1(chooseFU(rb, res!1))), int := int(res!1(chooseFU(rb, res!1))), t := t(robe(ROBI!1)(rb)), ss := ss(robe(ROBI!1)(rb)), pc := pc(robe(ROBI!1)(rb)), op := op(robe(ROBI!1)(rb)), br_pred := br_pred(robe(ROBI!1)(rb)), br_targ := br_targ(robe(ROBI!1)(rb)), oc := oc(robe(ROBI!1)(rb)) #) ELSIF occ_buffer(rb, ROBI!1) THEN robe(ROBI!1)(rb) WITH [ss := (LAMBDA (j: TWO): IF st (ss(robe(ROBI!1)(rb)) (j)) = BUSY AND (EXISTS FU: a(res!1(FU)) AND p (ss(robe(ROBI!1)(rb)) (j)) = p(res!1(FU)) AND p (ss(robe(ROBI!1)(rb)) (j)) > 0) THEN (# st := WRITE_B, p := p (ss(robe(ROBI!1)(rb)) (j)), v := v (res!1 (chooseFU (p (ss(robe(ROBI!1)(rb)) (j)), res!1))), r := r (ss(robe(ROBI!1)(rb)) (j)) #) ELSE ss(robe(ROBI!1)(rb)) (j) ENDIF)] ELSE robe(ROBI!1)(rb) ENDIF) #)") (("1" (SKOSIMP*) (("1" (LEMMA "chosenFUnonzero") (("1" (INST? -) (("1" (SIMP) NIL))))))) ("2" (SKOSIMP*) (("2" (LEMMA "chosenFUnonzero") (("2" (INST? -) (("2" (SIMP) NIL))))))))) ("2" (SKOSIMP*) (("2" (INST 2 "res!1" "RSW!1" "ROBW!1") (("2" (CASE "not rho_writeb(pcI!1, RF!1, RSI!1, RATI!1, ROBI!1, numinst!1, pcI!1, RF!1, RSW!1, RATI!1, ROBW!1, numinst!1, res!1)") (("1" (HIDE 3) (("1" (EXPAND "rho_writeb") (("1" (INST 1 "exec!1" "iex!1") (("1" (CASE "not (FORALL (FU: FU_ID[R, U, Z, B]): exec!1(FU) IMPLIES can_execute(ROBI!1) AND enabled(RSI!1, iex!1(FU)) AND fu_table(op(RSI!1(iex!1(FU)))) = FU)") (("1" (HIDE 2) (("1" (SKOSIMP*) (("1" (EXPAND "can_execute") (("1" (EXPAND "enabled") (("1" (INST? -) (("1" (SIMP) (("1" (REP-PLUS) (("1" (REP-PLUS) (("1" (LIFT-IF +) (("1" (SPLIT +) (("1" (SIMP) NIL) ("2" (SIMP) (("2" (SIMP) (("2" (SPLIT +) (("1" (SKOSIMP*) (("1" (EXPAND "dispatch") (("1" (PROPAX) NIL))))) ("2" (EXPAND "dispatch") (("2" (PROPAX) NIL))))))))))))))))))))))))))))) ("2" (EXPAND "dispatch") (("2" (SPLIT +) (("1" (PROPAX) NIL) ("2" (REP-PLUS) (("2" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("2" (CASE "exec!1(x!1)") (("1" (SIMP) (("1" (CASE "iex!1(x!1) = Sn!1") (("1" (SIMP) (("1" (EXPAND "enabled") (("1" (INST?) (("1" (INST?) (("1" (SIMP) NIL))))))))) ("2" (SIMP) (("2" (CASE "type_op(op(RS!1(iex!1(x!1)))) /= BRANCH") (("1" (SIMP) (("1" (CASE "Sn!1 = 0") (("1" (SIMP) NIL) ("2" (SIMP) (("2" (EXPAND "issuedBefore") (("2" (EXPAND "bufferIndex") (("2" (CASE "p(RS!1(iex!1(x!1))) /= tail(ROB!1)") (("1" (SIMP) NIL) ("2" (EXPAND "AllInvariants" -21) (("2" (EXPAND "occRS") (("2" (SIMP) (("2" (INST? -30) (("2" (INST?) (("2" (INST?) (("2" (EXPAND "enabled") (("2" (SIMP) (("2" (EXPAND "occTailROBfull") (("2" (SIMP) NIL))))))))))))))))))))))))))))))) ("2" (SIMP) (("2" (INST?) (("2" (INST?) (("2" (EXPAND "enabled") (("2" (CASE "Sn!1 = 0") (("1" (SIMP) NIL) ("2" (SIMP) (("2" (CASE "p(RS!1(iex!1(x!1))) = tail(ROB!1)") (("1" (EXPAND "AllInvariants" -29) (("1" (EXPAND "occRS") (("1" (SIMP) (("1" (HIDE 3) (("1" (INST? -37) (("1" (EXPAND " occTailROBfull") (("1" (SIMP) (("1" (SIMP) NIL))))))))))))))) ("2" (SIMP) (("2" (EXPAND "issuedBefore") (("2" (EXPAND "bufferIndex") (("2" (PROPAX) NIL))))))))))))))))))))))))))))) ("2" (SIMP) NIL))))))) ("3" (PROPAX) NIL) ("4" (EXPAND "enabled") (("4" (REPLACE -3) (("4" (APPLY-EXTENSIONALITY 1 :HIDE? T) NIL))))))))))))))))) ("2" (SIMP) (("2" (LEMMA "AllInvariants_writeb") (("2" (INST? -) (("2" (SIMP) (("2" (CASE "not rho_retire(pcI!1, RF!1, RSW!1, RATI!1, ROBW!1, numinst!1, pc_p!1, RF_p!1, RS_p!1, RAT_p!1, ROB_p!1, numinst_p!1)") (("1" (HIDE 3) (("1" (EXPAND "rho_retire") (("1" (INST 1 "retire!1") (("1" (EXPAND "can_retire") (("1" (CASE "not retire!1") (("1" (SIMP) (("1" (SPLIT +) (("1" (REP-PLUS) NIL) ("2" (REPLACE -18 +) (("2" (REPLACE -3 +) (("2" (REPLACE -8 +) (("2" (SIMP) (("2" (SPLIT +) (("1" (SPLIT-IF-SIMP) NIL) ("2" (SPLIT-IF-SIMP) NIL) ("3" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("1" (CASE "(Sn!1 > 0 AND x!1 = tail(ROB!1))") (("1" (SIMP) (("1" (LIFT-IF 1) (("1" (SPLIT +) (("1" (SIMP) (("1" (SKOSIMP*) (("1" (HIDE 1) (("1" (CLEAN-UP) (("1" (INSTBEST) (("1" (EXPAND "enabled") (("1" (EXPAND "dispatch") (("1" (CASE "not exec!1(FU!1)") (("1" (REPLACE -19) (("1" (SIMP) NIL))) ("2" (SIMP) (("2" (EXPAND "AllInvariants" -29) (("2" (EXPAND "occTailROBfull") (("2" (EXPAND "occRS") (("2" (FLATTEN) (("2" (INST -37 "iex!1(FU!1)") (("2" (SIMP) (("2" (REPLACE -22 (-3 -4)) (("2" (SIMP) NIL))))))))))))))))))))))))))))))))) ("2" (SIMP) (("2" (CLEAN-UP) (("2" (SPLIT 2) (("1" (SIMP) (("1" (EXPAND "occ_buffer") (("1" (SPLIT 2) (("1" (SIMP) NIL) ("2" (SIMP) NIL) ("3" (APPLY-EXTENSIONALITY 2 :HIDE? T) (("1" (CASE "b(RAT!1(src(prog(pc!1))(x!2)))") (("1" (SIMP) (("1" (LIFT-IF 1) (("1" (SPLIT +) (("1" (SIMP) (("1" (CASE "b(robe(ROB!1)(al(RAT!1(src(prog(pc!1))(x!2)))))") (("1" (SIMP) (("1" (LIFT-IF +) (("1" (SPLIT +) (("1" (SIMP) NIL) ("2" (SIMP) NIL))))))) ("2" (SIMP) (("2" (HIDE -20 -21 -22 -23 -24 -25) (("2" (EXPAND "enabled") (("2" (SKOSIMP*) (("2" (INSTBEST -) (("2" (REP-PLUS (-1 -2)) (("2" (REDUCE-IF) (("2" (EXPAND "AllInvariants" -21) (("2" (EXPAND "occRS") (("2" (SIMP) (("2" (INST? -32) (("2" (SIMP) NIL))))))))))))))))))))))))))) ("2" (SIMP) (("2" (SPLIT +) (("1" (SIMP) (("1" (LIFT-IF) (("1" (SPLIT +) (("1" (SIMP) NIL) ("2" (SIMP) NIL))))))) ("2" (SIMP) NIL))))))))))) ("2" (SIMP) NIL))) ("2" (SKOSIMP*) (("2" (LEMMA "chosenFUnonzero") (("2" (INST?) (("2" (SIMP) NIL))))))) ("3" (SKOSIMP*) (("3" (LEMMA "chosenFUnonzero") (("3" (INST?) (("3" (SIMP) NIL))))))))))))))) ("2" (SIMP) (("2" (HIDE 3) (("2" (EXPAND "occ_buffer" +) (("2" (EXPAND "dispatch") (("2" (HIDE 2) (("2" (EXPAND "succ" +) (("2" (SPLIT-IF-SIMP) (("2" (SPLIT-IF-SIMP) (("2" (EXPAND "AllInvariants" -23) (("2" (EXPAND "wrapWraps") (("2" (PROPAX) NIL))))))))))))))))))))))))))))))))) ("2" (CLEAN-UP) (("2" (REPLACE 1) (("2" (CASE " occ_buffer(x!1, ROB!1)") (("1" (SIMP) (("1" (LIFT-IF 2) (("1" (SPLIT 2) (("1" (SIMP) (("1" (LIFT-IF +) (("1" (APPLY (THEN (SPLIT +) (SIMP))) (("1" (SPLIT-IF-SIMP +) (("1" (APPLY-EXTENSIONALITY 1 :HIDE? T) NIL))) ("2" (SPLIT-IF-SIMP +) (("1" (APPLY-EXTENSIONALITY 1 :HIDE? T) NIL) ("2" (HIDE 2) (("2" (EXPAND "occ_buffer") (("2" (EXPAND "succ") (("2" (EXPAND "AllInvariants" -24) (("2" (EXPAND "wrapWraps") (("2" (EXPAND "dispatch") (("2" (SPLIT +) (("1" (SPLIT-IF-SIMP) (("1" (SPLIT-IF-SIMP -) NIL))) ("2" (SPLIT-IF-SIMP) (("1" (SPLIT-IF-SIMP -) NIL) ("2" (SPLIT-IF-SIMP -) NIL))) ("3" (PROPAX) NIL))))))))))))))))))))))) ("2" (SIMP) (("2" (LIFT-IF) (("2" (EXPAND "dispatch") (("2" (SPLIT-IF-SIMP) (("2" (SPLIT-IF-SIMP) (("2" (HIDE 1) (("2" (SPLIT-IF-SIMP) (("1" (SPLIT-IF-SIMP) NIL) ("2" (CASE "Sn!1 > 0") (("1" (HIDE 2) (("1" (EXPAND "AllInvariants" -22) (("1" (EXPAND "wrapWraps") (("1" (EXPAND "occ_buffer") (("1" (EXPAND "succ") (("1" (SPLIT-IF-SIMP) (("1" (SPLIT-IF-SIMP) (("1" (SPLIT-IF-SIMP -) NIL) ("2" (SPLIT -) (("1" (SIMP) NIL) ("2" (PROPAX) NIL))))) ("2" (REDUCE-IF) (("2" (SIMP) NIL))))))))))))))) ("2" (SIMP) NIL))))))))))))))))))))))) ("2" (SIMP) (("2" (HIDE -15 -16 -17 -18 -19) (("2" (EXPAND "dispatch") (("2" (SPLIT-IF-SIMP) (("2" (SPLIT-IF-SIMP) (("1" (SPLIT-IF-SIMP) (("1" (EXPAND "occ_buffer") (("1" (EXPAND "succ") (("1" (EXPAND "AllInvariants") (("1" (EXPAND "wrapWraps") (("1" (SPLIT-IF-SIMP) (("1" (SPLIT-IF-SIMP -) (("1" (SIMP) NIL))) ("2" (SPLIT-IF-SIMP -) (("2" (SPLIT-IF-SIMP -) (("2" (SPLIT -) (("1" (SIMP) NIL) ("2" (PROPAX) NIL))))))))))))))))))) ("2" (EXPAND "AllInvariants" -15) (("2" (EXPAND "wrapWraps") (("2" (SPLIT-IF-SIMP 2) (("2" (SPLIT-IF-SIMP) (("2" (EXPAND "occ_buffer") (("2" (EXPAND "succ") (("2" (SPLIT-IF-SIMP -) (("2" (SPLIT-IF-SIMP -) (("2" (SPLIT -) (("1" (SIMP) NIL) ("2" (PROPAX) NIL))))))))))))))))))))))))))))))))))))) ("2" (CLEAN-UP) (("2" (SKOSIMP*) (("2" (LEMMA "chosenFUnonzero") (("2" (INST?) (("2" (SIMP) (("2" (HIDE 1) (("2" (LEMMA "chosenFUnonzero") (("2" (INST? :WHERE -9) (("2" (HIDE -25 -26 -27 -28 -24) (("2" (LIFT-IF) (("2" (INST?) (("2" (SPLIT-IF-SIMP -7) (("2" (SPLIT-IF-SIMP -) NIL))))))))))))))))))))))))) ("3" (SKOSIMP*) (("3" (LEMMA "chosenFUnonzero") (("3" (INST?) (("3" (SIMP) NIL))))))) ("4" (SKOSIMP*) (("4" (LEMMA "chosenFUnonzero") (("4" (INST?) (("4" (SIMP) NIL))))))) ("5" (SKOSIMP*) (("5" (LEMMA "chosenFUnonzero") (("5" (INST?) (("5" (SIMP) NIL))))))) ("6" (SKOSIMP*) (("6" (LEMMA "chosenFUnonzero") (("6" (INST?) (("6" (SIMP) NIL))))))))))))))))))) ("3" (CLEAN-UP) (("3" (EXPAND "dispatch") (("3" (EXPAND "enabled") (("3" (REPLACE -19 +) (("3" (HIDE -15 -16 -17 -18 -19) (("3" (REPLACE -4 + :HIDE? T) (("3" (LEMMA "chosenFUnonzero") (("3" (HIDE -4) (("3" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("1" (REPLACE -9 + :HIDE? T) (("1" (SIMP) (("1" (HIDE -6 -7 -8) (("1" (SPLIT-IF-SIMP) (("1" (SPLIT-IF-SIMP) (("1" (SPLIT-IF-SIMP) (("1" (SKOSIMP*) (("1" (INST? +) (("1" (SIMP) (("1" (REP-PLUS 1) (("1" (SPLIT-IF-SIMP) (("1" (REP-PLUS -1) NIL))))))))))))) ("2" (HIDE 1) (("2" (SKOSIMP*) (("2" (HIDE -2) (("2" (REVEAL -1) (("2" (REP-PLUS -1) (("2" (REDUCE-IF) (("2" (INST?) (("2" (INST?) (("2" (INST?) (("2" (SIMP) NIL))))))))))))))))))))) ("2" (SPLIT-IF-SIMP) (("1" (SPLIT-IF-SIMP) (("1" (SPLIT-IF-SIMP) (("1" (SKOSIMP*) (("1" (REPLACE -13 (-4 -5)) (("1" (SIMP) (("1" (INST -12 "FU!2") (("1" (REDUCE-IF) (("1" (SIMP) (("1" (EXPAND "AllInvariants") (("1" (EXPAND "occRS") (("1" (EXPAND "occTailROBfull") (("1" (SIMP) (("1" (INST -70 "(iex!1(FU!2))") (("1" (SIMP) (("1" (SIMP) NIL))))))))))))))))))))))))) ("2" (SKOSIMP*) (("2" (INST?) (("2" (SIMP) (("2" (REP-PLUS (-1 -2)) (("2" (REDUCE-IF) (("2" (INST? -11) (("2" (SIMP) (("2" (EXPAND "AllInvariants" -17) (("2" (EXPAND "slotUnique") (("2" (FLATTEN) (("2" (INST -26 "x!1" "iex!1(FU!1)") (("2" (SIMP) (("2" (APPLY-EXTENSIONALITY 2 :HIDE? T) NIL))))))))))))))))))))))))))) ("2" (HIDE -2) (("2" (HIDE -2) (("2" (CASE "Sn!1 > 0") (("1" (HIDE 2) (("1" (SKOSIMP*) (("1" (INSTBEST -) (("1" (EXPAND "AllInvariants" -11) (("1" (EXPAND "occTailROBfull") (("1" (EXPAND "occRS") (("1" (REP-PLUS (-2 -3)) (("1" (REDUCE-IF) (("1" (SIMP) (("1" (INST -22 "iex!1(FU!1)") (("1" (SIMP) (("1" (SIMP) NIL))))))))))))))))))))))) ("2" (SIMP) (("2" (CLEAN-UP) (("2" (SPLIT-IF-SIMP) (("2" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("2" (APPLY (THEN (SKOSIMP*) (LEMMA "chosenFUnonzero") (INST? -) (SIMP))) NIL))))))))))))))))) ("2" (HIDE -1) (("2" (SPLIT-IF-SIMP) (("1" (SPLIT-IF-SIMP) (("1" (SKOSIMP*) (("1" (INST?) (("1" (INST?) (("1" (SIMP) (("1" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("1" (SPLIT-IF-SIMP) (("1" (SPLIT-IF-SIMP) (("1" (SPLIT-IF-SIMP) NIL) ("2" (SPLIT-IF-SIMP) (("2" (SKOSIMP*) (("2" (INST -12 "FU!2") (("2" (REP-PLUS (-1 -2)) (("2" (REDUCE-IF) (("2" (SIMP) (("2" (EXPAND "AllInvariants" -18) (("2" (EXPAND "occRS") (("2" (SIMP) (("2" (INST -26 "iex!1(FU!2)") (("2" (SIMP) NIL))))))))))))))))))))))))) ("2" (APPLY (THEN (SKOSIMP*) (LEMMA "chosenFUnonzero") (INST? -) (SIMP))) NIL) ("3" (APPLY (THEN (SKOSIMP*) (LEMMA "chosenFUnonzero") (INST? -) (SIMP))) NIL))))))))))) ("2" (SKOSIMP*) (("2" (INST?) (("2" (INST?) (("2" (SIMP) (("2" (EXPAND "AllInvariants" -11) (("2" (EXPAND "slotUnique") (("2" (INST?) (("2" (SIMP) (("2" (INST? :WHERE 4) (("2" (SIMP) (("2" (REP-PLUS (-1 -2)) (("2" (REDUCE-IF) (("2" (SIMP) (("2" (SIMP) (("2" (APPLY-EXTENSIONALITY 2 :HIDE? T) NIL))))))))))))))))))))))))))))))) ("2" (SPLIT-IF-SIMP) (("1" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("1" (SPLIT-IF-SIMP) (("1" (SPLIT-IF-SIMP) (("1" (SPLIT-IF-SIMP) NIL) ("2" (SPLIT-IF-SIMP) (("2" (SKOSIMP*) (("2" (INST? -) (("2" (REP-PLUS (-1 -2)) (("2" (REDUCE-IF) (("2" (SIMP) (("2" (EXPAND "AllInvariants") (("2" (EXPAND "occRS") (("2" (SIMP) (("2" (INST? -68) (("2" (SIMP) NIL))))))))))))))))))))))))) ("2" (APPLY (THEN (SKOSIMP*) (LEMMA "chosenFUnonzero") (INST? -) (SIMP))) NIL) ("3" (APPLY (THEN (SKOSIMP*) (LEMMA "chosenFUnonzero") (INST? -) (SIMP))) NIL))) ("2" (SPLIT-IF-SIMP) (("2" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("2" (APPLY (THEN (SKOSIMP*) (LEMMA "chosenFUnonzero") (INST? -) (SIMP))) NIL))))))))))))))))))))) ("2" (APPLY (THEN (SKOSIMP*) (INST? -) (SIMP))) NIL) ("3" (APPLY (THEN (SKOSIMP*) (INST? -) (SIMP))) NIL) ("4" (APPLY (THEN (SKOSIMP*) (INST? -) (SIMP))) NIL))))))))))))))))))))))) ("2" (SIMP) (("2" (CASE "(exists FU : a(res!1(FU)) and p(res!1(FU)) = head(ROB!1))") (("1" (HIDE 1 -17 -18 -19 -20 -21) (("1" (SKOSIMP*) (("1" (INST? -15) (("1" (EXPAND "enabled") (("1" (REP-PLUS (-1 -2)) (("1" (REDUCE-IF) (("1" (EXPAND "AllInvariants" -19) (("1" (EXPAND "occRS") (("1" (SIMP) (("1" (INST? -30) (("1" (SIMP) NIL))))))))))))))))))))) ("2" (CASE "int(robe(ROBW!1)(head(ROBW!1)))") (("1" (HIDE 2) (("1" (REPLACE -5 (-1) :HIDE? T) (("1" (HIDE -16 -17 -18 -19 -20) (("1" (SIMP) (("1" (REPLACE -9 (-1) :HIDE? T) (("1" (SIMP) (("1" (REDUCE-IF) NIL))))))))))))) ("2" (SIMP) (("2" (SPLIT-IF-SIMP) (("1" (EXPAND "dispatch") (("1" (EXPAND "enabled") (("1" (CASE "not (occ_buffer(head(ROBW!1), ROBW!1) AND NOT b(robe(ROBW!1)(head(ROBW!1))))") (("1" (HIDE 3) (("1" (REPLACE -4 (1) :HIDE? T) (("1" (SIMP) (("1" (EXPAND "occ_buffer") (("1" (REPLACE -8 + :HIDE? T) (("1" (SIMP) (("1" (EXPAND "succ") (("1" (SPLIT-IF-SIMP) (("1" (SPLIT-IF-SIMP) (("1" (SPLIT-IF-SIMP -) (("1" (REDUCE-IF) (("1" (SIMP) NIL))))))))))))))))))))))) ("2" (SIMP) (("2" (SPLIT 3) (("1" (REP-PLUS 1) NIL) ("2" (REPLACE -18 +) (("2" (REPLACE -5 (1) :HIDE? T) (("2" (SIMP) (("2" (REP-PLUS 1) (("2" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("2" (SPLIT-IF-SIMP) (("2" (SPLIT-IF-SIMP) (("2" (EXPAND "occ_buffer") (("2" (PROPAX) NIL))))))))))))))))) ("3" (REPLACE -19 + :HIDE? T) (("3" (REPLACE -5 (1) :HIDE? T) (("3" (SIMP) (("3" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("1" (REPLACE -9 +) (("1" (SIMP) (("1" (SPLIT-IF-SIMP) (("1" (SPLIT-IF-SIMP) (("1" (SPLIT-IF-SIMP) NIL) ("2" (SPLIT-IF-SIMP) (("2" (SPLIT-IF-SIMP 2) (("1" (SPLIT-IF-SIMP) (("1" (EXPAND "occ_buffer") (("1" (PROPAX) NIL))))) ("2" (SPLIT-IF-SIMP) (("2" (EXPAND "occ_buffer") (("2" (PROPAX) NIL))))))))))) ("2" (EXPAND "occ_buffer" -) (("2" (SPLIT-IF-SIMP) (("2" (SPLIT-IF-SIMP) (("2" (SPLIT-IF-SIMP) (("2" (SPLIT-IF-SIMP 2) NIL))))))))))))))) ("2" (APPLY (THEN (SKOSIMP*) (LEMMA "chosenFUnonzero") (INST? -) (SIMP))) NIL))))))))) ("4" (REPLACE -20 + :HIDE? T) (("4" (HIDE -16 -17 -18 -19 -20) (("4" (REPLACE -5 (1) :HIDE? T) (("4" (SIMP) (("4" (SPLIT +) (("1" (REP-PLUS 1) NIL) ("2" (REP-PLUS 1) (("2" (SPLIT-IF-SIMP) NIL))) ("3" (REP-PLUS 1) (("3" (SPLIT-IF-SIMP) (("3" (CASE "wrap(ROB!1)") (("1" (SIMP) (("1" (CASE "succ(head(ROB!1)) = 1") (("1" (SIMP) (("1" (EXPAND "succ") (("1" (SPLIT-IF-SIMP -) NIL))))) ("2" (SIMP) NIL))))) ("2" (SIMP) (("2" (EXPAND "succ") (("2" (SPLIT-IF-SIMP) (("2" (SPLIT-IF-SIMP -) (("2" (EXPAND "occ_buffer") (("2" (PROPAX) NIL))))))))))))))))) ("4" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("1" (CASE "Sn!1 = 0") (("1" (SIMP) (("1" (REPLACE -10) (("1" (SPLIT-IF-SIMP) (("1" (SPLIT-IF-SIMP) (("1" (SKOSIMP*) (("1" (INST? +) (("1" (SIMP) NIL))))) ("2" (APPLY-EXTENSIONALITY 2 :HIDE? T) (("1" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("1" (SPLIT-IF-SIMP) (("1" (EXPAND "AllInvariants" -20) (("1" (EXPAND "busyOperandsNearest") (("1" (SIMP) (("1" (INST? -33) (("1" (EXPAND "preceed") (("1" (EXPAND "occEqual") (("1" (FLATTEN) (("1" (INST? -24) (("1" (SIMP) NIL))))))))))))))))))) ("2" (APPLY (THEN (SKOSIMP*) (LEMMA "chosenFUnonzero") (INST? -) (SIMP))) NIL))) ("2" (APPLY (THEN (SKOSIMP*) (LEMMA "chosenFUnonzero") (INST? -) (SIMP))) NIL))))) ("2" (SPLIT-IF-SIMP) (("1" (CASE "not occ_buffer(x!1, ROB!1)") (("1" (HIDE 2) (("1" (EXPAND "occ_buffer") (("1" (PROPAX) NIL))))) ("2" (SIMP) (("2" (HIDE -2) (("2" (SPLIT-IF-SIMP) (("1" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("1" (SPLIT-IF-SIMP) (("1" (APPLY-EXTENSIONALITY 2 :HIDE? T) NIL))))) ("2" (APPLY-EXTENSIONALITY 2 :HIDE? T) (("1" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("1" (SPLIT-IF-SIMP) (("1" (SPLIT-IF-SIMP) (("1" (EXPAND "AllInvariants") (("1" (EXPAND " busyOperandsNearest") (("1" (SIMP) (("1" (INST? -78) (("1" (SIMP) (("1" (EXPAND "occEqual") (("1" (FLATTEN) (("1" (INST? -71) (("1" (SIMP) NIL))))))))))))))))))) ("2" (SPLIT-IF-SIMP) (("2" (APPLY-EXTENSIONALITY 2 :HIDE? T) NIL))))) ("2" (APPLY (THEN (SKOSIMP*) (LEMMA "chosenFUnonzero") (INST? -) (SIMP))) NIL) ("3" (APPLY (THEN (SKOSIMP*) (LEMMA "chosenFUnonzero") (INST? -) (SIMP))) NIL))) ("2" (APPLY (THEN (SKOSIMP*) (LEMMA "chosenFUnonzero") (INST? -) (SIMP))) NIL) ("3" (APPLY (THEN (SKOSIMP*) (LEMMA "chosenFUnonzero") (INST? -) (SIMP))) NIL))))))))))) ("2" (CASE "occ_buffer(x!1, ROB!1)") (("1" (EXPAND "occ_buffer") (("1" (PROPAX) NIL))) ("2" (HIDE 2) (("2" (SIMP) NIL))))))))))))) ("2" (SIMP) (("2" (SPLIT-IF-SIMP) (("1" (CASE "not occ_buffer(x!1, ROBI!1)") (("1" (HIDE 2) (("1" (REP-PLUS 1) (("1" (EXPAND "occ_buffer") (("1" (EXPAND "succ") (("1" (SPLIT-IF-SIMP) (("1" (SPLIT-IF-SIMP) NIL))))))))))) ("2" (SIMP) (("2" (CASE " (EXISTS (FU: FU_ID[R, U, Z, B]): a(res!1(FU)) AND p(res!1(FU)) = x!1)") (("1" (HIDE 1) (("1" (SKOSIMP*) (("1" (INST? -) (("1" (EXPAND "AllInvariants" -20) (("1" (EXPAND "occTailROBfull") (("1" (EXPAND "occRS") (("1" (REP-PLUS (-1 -2)) (("1" (REDUCE-IF) (("1" (INST? -28) (("1" (SIMP) (("1" (SIMP) (("1" (SIMP) NIL))))))))))))))))))))))) ("2" (REPLACE 1) (("2" (SPLIT-IF-SIMP) (("1" (REP-PLUS (-1)) (("1" (EXPAND "occ_buffer") (("1" (PROPAX) NIL))))) ("2" (SPLIT-IF-SIMP) (("1" (HIDE -1) (("1" (REPLACE -11 (1)) (("1" (SIMP) (("1" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("1" (SPLIT-IF-SIMP) (("1" (SPLIT-IF-SIMP) (("1" (SPLIT-IF-SIMP) NIL) ("2" (SPLIT-IF-SIMP) (("2" (SPLIT-IF-SIMP) (("2" (SKOSIMP*) (("2" (EXPAND "AllInvariants" -21) (("2" (EXPAND "occRS") (("2" (REP-PLUS (-1 -2)) (("2" (INST? -) (("2" (REDUCE-IF) (("2" (INST? -29) (("2" (SIMP) NIL))))))))))))))))))))))) ("2" (APPLY (THEN (SKOSIMP*) (LEMMA "chosenFUnonzero") (INST? -) (SIMP))) NIL) ("3" (APPLY (THEN (SKOSIMP*) (LEMMA "chosenFUnonzero") (INST? -) (SIMP))) NIL))))))))) ("2" (EXPAND "occ_buffer") (("2" (PROPAX) NIL))))))))))))))) ("2" (SPLIT-IF-SIMP) (("1" (CASE "not (occ_buffer(x!1, ROBI!1) AND x!1 = head(ROB!1))") (("1" (HIDE 2) (("1" (REP-PLUS 1) (("1" (EXPAND "occ_buffer") (("1" (SPLIT-IF-SIMP) NIL))))))) ("2" (SIMP) (("2" (SPLIT-IF-SIMP) (("1" (SKOSIMP*) (("1" (INST? +) (("1" (SIMP) NIL))))) ("2" (REPLACE -12 (2)) (("2" (SIMP) (("2" (APPLY-EXTENSIONALITY 2 :HIDE? T) (("1" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("1" (SPLIT-IF-SIMP) (("1" (EXPAND "AllInvariants" -21) (("1" (EXPAND "busyOperandsNearest") (("1" (SIMP) (("1" (INST? -34) (("1" (EXPAND "preceed") (("1" (EXPAND "occEqual") (("1" (FLATTEN) (("1" (INST? -25) (("1" (SIMP) NIL))))))))))))))))))) ("2" (APPLY (THEN (SKOSIMP*) (LEMMA "chosenFUnonzero") (INST? -) (SIMP))) NIL))) ("2" (APPLY (THEN (SKOSIMP*) (LEMMA "chosenFUnonzero") (INST? -) (SIMP))) NIL))))))))))))) ("2" (SPLIT-IF-SIMP) (("1" (CASE "not (occ_buffer(x!1, ROBI!1) and not (x!1 = head(ROB!1)) and occ_buffer(x!1, ROB!1))") (("1" (HIDE 2) (("1" (EXPAND "occ_buffer") (("1" (REP-PLUS (1 2 -1)) (("1" (EXPAND "succ") (("1" (SPLIT-IF-SIMP) (("1" (SPLIT-IF-SIMP -) (("1" (SIMP) NIL))) ("2" (SPLIT-IF-SIMP -) NIL))))))))))) ("2" (SIMP) (("2" (SPLIT-IF-SIMP) (("1" (SPLIT-IF-SIMP) (("1" (REPLACE -14 1) (("1" (SIMP) (("1" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("1" (SPLIT-IF-SIMP) (("1" (APPLY-EXTENSIONALITY 2 :HIDE? T) NIL))))))))))) ("2" (SPLIT-IF-SIMP) (("2" (REPLACE -12 (2)) (("2" (SIMP) (("2" (APPLY-EXTENSIONALITY 2 :HIDE? T) (("1" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("1" (SPLIT-IF-SIMP) (("1" (SPLIT-IF-SIMP) (("1" (SKOSIMP*) (("1" (INST?) (("1" (EXPAND "AllInvariants" -23) (("1" (EXPAND "occRS") (("1" (REPLACE -21 (-2 -3)) (("1" (SIMP) (("1" (REDUCE-IF) (("1" (INST? -31) (("1" (SIMP) (("1" (INST? -20) (("1" (SIMP) NIL))))))))))))))))))))))) ("2" (SPLIT-IF-SIMP) (("2" (APPLY-EXTENSIONALITY 2 :HIDE? T) NIL))))) ("2" (APPLY (THEN (SKOSIMP*) (LEMMA "chosenFUnonzero") (INST? -) (SIMP))) NIL) ("3" (APPLY (THEN (SKOSIMP*) (LEMMA "chosenFUnonzero") (INST? -) (SIMP))) NIL))) ("2" (APPLY (THEN (SKOSIMP*) (LEMMA "chosenFUnonzero") (INST? -) (SIMP))) NIL) ("3" (APPLY (THEN (SKOSIMP*) (LEMMA "chosenFUnonzero") (INST? -) (SIMP))) NIL))))))))))))))) ("2" (CASE "occ_buffer(x!1, ROBI!1)") (("1" (HIDE 2) (("1" (EXPAND "occ_buffer") (("1" (PROPAX) NIL))))) ("2" (HIDE 2) (("2" (SIMP) (("2" (CASE "occ_buffer(x!1, ROB!1)") (("1" (HIDE 2) (("1" (REP-PLUS 1) (("1" (EXPAND "occ_buffer") (("1" (EXPAND "succ") (("1" (SPLIT-IF-SIMP) (("1" (SPLIT-IF-SIMP) (("1" (SPLIT-IF-SIMP -) NIL) ("2" (SPLIT -) (("1" (SIMP) NIL) ("2" (PROPAX) NIL))))) ("2" (REDUCE-IF) (("2" (SIMP) NIL))))))))))))) ("2" (SIMP) (("2" (REP-PLUS 3) NIL))))))))))))))))))))) ("2" (APPLY (THEN (SKOSIMP*) (LEMMA "chosenFUnonzero") (INST? -) (SIMP))) NIL) ("3" (APPLY (THEN (SKOSIMP*) (LEMMA "chosenFUnonzero") (INST? -) (SIMP))) NIL) ("4" (APPLY (THEN (SKOSIMP*) (LEMMA "chosenFUnonzero") (INST? -) (SIMP))) NIL) ("5" (APPLY (THEN (SKOSIMP*) (LEMMA "chosenFUnonzero") (INST? -) (SIMP))) NIL) ("6" (APPLY (THEN (SKOSIMP*) (LEMMA "chosenFUnonzero") (INST? -) (SIMP))) NIL) ("7" (APPLY (THEN (SKOSIMP*) (LEMMA "chosenFUnonzero") (INST? -) (SIMP))) NIL) ("8" (APPLY (THEN (SKOSIMP*) (LEMMA "chosenFUnonzero") (INST? -) (SIMP))) NIL) ("9" (APPLY (THEN (SKOSIMP*) (LEMMA "chosenFUnonzero") (INST? -) (SIMP))) NIL) ("10" (APPLY (THEN (SKOSIMP*) (LEMMA "chosenFUnonzero") (INST? -) (SIMP))) NIL) ("11" (APPLY (THEN (SKOSIMP*) (LEMMA "chosenFUnonzero") (INST? -) (SIMP))) NIL) ("12" (APPLY (THEN (SKOSIMP*) (LEMMA "chosenFUnonzero") (INST? -) (SIMP))) NIL) ("13" (APPLY (THEN (SKOSIMP*) (LEMMA "chosenFUnonzero") (INST? -) (SIMP))) NIL))))))))))))) ("5" (REPLACE -21 + :HIDE? T) (("5" (HIDE -16 -17 -18 -19 -20) (("5" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("1" (REPLACE -6 + :HIDE? T) (("1" (SIMP) (("1" (SPLIT-IF-SIMP) (("1" (CASE "not (EXISTS (FU: FU_ID[R, U, Z, B]): a(res!1(FU)) AND p(res!1(FU)) = p(RSI!1(x!1)))") (("1" (HIDE 2) (("1" (SKOSIMP*) (("1" (INST? +) (("1" (REPLACE -13 +) (("1" (SIMP) (("1" (REPLACE -16 (1 -1)) (("1" (SIMP) (("1" (INST? -) (("1" (REDUCE-IF) (("1" (SIMP) (("1" (SPLIT-IF-SIMP) NIL))))))))))))))))))))) ("2" (SIMP) (("2" (SPLIT-IF-SIMP) (("2" (REP-PLUS 1) (("2" (SPLIT-IF-SIMP) (("2" (HIDE 1) (("2" (SKOSIMP*) (("2" (INST -20 "FU!3") (("2" (REPLACE -21 (-6)) (("2" (SIMP) NIL))))))))))))))))))) ("2" (SPLIT-IF-SIMP) (("1" (SKOSIMP*) (("1" (INST? +) (("1" (INST? -) (("1" (REP-PLUS (-1 -2 2)) (("1" (REDUCE-IF) (("1" (SIMP) (("1" (SPLIT-IF-SIMP) (("1" (HIDE 1) (("1" (EXPAND "AllInvariants" -22) (("1" (EXPAND "occTailROBfull") (("1" (EXPAND "occRS") (("1" (FLATTEN) (("1" (INST? -30) (("1" (SIMP) (("1" (SIMP) NIL))))))))))))))) ("2" (EXPAND "AllInvariants" -21) (("2" (EXPAND "slotUnique") (("2" (FLATTEN) (("2" (INST -30 "iex!1(FU!1)" "x!1") (("2" (SIMP) (("2" (REP-PLUS 2) (("2" (APPLY-EXTENSIONALITY 2 :HIDE? T) NIL))))))))))))))))))))))))))) ("2" (CASE "x!1 = Sn!1") (("1" (SIMP) (("1" (REPLACE -12 +) (("1" (SIMP) (("1" (APPLY-EXTENSIONALITY 2 :HIDE? T) (("1" (SPLIT-IF-SIMP) (("1" (SPLIT-IF-SIMP) (("1" (SPLIT-IF-SIMP) (("1" (REPLACE -8 (-1)) (("1" (SIMP) (("1" (REP-PLUS -1) NIL))))))) ("2" (SPLIT 2) (("1" (SIMP) (("1" (REP-PLUS 1) NIL))) ("2" (SIMP) (("2" (APPLY (THEN (SPLIT +) (SIMP))) (("2" (SPLIT-IF-SIMP) (("1" (SPLIT-IF-SIMP) NIL) ("2" (SKOSIMP*) (("2" (INSTBEST -) (("2" (EXPAND "AllInvariants" -20) (("2" (EXPAND "occRS") (("2" (REP-PLUS (-1 -2)) (("2" (INST? -28) (("2" (REDUCE-IF) (("2" (SIMP) NIL))))))))))))))))))))))))))) ("2" (APPLY (THEN (SKOSIMP*) (LEMMA "chosenFUnonzero") (INST? -) (SIMP))) NIL) ("3" (APPLY (THEN (SKOSIMP*) (LEMMA "chosenFUnonzero") (INST? -) (SIMP))) NIL))))))))) ("2" (SIMP) (("2" (SPLIT-IF-SIMP) (("1" (SPLIT-IF-SIMP) (("1" (REPLACE -13 +) (("1" (SIMP) (("1" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("1" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("1" (REPLACE -7 (1) :HIDE? T) (("1" (SIMP) (("1" (REPLACE -10 + :HIDE? T) (("1" (SIMP) (("1" (SPLIT-IF-SIMP) (("1" (SPLIT-IF-SIMP) (("1" (EXPAND "AllInvariants" -19) (("1" (EXPAND "occEqual") (("1" (EXPAND "busyOperandsNearest") (("1" (EXPAND "preceed") (("1" (SIMP) (("1" (EXPAND "RS_ROB_opsEqual") (("1" (INST? -30) (("1" (INST? -33) (("1" (SIMP) (("1" (EXPAND "occRS") (("1" (INST? -28) (("1" (SIMP) NIL))))))))))))))))))))))))) ("2" (SPLIT-IF-SIMP) (("2" (APPLY-EXTENSIONALITY 2 :HIDE? T) NIL))))))))))))) ("2" (APPLY (THEN (SKOSIMP*) (LEMMA "chosenFUnonzero") (INST? -) (SIMP))) NIL) ("3" (APPLY (THEN (SKOSIMP*) (LEMMA "chosenFUnonzero") (INST? -) (SIMP))) NIL))) ("2" (APPLY (THEN (SKOSIMP*) (LEMMA "chosenFUnonzero") (INST? -) (SIMP))) NIL) ("3" (APPLY (THEN (SKOSIMP*) (LEMMA "chosenFUnonzero") (INST? -) (SIMP))) NIL))))))) ("2" (REP-PLUS -1) NIL))) ("2" (REP-PLUS (1 2)) NIL))))))))))))))) ("2" (APPLY (THEN (SKOSIMP*) (LEMMA "chosenFUnonzero") (INST? -) (SIMP))) NIL) ("3" (APPLY (THEN (SKOSIMP*) (LEMMA "chosenFUnonzero") (INST? -) (SIMP))) NIL))))))))))))))))) ("2" (HIDE 1) (("2" (HIDE -18 -19 -20 -21 -22) (("2" (REPLACE -6 (-1 -2) :HIDE? T) (("2" (SIMP) (("2" (REPLACE -10 (-1 -2) :HIDE? T) (("2" (SIMP) (("2" (SPLIT-IF-SIMP -) (("1" (SPLIT-IF-SIMP -) NIL) ("2" (SPLIT-IF-SIMP -) (("1" (REDUCE-IF) NIL) ("2" (SPLIT-IF-SIMP -) (("2" (EXPAND "dispatch") (("2" (SIMP) (("2" (EXPAND "occ_buffer") (("2" (PROPAX) NIL))))))))))))))))))))))))))))))))))))))))))))) ("2" (SIMP) (("2" (LEMMA "AllInvariants_retire") (("2" (INST?) (("2" (SIMP) NIL))))))))))))))))))))))) ("3" (SKOSIMP*) (("3" (LEMMA "chosenFUnonzero") (("3" (INST? -) (("3" (SIMP) NIL))))))) ("4" (SKOSIMP*) (("4" (LEMMA "chosenFUnonzero") (("4" (INST? -) (("4" (SIMP) NIL))))))))) ("3" (SKOSIMP*) (("3" (LEMMA "chosenFUnonzero") (("3" (INST? -) (("3" (SIMP) NIL)))))))))))))))))))))))))))))))))))))))))))) $$$live.pvs live[R, U, Z: posnat, (IMPORTING more_nat_types[1]) B: greater_one_nat]: THEORY % In every situation the speculative system, DES, can either issue, write-back (execute), % or retire an instruction. This is noted by showing that the retirement buffer has % been modified, implying that progress of some type has been made. BEGIN IMPORTING Invs3[R, U, Z, B] RF, RF_p: VAR [REG_ID -> RF_TYPE] RAT, RAT_p: VAR [REG_ID -> RAT_TYPE] ROB, ROB_p: VAR ROB_TYPE RS, RS_p: VAR [SLOT_ID -> RS_TYPE] res, res_p: VAR [FU_ID -> result_TYPE] pc, pc_p: VAR posnat numinst, numinst_p: VAR nat FU: VAR FU_ID S, S2: VAR SLOT_ID r: VAR REG_ID rb, rb2: VAR ROB_ID canRetire: LEMMA occ_buffer(head(ROB), ROB) AND NOT b(robe(ROB)(head(ROB))) AND AllInvariants(RF, RS, RAT, ROB, numinst, pc) IMPLIES (EXISTS RF_p, RS_p, RAT_p, ROB_p, numinst_p, pc_p: rho_retire(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p) AND NOT occ_buffer(head(ROB), ROB_p)) canWriteb: LEMMA occ_buffer(head(ROB), ROB) AND b(robe(ROB)(head(ROB))) AND AllInvariants(RF, RS, RAT, ROB, numinst, pc) IMPLIES (EXISTS RF_p, RS_p, RAT_p, ROB_p, numinst_p, pc_p, res: rho_writeb(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p, res) AND NOT b(robe(ROB_p)(head(ROB_p)))) canIssue: LEMMA NOT occ_buffer(head(ROB), ROB) AND AllInvariants(RF, RS, RAT, ROB, numinst, pc) IMPLIES (EXISTS RF_p, RS_p, RAT_p, ROB_p, numinst_p, pc_p: rho_issue(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p) AND occ_buffer(head(ROB_p), ROB_p)) canProgress: LEMMA AllInvariants(RF, RS, RAT, ROB, numinst, pc) IMPLIES (EXISTS RF_p, RS_p, RAT_p, ROB_p, numinst_p, pc_p: (rho_issue(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p) or (exists res: rho_writeb(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p, res)) or rho_retire(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p)) and ROB_p /= ROB) END live $$$live.prf (|live| (|canRetire| "" (SKOSIMP*) (("" (EXPAND "rho_retire") (("" (EXPAND "can_retire") (("" (CASE "NOT (int(robe(ROB!1)(head(ROB!1))) OR (type_op(op(robe(ROB!1)(head(ROB!1)))) = BRANCH AND EXOR(br_pred(robe(ROB!1)(head(ROB!1))), v(robe(ROB!1)(head(ROB!1))) > 0)))") (("1" (INST 3 "(LAMBDA (r:REG_ID): IF r = t(robe(ROB!1)(head(ROB!1))) THEN (# v := v(robe(ROB!1)(head(ROB!1))) #) ELSE RF!1(r) ENDIF)" "(LAMBDA S: IF oc(RS!1(S)) THEN RS!1(S) WITH [ ss := (LAMBDA (j: TWO): (# st := IF p(ss(RS!1(S))(j)) = head(ROB!1) THEN RETIRED ELSE st(ss(RS!1(S))(j)) ENDIF, p := p(ss(RS!1(S))(j)), v := v(ss(RS!1(S))(j)), r := r(ss(RS!1(S))(j)) #)) ] ELSE RS!1(S) ENDIF)" "(LAMBDA (r:REG_ID): IF al(RAT!1(r)) = head(ROB!1) THEN (# b := FALSE, al := al(RAT!1(r)) #) ELSE RAT!1(r) ENDIF)" " (# head := succ(head(ROB!1)), tail := tail(ROB!1), wrap := wrap(ROB!1) AND NOT succ(head(ROB!1)) = 1, robe := (LAMBDA rb: IF rb = head(ROB!1) THEN robe(ROB!1)(rb) WITH [oc := FALSE] ELSIF occ_buffer(rb, ROB!1) THEN robe(ROB!1)(rb) WITH [ ss := (LAMBDA (j: TWO): (# st := IF p(ss(robe(ROB!1)(rb))(j)) = head(ROB!1) THEN RETIRED ELSE st(ss(robe(ROB!1)(rb))(j)) ENDIF, v := v(ss(robe(ROB!1)(rb))(j)), p := p(ss(robe(ROB!1)(rb))(j)), r := r(ss(robe(ROB!1)(rb))(j)) #)) ] ELSE robe(ROB!1)(rb) ENDIF ) #)" "numinst!1 + 1" "pc!1") (("1" (SIMP) (("1" (SPLIT 4) (("1" (INST 1 "true") (("1" (SPLIT +) (("1" (SIMP) NIL) ("2" (SIMP) NIL))))) ("2" (EXPAND "occ_buffer") (("2" (EXPAND "succ") (("2" (SPLIT-ALL) (("2" (EXPAND "AllInvariants") (("2" (EXPAND "wrapWraps") (("2" (PROPAX) NIL))))))))))))))))) ("2" (INST 2 "IF int(robe(ROB!1)(head(ROB!1))) THEN RF!1 ELSE (LAMBDA r: IF r = t(robe(ROB!1)(head(ROB!1))) THEN IF v(robe(ROB!1)(head(ROB!1))) > 0 THEN (# v := 1#) ELSE (# v := 0#) ENDIF ELSE RF!1(r) ENDIF) ENDIF" "(LAMBDA S: RS!1(S) with [oc := FALSE])" "(LAMBDA r: (# b:= FALSE, al := B #))" "(# tail := 1, head := 1, wrap := FALSE, robe := (LAMBDA rb: robe(ROB!1)(rb) WITH [ b := FALSE, oc := FALSE ]) #)" "numinst!1 + 1" "IF (int(robe(ROB!1)(head(ROB!1)))) THEN Int_interrupt_addr(pc(robe(ROB!1)(head(ROB!1))), type_op(op(robe(ROB!1)(head(ROB!1))))) ELSIF v(robe(ROB!1)(head(ROB!1))) > 0 THEN br_targ(robe(ROB!1)(head(ROB!1))) ELSE pc(robe(ROB!1)(head(ROB!1))) + 1 ENDIF") (("1" (SPLIT 2) (("1" (INST 1 "true") (("1" (SPLIT +) (("1" (SIMP) NIL) ("2" (SIMP) NIL) ("3" (SIMP) NIL))))) ("2" (EXPAND "occ_buffer") (("2" (PROPAX) NIL))))) ("2" (SIMP) NIL) ("3" (SIMP) NIL))))))))))) (|canWriteb| "" (SKOSIMP*) (("" (EXPAND "AllInvariants") (("" (EXPAND "occEqual") (("" (EXPAND "busyROBoccRS") (("" (SIMP) (("" (INST?) (("" (INST?) (("" (INST?) (("" (SIMP) (("" (SKOSIMP*) (("" (CASE "not (exists (FU : FU_ID) : fu_table(op(RS!1(S!1)))= FU)") (("1" (INST 1 "fu_table(op(RS!1(S!1)))") NIL) ("2" (SKOSIMP*) (("2" (INST 1 "RF!1" _ "RAT!1" _ "numinst!1" "pc!1" _) (("2" (INST 1 _ _ "(LAMBDA (FU: FU_ID): IF FU = FU!1 THEN (# a := TRUE, p := p(RS!1(S!1)), v := IF type_op(op(RS!1(S!1))) /= BRANCH THEN do_op(op(RS!1(S!1)), v(ss(RS!1(S!1))(1)), v(ss(RS!1(S!1))(2))) ELSIF branch_act(pc(robe(ROB!1)(p(RS!1(S!1)))), issuedBefore(numinst!1, ROB!1, p(RS!1(S!1))) +1) THEN 1 ELSE 0 ENDIF, int := int_interrupt(pc(robe(ROB!1)(p(RS!1(S!1)))), issuedBefore(numinst!1, ROB!1, p(RS!1(S!1))) +1) #) ELSE (# a:= false, p:= 1, v:= 0, int:= false #) ENDIF) ") (("2" (CASE "not (exists (v : VALUE) : v = IF type_op(op(RS!1(S!1))) /= BRANCH THEN do_op(op(RS!1(S!1)), v(ss(RS!1(S!1))(1)), v(ss(RS!1(S!1))(2))) ELSIF branch_act(pc(robe(ROB!1)(p(RS!1(S!1)))), issuedBefore(numinst!1, ROB!1, p(RS!1(S!1))) +1) THEN 1 ELSE 0 ENDIF)") (("1" (INST 1 "IF type_op(op(RS!1(S!1))) /= BRANCH THEN do_op(op(RS!1(S!1)), v(ss(RS!1(S!1))(1)), v(ss(RS!1(S!1))(2))) ELSIF branch_act(pc(robe(ROB!1)(p(RS!1(S!1)))), issuedBefore(numinst!1, ROB!1, p(RS!1(S!1))) + 1) THEN 1 ELSE 0 ENDIF") NIL) ("2" (SKOSIMP*) (("2" (INST 1 "(LAMBDA (S: SLOT_ID): IF S = S!1 THEN RS!1(S) with [oc := FALSE] ELSIF oc(RS!1(S)) THEN (# oc := oc(RS!1(S)), p := p(RS!1(S)), op := op(RS!1(S)), ss := (LAMBDA (j: TWO): IF st(ss(RS!1(S))(j)) = BUSY AND p(ss(RS!1(S))(j)) = head(ROB!1) AND p(ss(RS!1(S))(j)) > 0 THEN (# st := WRITE_B, p := p(ss(RS!1(S))(j)), v := v!1, r := r(ss(RS!1(S))(j)) #) ELSE ss(RS!1(S))(j) ENDIF) #) ELSE RS!1(S) ENDIF) " _) (("2" (INST 1 " (# head := head(ROB!1), tail := tail(ROB!1), wrap := wrap(ROB!1), robe := (LAMBDA (rb: ROB_ID): IF occ_buffer(rb, ROB!1) AND rb = head(ROB!1) THEN (# b := FALSE, v := v!1, int := int_interrupt(pc(robe(ROB!1)(p(RS!1(S!1)))), issuedBefore(numinst!1, ROB!1, p(RS!1(S!1))) +1), t := t(robe(ROB!1)(rb)), ss := ss(robe(ROB!1)(rb)), pc := pc(robe(ROB!1)(rb)), op := op(robe(ROB!1)(rb)), br_pred := br_pred(robe(ROB!1)(rb)), br_targ := br_targ(robe(ROB!1)(rb)), oc := oc(robe(ROB!1)(rb)) #) ELSIF occ_buffer(rb, ROB!1) THEN robe(ROB!1)(rb) WITH [ss := (LAMBDA (j: TWO): IF st(ss(robe(ROB!1)(rb))(j)) = BUSY AND p(ss(robe(ROB!1)(rb))(j)) = head(ROB!1) THEN (# st := WRITE_B, p := p(ss(robe(ROB!1)(rb))(j)), v := v!1, r := r(ss(robe(ROB!1)(rb))(j)) #) ELSE ss(robe(ROB!1)(rb))(j) ENDIF)] ELSE robe(ROB!1)(rb) ENDIF ) #) ") (("2" (EXPAND "rho_writeb") (("2" (INST 1 "(lambda (FU : FU_ID) : FU = FU!1)" "(lambda (FU : FU_ID) : S!1)") (("2" (EXPAND "can_execute") (("2" (EXPAND "enabled") (("2" (SIMP) (("2" (SPLIT +) (("1" (SKOSIMP*) (("1" (SIMP) (("1" (SKOSIMP*) (("1" (EXPAND "RS_ROB_opsEqual") (("1" (INST?) (("1" (EXPAND "busyOperandsNearest") (("1" (INST?) (("1" (SIMP) (("1" (EXPAND "preceed") (("1" (PROPAX) NIL))))))))))))))))))) ("2" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("2" (NEW-SPLIT-IF) NIL))) ("3" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("3" (CASE "x!1 = head(ROB!1)") (("1" (SIMP) (("1" (CASE "chooseFU(x!1, (LAMBDA (FU: FU_ID): IF FU = FU!1 THEN (# a := TRUE, p := p(RS!1(S!1)), v := IF type_op(op(RS!1(S!1))) /= BRANCH THEN do_op(op(RS!1(S!1)), v(ss(RS!1(S!1))(1)), v(ss(RS!1(S!1))(2))) ELSIF branch_act (pc(robe(ROB!1)(p(RS!1(S!1)))), 1 + issuedBefore(numinst!1, ROB!1, p(RS!1(S!1)))) THEN 1 ELSE 0 ENDIF, int := int_interrupt (pc(robe(ROB!1)(p(RS!1(S!1)))), 1 + issuedBefore(numinst!1, ROB!1, p(RS!1(S!1)))) #) ELSE (# a := FALSE, p := 1, v := 0, int := FALSE #) ENDIF)) = FU!1") (("1" (REPLACE -1) (("1" (LIFT-IF +) (("1" (SPLIT +) (("1" (SIMP) (("1" (NEW-SPLIT-IF) NIL))) ("2" (SIMP) (("2" (INST 1 "FU!1") (("2" (SIMP) NIL))))))))))) ("2" (HIDE 2) (("2" (EXPAND "chooseFU") (("2" (EXPAND "choose") (("2" (NEW-SPLIT-IF) (("1" (USE "epsilon_ax[FU_ID[R, U, Z, B]]") (("1" (SPLIT -) (("1" (SIMP) NIL) ("2" (INST 1 "FU!1") (("2" (SIMP) NIL))))))) ("2" (INST 1 "FU!1") (("2" (SIMP) NIL))))))))))))))) ("2" (SIMP) (("2" (NEW-SPLIT-IF) (("2" (NEW-SPLIT-IF) (("1" (SKOSIMP*) (("1" (REDUCE-ALL) NIL))) ("2" (APPLY-EXTENSIONALITY 2 :HIDE? T) (("2" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("2" (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF) (("1" (SKOSIMP*) (("1" (REDUCE-ALL) (("1" (APPLY (THEN (REPEAT* (THEN (SPLIT +) (SIMP))))) (("1" (EXPAND "chooseFU") (("1" (EXPAND "choose") (("1" (NEW-SPLIT-IF) (("1" (USE "epsilon_ax[FU_ID[R, U, Z, B]]") (("1" (SPLIT -) (("1" (SIMP) NIL) ("2" (INST 1 "FU!1") (("2" (SIMP) NIL))))))) ("2" (INST 1 "FU!1") (("2" (SIMP) NIL))))))))))))))) ("2" (INST 1 "FU!1") (("2" (SIMP) NIL))))) ("2" (NEW-SPLIT-IF) (("2" (SPLIT +) (("1" (SIMP) (("1" (HIDE 1) (("1" (EXPAND "chooseFU") (("1" (NEW-SPLIT-IF -) (("1" (SKOSIMP*) (("1" (REDUCE-ALL) NIL))))))))))) ("2" (SIMP) (("2" (SKOSIMP*) (("2" (REDUCE-ALL) NIL))))))))))))))))))))))))) ("4" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("4" (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF) (("1" (INST? +) (("1" (SIMP) NIL))))) ("2" (NEW-SPLIT-IF) (("1" (SKOSIMP*) (("1" (REDUCE-ALL) (("1" (EXPAND "slotUnique") (("1" (INST? :WHERE 2) (("1" (SIMP) (("1" (APPLY-EXTENSIONALITY 1 :HIDE? T) NIL))))))))))) ("2" (NEW-SPLIT-IF) (("2" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("2" (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF) (("1" (SPLIT +) (("1" (SIMP) (("1" (APPLY (THEN (REPEAT* (THEN (SPLIT +) (SIMP))))) NIL))) ("2" (SIMP) (("2" (EXPAND "chooseFU") (("2" (EXPAND "choose") (("2" (NEW-SPLIT-IF) (("1" (USE "epsilon_ax[FU_ID[R, U, Z, B]]") (("1" (SPLIT -) (("1" (SIMP) NIL) ("2" (INST 1 "FU!1") (("2" (SIMP) NIL))))))) ("2" (INST 1 "FU!1") (("2" (SIMP) NIL))))))))))))) ("2" (INSTBEST +) (("2" (SIMP) NIL))))) ("2" (NEW-SPLIT-IF) (("2" (SKOSIMP*) (("2" (REDUCE-ALL) NIL))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (|canIssue| "" (SKOSIMP*) (("" (INST 2 "RF!1" _ _ _ "numinst!1" _) (("" (INST 2 " (LAMBDA S: IF S /= Z THEN RS!1(S) ELSE (# oc := TRUE, p := tail(ROB!1), op := op(prog(pc!1)), ss := (LAMBDA (j: TWO): IF b(RAT!1(src(prog(pc!1))(j))) THEN (# st := IF b(robe(ROB!1)(al(RAT!1(src(prog(pc!1))(j))))) THEN BUSY ELSE WRITE_B ENDIF, p := al(RAT!1(src(prog(pc!1))(j))), v := v(robe(ROB!1)(al(RAT!1(src(prog(pc!1))(j))))), r := src(prog(pc!1))(j) #) ELSE (# st := RETIRED, v := v(RF!1(src(prog(pc!1))(j))), r := src(prog(pc!1))(j), p := al(RAT!1(src(prog(pc!1))(j))) #) ENDIF) #) ENDIF ) " _ _ _) (("" (INST 2 "(LAMBDA (r: REG_ID): IF Z > 0 AND r = t(prog(pc!1)) THEN (# b := TRUE , al := tail(ROB!1) #) ELSE RAT!1(r) ENDIF)" _ "IF type_op(op(prog(pc!1))) = BRANCH AND branch_pred(pc!1, totalIssued(numinst!1, ROB!1) + 1) THEN br_target(prog(pc!1)) ELSE 1 + pc!1 ENDIF") (("" (INST 2 " (# head := head(ROB!1), tail := succ(tail(ROB!1)), wrap := wrap(ROB!1) OR succ(tail(ROB!1)) = 1, robe := (LAMBDA rb: IF rb /= tail(ROB!1) THEN robe(ROB!1)(rb) ELSE (# b := TRUE, v := 0, op := op(prog(pc!1)), int := FALSE, oc := TRUE, br_pred := branch_pred(pc!1, totalIssued(numinst!1, ROB!1) + 1), br_targ := br_target(prog(pc!1)), t := t(prog(pc!1)), pc := pc!1, ss := (LAMBDA (j: TWO): IF b(RAT!1(src(prog(pc!1))(j))) THEN (# st := IF b(robe(ROB!1)(al(RAT!1(src(prog(pc!1))(j))))) THEN BUSY ELSE WRITE_B ENDIF, p := al(RAT!1(src(prog(pc!1))(j))), v := v(robe(ROB!1)(al(RAT!1(src(prog(pc!1))(j))))), r := src(prog(pc!1))(j) #) ELSE (# st := RETIRED, v := v(RF!1(src(prog(pc!1))(j))), r := src(prog(pc!1))(j), p := al(RAT!1(src(prog(pc!1))(j))) #) ENDIF) #) ENDIF) #)") (("" (EXPAND "rho_issue") (("" (SPLIT +) (("1" (INST 1 "Z") (("1" (EXPAND "can_issue") (("1" (EXPAND "dispatch") (("1" (SIMP) (("1" (EXPAND "AllInvariants") (("1" (EXPAND "occ_buffer" +) (("1" (NEW-SPLIT-IF) (("1" (EXPAND "occRS") (("1" (INST?) (("1" (EXPAND "occEqual") (("1" (SIMP) (("1" (INST?) (("1" (INST?) (("1" (EXPAND "occ_buffer") (("1" (PROPAX) NIL))))))))))))))))))))))))))))) ("2" (EXPAND "occ_buffer") (("2" (EXPAND "succ") (("2" (SPLIT-ALL) (("2" (EXPAND "AllInvariants") (("2" (EXPAND "wrapWraps") (("2" (PROPAX) NIL))))))))))))))))))))))))) (|canProgress| "" (SKOSIMP*) (("" (LEMMA "canIssue") (("" (INST? -) (("" (SIMP) (("" (CASE "NOT occ_buffer(head(ROB!1), ROB!1)") (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST? +) (("1" (SIMP) NIL))))))) ("2" (SIMP) (("2" (CLEAN-UP) (("2" (LEMMA "canWriteb") (("2" (INST?) (("2" (SIMP) (("2" (CASE "b(robe(ROB!1)(head(ROB!1)))") (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST 2 "RF_p!1" "RS_p!1" "RAT_p!1" "ROB_p!1" "numinst_p!1" "pc_p!1") (("1" (SIMP) (("1" (INST?) NIL))))))))) ("2" (SIMP) (("2" (LEMMA "canRetire") (("2" (INST?) (("2" (CLEAN-UP) (("2" (SIMP) (("2" (SKOSIMP*) (("2" (INST? +) (("2" (SIMP) NIL)))))))))))))))))))))))))))))))))))))) $$$seq.pvs seq[R: posnat]: THEORY % The sequential system. BEGIN IMPORTING more_nat_types, def[R] pc, pc_p: VAR PC_RANGE reg, reg_p: VAR [REG_ID[R] -> VALUE] delay: VAR bool numinst, numinst_p: VAR nat r: VAR REG_ID THETA(pc, reg, numinst): bool = (pc = 1 AND numinst = 0 AND (FORALL (r: REG_ID): reg(r) = 0)) rho(pc, reg, numinst, pc_p, reg_p, numinst_p): bool = (EXISTS delay: IF delay THEN numinst_p = numinst AND reg_p = reg AND pc_p = pc ELSIF int_interrupt(pc, numinst + 1) THEN pc_p = Int_interrupt_addr(pc, type_op(op(prog(pc)))) AND numinst_p = numinst + 1 AND reg_p = reg ELSIF type_op(op(prog(pc))) = BRANCH THEN IF branch_act(pc, numinst + 1) THEN pc_p = br_target(prog(pc)) ELSE pc_p = pc + 1 ENDIF AND numinst_p = numinst + 1 AND reg_p = (LAMBDA r: IF r = t(prog(pc)) THEN IF branch_act(pc, numinst + 1) THEN 1 ELSE 0 ENDIF ELSE reg(r) ENDIF) ELSE pc_p = pc + 1 AND numinst_p = numinst + 1 AND reg_p = (LAMBDA r: IF r = t(prog(pc)) THEN do_op (op(prog(pc)), reg(src(prog(pc))(1)), reg(src(prog(pc))(2))) ELSE reg(r) ENDIF) ENDIF) END seq $$$seq.prf (|seq| (|rho_TCC1| "" (SUBTYPE-TCC) NIL) (|rho_TCC2| "" (SUBTYPE-TCC) NIL) (|rho_TCC3| "" (SUBTYPE-TCC) NIL) (|rho_TCC4| "" (SUBTYPE-TCC) NIL)) $$$InvDefs3.pvs InvDefs3[R, U, Z: posnat, (IMPORTING more_nat_types[1]) B: greater_one_nat]: THEORY % The third of 3 files defining properties which are invariants of Spec BEGIN IMPORTING InvDefs2[R, U, Z, B] RF, RF_p: VAR [REG_ID -> RF_TYPE] RAT, RAT_p: VAR [REG_ID -> RAT_TYPE] ROB, ROB_p: VAR ROB_TYPE RS, RS_p: VAR [SLOT_ID -> RS_TYPE] res, res_p: VAR [FU_ID -> result_TYPE] pc, pc_p: VAR posnat numinst, numinst_p: VAR nat FU: VAR FU_ID S, S2: VAR SLOT_ID r: VAR REG_ID rb, rb2: VAR ROB_ID chosenFUunique(res): boolean = (FORALL FU: a(res(FU)) IMPLIES chooseFU(p(res(FU)), res) = FU) busyOpBusyROB(ROB): boolean = (FORALL rb, (j: TWO): oc(robe(ROB)(rb)) AND st(ss(robe(ROB)(rb))(j)) = BUSY IMPLIES b(robe(ROB)(rb))) numOcc(ROB): boolean = (FORALL rb: oc(robe(ROB)(rb)) IMPLIES numOccBuffers(ROB) > bufferIndex(rb, ROB)) robeMatchesProg(ROB, numinst): boolean = (FORALL rb, (j: TWO): oc(robe(ROB)(rb)) IMPLIES op(robe(ROB)(rb)) = op(prog(pc(robe(ROB)(rb)))) AND r(ss(robe(ROB)(rb))(j)) = src(prog(pc(robe(ROB)(rb))))(j) AND br_pred(robe(ROB)(rb)) = branch_pred(pc(robe(ROB)(rb)), issuedBefore(numinst, ROB, rb) + 1) AND t(robe(ROB)(rb)) = t(prog(pc(robe(ROB)(rb)))) AND br_targ(robe(ROB)(rb)) = br_target(prog(pc(robe(ROB)(rb))))) activeResCorrectVal(res, ROB, numinst): boolean = (FORALL FU: a(res(FU)) IMPLIES int(res(FU)) = int_interrupt(pc(robe(ROB)(p(res(FU)))), issuedBefore(numinst, ROB, p(res(FU))) + 1) AND IF type_op(op(robe(ROB)(p(res(FU))))) = BRANCH THEN v(res(FU)) = IF branch_act(pc(robe(ROB)(p(res(FU)))), issuedBefore(numinst, ROB, p(res(FU))) + 1) THEN 1 ELSE 0 ENDIF ELSE v(res(FU)) = do_op(op(robe(ROB)(p(res(FU)))), v(ss(robe(ROB)(p(res(FU))))(1)), v(ss(robe(ROB)(p(res(FU))))(2))) ENDIF) completedROBEcorrectVal(ROB, numinst): boolean = (FORALL rb: (oc(robe(ROB)(rb)) AND NOT b(robe(ROB)(rb))) IMPLIES IF type_op(op(robe(ROB)(rb))) = BRANCH THEN v(robe(ROB)(rb)) = IF branch_act(pc(robe(ROB)(rb)), issuedBefore(numinst, ROB, rb) + 1) THEN 1 ELSE 0 ENDIF ELSE v(robe(ROB)(rb)) = do_op(op(robe(ROB)(rb)), v(ss(robe(ROB)(rb))(1)), v(ss(robe(ROB)(rb))(2))) ENDIF) headROBEcorrectVal(RF, ROB, numinst): boolean = (oc(robe(ROB)(head(ROB))) AND NOT b(robe(ROB)(head(ROB)))) IMPLIES IF type_op(op(robe(ROB)(head(ROB)))) /= BRANCH THEN v(robe(ROB)(head(ROB))) = do_op(op(robe(ROB)(head(ROB))), v(RF(r(ss(robe(ROB)(head(ROB)))(1)))), v(RF(r(ss(robe(ROB)(head(ROB)))(2))))) ELSE v(robe(ROB)(head(ROB))) = IF branch_act(pc(robe(ROB)(head(ROB))), issuedBefore(numinst, ROB, head(ROB)) + 1) THEN 1 ELSE 0 ENDIF ENDIF intBrMatch(ROB, numinst): boolean = (FORALL rb: (oc(robe(ROB)(rb)) AND NOT b(robe(ROB)(rb))) IMPLIES (int(robe(ROB)(rb)) = int_interrupt(pc(robe(ROB)(rb)), issuedBefore(numinst, ROB, rb) + 1) AND (type_op(op(robe(ROB)(rb))) = BRANCH IMPLIES (v(robe(ROB)(rb)) > 0) = branch_act(pc(robe(ROB)(rb)), issuedBefore(numinst, ROB, rb) + 1)))) robeMatchesBr(ROB, numinst, pc): boolean = (FORALL rb: oc(robe(ROB)(rb)) IMPLIES IF type_op(op(robe(ROB)(rb))) = BRANCH AND br_pred(robe(ROB)(rb)) THEN IF oc(robe(ROB)(succ(rb))) AND NOT succ(rb) = head(ROB) THEN pc(robe(ROB)(succ(rb))) = br_targ(robe(ROB)(rb)) ELSE pc = br_targ(robe(ROB)(rb)) ENDIF ELSE IF oc(robe(ROB)(succ(rb))) AND NOT succ(rb) = head(ROB) THEN pc(robe(ROB)(succ(rb))) = pc(robe(ROB)(rb)) + 1 ELSE pc = pc(robe(ROB)(rb)) + 1 ENDIF ENDIF) AllInvariants(RF, RS, RAT, ROB, numinst, pc): boolean = wrapWraps(ROB) AND headTailEq(ROB) AND occTailROBfull(ROB) AND freeHeadROBempty(ROB) AND occEqual(ROB) AND busyRAT(RAT, ROB) AND occBuffBusyRAT(RAT, ROB) AND RATpointsNewestBuff(RAT, ROB) AND occRS(RS, ROB) AND slotUnique(RS) AND RS_ROB_opsEqual(RS, ROB) AND busyROBoccRS(RS, ROB) AND opsMatchROB(ROB) AND busyOperandsNearest(ROB) AND writeBoperandsNearest(ROB) AND retiredOperandsMatchRF(RF, ROB) AND busyOpBusyROB(ROB) AND numOcc(ROB) AND robeMatchesProg(ROB, numinst) AND completedROBEcorrectVal(ROB, numinst) AND headROBEcorrectVal(RF, ROB, numinst) AND intBrMatch(ROB, numinst) AND robeMatchesBr(ROB, numinst, pc) END InvDefs3 $$$InvDefs3.prf (|InvDefs3| (|activeResCorrectVal_TCC1| "" (SUBTYPE-TCC) NIL) (|activeResCorrectVal_TCC2| "" (SUBTYPE-TCC) NIL) (|completedROBEcorrectVal_TCC1| "" (SUBTYPE-TCC) NIL) (|completedROBEcorrectVal_TCC2| "" (SUBTYPE-TCC) NIL) (|headROBEcorrectVal_TCC1| "" (SUBTYPE-TCC) NIL) (|headROBEcorrectVal_TCC2| "" (SUBTYPE-TCC) NIL)) $$$InvDefs2.pvs InvDefs2[R, U, Z: posnat, (IMPORTING more_nat_types[1]) B: greater_one_nat]: THEORY % The second of 3 files defining properties which are invariants of Spec BEGIN IMPORTING InvDefs1[R, U, Z, B] RF, RF_p: VAR [REG_ID -> RF_TYPE] RAT, RAT_p: VAR [REG_ID -> RAT_TYPE] ROB, ROB_p: VAR ROB_TYPE RS, RS_p: VAR [SLOT_ID -> RS_TYPE] res, res_p: VAR [FU_ID -> result_TYPE] pc, pc_p: VAR posnat numinst, numinst_p: VAR nat FU: VAR FU_ID S, S2: VAR SLOT_ID r: VAR REG_ID rb, rb2: VAR ROB_ID activeRes(res, RS, ROB, RS_p, ROB_p): boolean = (FORALL FU: a(res(FU)) IMPLIES oc(robe(ROB)(p(res(FU)))) AND b(robe(ROB)(p(res(FU)))) AND NOT b(robe(ROB_p)(p(res(FU)))) AND NOT (EXISTS S: oc(RS_p(S)) AND p(RS_p(S)) = p(res(FU))) AND fu_table(op(robe(ROB)(p(res(FU))))) = FU) chosenFUunique(res): boolean = (FORALL FU: a(res(FU)) IMPLIES chooseFU(p(res(FU)), res) = FU) wb_prop(res, RS, ROB, RS_p, ROB_p): boolean = activeRes(res, RS, ROB, RS_p, ROB_p) AND chosenFUunique(res) RS_ROB_opsEqual(RS, ROB): boolean = (FORALL S, (j: TWO): oc(RS(S)) IMPLIES ss(RS(S))(j) = ss(robe(ROB)(p(RS(S))))(j)) busyROBoccRS(RS, ROB): boolean = (FORALL rb: (oc(robe(ROB)(rb)) AND b(robe(ROB)(rb))) IMPLIES (EXISTS S: oc(RS(S)) AND p(RS(S)) = rb)) opsMatchROB(ROB): boolean = (FORALL rb, (j: TWO): (oc(robe(ROB)(rb)) AND st(ss(robe(ROB)(rb))(j)) /= RETIRED) IMPLIES (preceed(p(ss(robe(ROB)(rb))(j)), rb, ROB) AND IF st(ss(robe(ROB)(rb))(j)) = BUSY THEN b(robe(ROB)(p(ss(robe(ROB)(rb))(j)))) ELSE NOT b(robe(ROB)(p(ss(robe(ROB)(rb))(j)))) AND v(robe(ROB)(p(ss(robe(ROB)(rb))(j)))) = v(ss(robe(ROB)(rb))(j)) ENDIF AND r(ss(robe(ROB)(rb))(j)) = t(robe(ROB)(p(ss(robe(ROB)(rb))(j)))))) activeResOpsNotBusy(res, ROB): boolean = (FORALL FU, (j: TWO): (a(res(FU)) AND preceed(p(ss(robe(ROB)(p(res(FU))))(j)), p(res(FU)), ROB)) IMPLIES st(ss(robe(ROB)(p(res(FU))))(j)) /= BUSY) busyOperandsNearest(ROB): boolean = (FORALL rb, (j: TWO): (oc(robe(ROB)(rb)) AND st(ss(robe(ROB)(rb))(j)) = BUSY) IMPLIES preceed(p(ss(robe(ROB)(rb))(j)), rb, ROB) AND b(robe(ROB)(p(ss(robe(ROB)(rb))(j)))) AND (FORALL rb2: oc(robe(ROB)(rb2)) AND t(robe(ROB)(rb2)) = r(ss(robe(ROB)(rb))(j)) IMPLIES (weakPreceed(rb2, p(ss(robe(ROB)(rb))(j)), ROB) OR weakPreceed(rb, rb2, ROB)))) writeBoperandsNearest(ROB): boolean = (FORALL rb, (j: TWO): (oc(robe(ROB)(rb)) AND st(ss(robe(ROB)(rb))(j)) = WRITE_B) IMPLIES preceed(p(ss(robe(ROB)(rb))(j)), rb, ROB) AND NOT b(robe(ROB)(p(ss(robe(ROB)(rb))(j)))) AND v(robe(ROB)(p(ss(robe(ROB)(rb))(j)))) = v(ss(robe(ROB)(rb))(j)) AND (FORALL rb2: oc(robe(ROB)(rb2)) AND t(robe(ROB)(rb2)) = r(ss(robe(ROB)(rb))(j)) IMPLIES (weakPreceed(rb2, p(ss(robe(ROB)(rb))(j)), ROB) OR weakPreceed(rb, rb2, ROB)))) retiredOperandsMatchRF(RF, ROB): boolean = (FORALL rb, (j: TWO): (oc(robe(ROB)(rb)) AND st(ss(robe(ROB)(rb))(j)) = RETIRED) IMPLIES v(ss(robe(ROB)(rb))(j)) = v(RF(r(ss(robe(ROB)(rb))(j)))) AND (FORALL rb2: oc(robe(ROB)(rb2)) AND t(robe(ROB)(rb2)) = r(ss(robe(ROB)(rb))(j)) IMPLIES weakPreceed(rb, rb2, ROB))) END InvDefs2 $$$def.pvs def[R: posnat]: THEORY % Defintions used in Spec and Seq BEGIN IMPORTING more_nat_types REG_ID: TYPE = upto_nz[R] TARGET: TYPE = upto[R] VALUE: TYPE = real OP_TYPE: TYPE+ do_op: FUNCTION [OP_TYPE, VALUE, VALUE -> VALUE] TWO: TYPE = upto_nz[2] TYPE_OF_OP : TYPE = {BRANCH, ARITH} PC_RANGE : TYPE = posnat type_op : [OP_TYPE -> TYPE_OF_OP] SRC: TYPE = [TWO -> REG_ID] INST: TYPE = [# op:OP_TYPE, t:TARGET, br_target : PC_RANGE, src:SRC#] INST_INDEX: TYPE = posnat prog: [INST_INDEX -> INST] EXOR((b1, b2 : bool)) : bool = (b1 OR b2) AND NOT (b1 AND b2) int_interrupt: FUNCTION [PC_RANGE, nat -> bool] ext_interrupt: FUNCTION [nat -> bool] Int_interrupt_addr(pc: PC_RANGE, op : TYPE_OF_OP) : PC_RANGE = pc Ext_interrupt_addr(pc: PC_RANGE, numinst: nat) : PC_RANGE = pc branch_pred: FUNCTION [PC_RANGE, nat -> bool] branch_act: FUNCTION [PC_RANGE, nat -> bool] END def $$$def.prf (|def| (|lw_TCC1| "" (SUBTYPE-TCC) NIL) (|lw_TCC2| "" (SUBTYPE-TCC) NIL) (|lw_TCC3| "" (TERMINATION-TCC) NIL)) $$$IOdef.pvs IOdef[R, U, Z, B: posnat]: THEORY % Defintions used only in Spec BEGIN IMPORTING more_nat_types, def[R] FU_ID: TYPE = upto_nz[U] SLOT_ID: TYPE = upto_nz[Z] ROB_ID: TYPE = upto_nz[B] BUSY: TYPE = bool STATUS : TYPE = {BUSY, WRITE_B, RETIRED} OCCUPIED: TYPE = bool ACTIVE: TYPE = bool SRC_RS_TYPE: TYPE = [# st: STATUS, p: ROB_ID, v: VALUE, r: REG_ID #] SRC_TYPE: TYPE = [TWO -> SRC_RS_TYPE] SRC_ROB_TYPE: TYPE = [# p: ROB_ID, r: REG_ID, v : VALUE, st : STATUS #] RS_TYPE: TYPE = [# oc: OCCUPIED, p: ROB_ID, op: OP_TYPE, ss: SRC_TYPE #] RF_TYPE: TYPE = [# v: VALUE #] ROB_ENTRY_TYPE: TYPE = [# oc: OCCUPIED, b : BUSY, v: VALUE, t: TARGET, op: OP_TYPE, pc: PC_RANGE, br_pred : bool, br_targ : PC_RANGE, int: bool, ss: [TWO -> SRC_ROB_TYPE] #] ROB_TYPE : TYPE = [# robe : [ROB_ID -> ROB_ENTRY_TYPE], head, tail : ROB_ID, wrap : bool #] % head > tail => the ROB has been wrapped. % wrap is set to 1 when tail goes to first buffer % wrap is set to 0 when head goes to first buffer % if wrap is set and head = tail then buffer is full RAT_TYPE: TYPE = [# b: BUSY, al: ROB_ID #] result_TYPE: TYPE = [# a: ACTIVE, p: ROB_ID, v: VALUE, int : bool #] fu_table: FUNCTION[OP_TYPE -> FU_ID] pc: VAR posnat fu: VAR upto[U] Sn, S: VAR SLOT_ID r: VAR REG_ID rb: VAR ROB_ID ext_int : VAR bool RF: VAR [REG_ID -> RF_TYPE] RAT: VAR [REG_ID -> RAT_TYPE] ROB: VAR ROB_TYPE RS: VAR [SLOT_ID -> RS_TYPE] res: VAR [FU_ID -> result_TYPE] bus_active(res, fu): bool = fu > 0 AND a(res(fu)) FUn(pc): FU_ID = fu_table(op(prog(pc))) succ(rb): ROB_ID = IF (rb < B) THEN rb + 1 ELSE 1 ENDIF pred(rb): ROB_ID = IF (rb > 1) THEN rb - 1 ELSE B ENDIF occ_buffer(rb, ROB): boolean = IF (tail(ROB) > head(ROB)) THEN rb >= head(ROB) AND rb < tail(ROB) ELSE (rb < tail(ROB) OR rb >= head(ROB)) AND wrap(ROB) ENDIF can_issue(ROB): bool = TRUE; can_execute(ROB) : bool = TRUE; can_writeb(ROB) : bool = TRUE; can_retire(ROB) : bool = TRUE; dispatch(RS, ROB, Sn): bool = NOT ((tail(ROB) = head(ROB) AND wrap(ROB))) AND NOT oc(RS(Sn)) enabled(RS, S): bool = oc(RS(S)) AND (forall (j:TWO): NOT st(ss(RS(S))(j)) = BUSY) preceed((rb1, rb2: ROB_ID), ROB): boolean = oc(robe(ROB)(rb1)) AND oc(robe(ROB)(rb2)) AND rb1 /= rb2 AND IF (rb2 = head(ROB)) THEN FALSE ELSIF (rb1 = head(ROB)) THEN TRUE ELSE ((rb2 <= head(ROB) AND (rb1 < rb2 OR rb1 > head(ROB))) OR (rb1 < rb2 AND rb1 > head(ROB))) ENDIF weakPreceed((rb1, rb2: ROB_ID), ROB): boolean = rb1 = rb2 AND oc(robe(ROB)(rb1)) OR preceed(rb1, rb2, ROB) bufferIndex(rb, ROB): upto[B] = IF rb >= head(ROB) THEN rb - head(ROB) ELSE rb + B - head(ROB) ENDIF numOccBuffers(ROB): upto[B] = IF tail(ROB) > head(ROB) THEN tail(ROB) - head(ROB) ELSIF tail(ROB) = head(ROB) THEN IF wrap(ROB) THEN B ELSE 0 ENDIF ELSE tail(ROB) + B - head(ROB) ENDIF totalIssued(numinst: nat, ROB): nat = numOccBuffers(ROB) + numinst; issuedBefore(numinst:nat, ROB, rb) : nat = bufferIndex(rb, ROB) + numinst; chooseFU((prod: ROB_ID), res): upto[U] = IF (EXISTS (FU: FU_ID): a(res(FU)) AND p(res(FU)) = prod) THEN choose(LAMBDA (FU: FU_ID): a(res(FU)) AND p(res(FU)) = prod) ELSE 0 ENDIF END IOdef $$$IOdef.prf (|IOdef| (|bus_active_TCC1| "" (SUBTYPE-TCC) NIL) (|succ_TCC1| "" (SUBTYPE-TCC) NIL) (|succ_TCC2| "" (SUBTYPE-TCC) NIL) (|pred_TCC1| "" (SUBTYPE-TCC) NIL) (|pred_TCC2| "" (SUBTYPE-TCC) NIL) (|bufferIndex_TCC1| "" (SUBTYPE-TCC) NIL) (|bufferIndex_TCC2| "" (SUBTYPE-TCC) NIL) (|numOccBuffers_TCC1| "" (SUBTYPE-TCC) NIL) (|numOccBuffers_TCC2| "" (SUBTYPE-TCC) NIL) (|numOccBuffers_TCC3| "" (SUBTYPE-TCC) NIL) (|numOccBuffers_TCC4| "" (SUBTYPE-TCC) NIL) (|chooseFU_TCC1| "" (SUBTYPE-TCC) NIL) (|chooseFU_TCC2| "" (SUBTYPE-TCC) NIL)) $$$Spec.pvs Spec[R,U,Z: posnat, (IMPORTING more_nat_types[1]) B: greater_one_nat ]: THEORY % The speculative system, DES in the article, with a split transition relation defining % issue, write-back (execute) and retirement separately. BEGIN IMPORTING IOdef[R,U,Z,B] RF, RF_p: VAR [REG_ID -> RF_TYPE] RAT, RAT_p: VAR [REG_ID -> RAT_TYPE] ROB, ROB_p: VAR ROB_TYPE RS, RS_p: VAR [SLOT_ID -> RS_TYPE] res, res_p: VAR [FU_ID -> result_TYPE] pc, pc_p : VAR posnat numinst, numinst_p : VAR nat FU: VAR FU_ID S: VAR SLOT_ID r: VAR REG_ID rb : VAR ROB_ID Theta(pc, RF, RS, RAT, ROB, numinst): bool = pc = 1 AND numinst = 0 AND (FORALL r: RF(r) = (# v := 0 #) AND RAT(r) = (# b:= FALSE, al := B #)) AND (FORALL rb: NOT oc(robe(ROB)(rb))) AND tail(ROB) = 1 AND head(ROB) = 1 AND not wrap(ROB) AND (FORALL S: NOT(oc(RS(S)))) rho_issue(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p): bool = EXISTS (Sn: upto[Z]): (Sn > 0 IMPLIES (can_issue(ROB) AND dispatch(RS, ROB, Sn))) AND numinst_p = numinst AND pc_p = IF Sn > 0 THEN IF type_op(op(prog(pc))) = BRANCH AND branch_pred(pc, totalIssued(numinst, ROB) + 1) THEN br_target(prog(pc)) ELSE 1 + pc ENDIF ELSE pc ENDIF AND RAT_p = (LAMBDA r: IF Sn > 0 AND r = t(prog(pc)) THEN (# b := TRUE , al := tail(ROB) #) ELSE RAT(r) ENDIF) AND RF_p = RF AND ROB_p = IF NOT (Sn > 0) THEN ROB ELSE (# head := head(ROB), tail := succ(tail(ROB)), wrap := wrap(ROB) OR succ(tail(ROB)) = 1, robe := (LAMBDA rb: IF rb /= tail(ROB) THEN robe(ROB)(rb) ELSE (# b := TRUE, v := 0, op := op(prog(pc)), int := FALSE, oc := TRUE, br_pred := branch_pred(pc, totalIssued(numinst, ROB) + 1), br_targ := br_target(prog(pc)), t := t(prog(pc)), pc := pc, ss := (LAMBDA (j: TWO): IF b(RAT(src(prog(pc))(j))) THEN (# st := IF b(robe(ROB)(al(RAT(src(prog(pc))(j))))) THEN BUSY ELSE WRITE_B ENDIF, p := al(RAT(src(prog(pc))(j))), v := v(robe(ROB)(al(RAT(src(prog(pc))(j))))), r := src(prog(pc))(j) #) ELSE (# st := RETIRED, v := v(RF(src(prog(pc))(j))), r := src(prog(pc))(j), p := al(RAT(src(prog(pc))(j))) #) ENDIF) #) ENDIF) #) ENDIF AND RS_p = (LAMBDA S: IF S /= Sn THEN RS(S) ELSE (# oc := TRUE, p := tail(ROB), op := op(prog(pc)), ss := (LAMBDA (j: TWO): IF b(RAT(src(prog(pc))(j))) THEN (# st := IF b(robe(ROB)(al(RAT(src(prog(pc))(j))))) THEN BUSY ELSE WRITE_B ENDIF, p := al(RAT(src(prog(pc))(j))), v := v(robe(ROB)(al(RAT(src(prog(pc))(j))))), r := src(prog(pc))(j) #) ELSE (# st := RETIRED, v := v(RF(src(prog(pc))(j))), r := src(prog(pc))(j), p := al(RAT(src(prog(pc))(j))) #) ENDIF) #) ENDIF ) rho_writeb(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p, res): bool = (EXISTS (exec: [FU_ID -> boolean]), (iex: [FU_ID -> SLOT_ID]): pc_p = pc AND numinst_p = numinst AND (FORALL (FU: FU_ID): exec(FU) IMPLIES can_execute(ROB) AND enabled(RS, iex(FU)) AND fu_table(op(RS(iex(FU))))= FU) AND res = (LAMBDA (FU: FU_ID): IF exec(FU) THEN (# a := TRUE, p := p(RS(iex(FU))), v := IF type_op(op(RS(iex(FU)))) /= BRANCH THEN do_op(op(RS(iex(FU))), v(ss(RS(iex(FU)))(1)), v(ss(RS(iex(FU)))(2))) ELSIF branch_act(pc(robe(ROB)(p(RS(iex(FU))))), issuedBefore(numinst, ROB, p(RS(iex(FU)))) +1) THEN 1 ELSE 0 ENDIF, int := int_interrupt(pc(robe(ROB)(p(RS(iex(FU))))), issuedBefore(numinst, ROB, p(RS(iex(FU)))) +1) #) ELSE (# a:= false, p:= 1, v:= 0, int:= false #) ENDIF) AND RAT_p = RAT AND RF_p = RF AND ROB_p = (# head := head(ROB), tail := tail(ROB), wrap := wrap(ROB), robe := (LAMBDA rb: IF occ_buffer(rb, ROB) AND (EXISTS FU: a(res(FU)) AND p(res(FU)) = rb) THEN (# b := FALSE, v := v(res(chooseFU(rb, res))), int := int(res(chooseFU(rb, res))), t := t(robe(ROB)(rb)), ss := ss(robe(ROB)(rb)), pc := pc(robe(ROB)(rb)), op := op(robe(ROB)(rb)), br_pred := br_pred(robe(ROB)(rb)), br_targ := br_targ(robe(ROB)(rb)), oc := oc(robe(ROB)(rb)) #) ELSIF occ_buffer(rb, ROB) THEN robe(ROB)(rb) WITH [ss := (LAMBDA (j: TWO): IF st(ss(robe(ROB)(rb))(j)) = BUSY AND (EXISTS FU: a(res(FU)) AND p(ss(robe(ROB)(rb))(j)) = p(res(FU)) AND p(ss(robe(ROB)(rb))(j)) > 0) THEN (# st := WRITE_B, p := p(ss(robe(ROB)(rb))(j)), v := v(res(chooseFU(p(ss(robe(ROB)(rb))(j)), res))), r := r(ss(robe(ROB)(rb))(j)) #) ELSE ss(robe(ROB)(rb))(j) ENDIF)] ELSE robe(ROB)(rb) ENDIF ) #) AND RS_p = (LAMBDA S: IF (EXISTS FU : a(res(FU)) AND p(res(FU)) = p(RS(S))) THEN RS(S) with [oc := FALSE] ELSIF oc(RS(S)) THEN (# oc := oc(RS(S)), p := p(RS(S)), op := op(RS(S)), ss := (LAMBDA (j: TWO): IF st(ss(RS(S))(j)) = BUSY AND (EXISTS FU: a(res(FU)) AND p(ss(RS(S))(j)) = p(res(FU)) AND p(ss(RS(S))(j)) > 0) THEN (# st := WRITE_B, p := p(ss(RS(S))(j)), v := v(res(chooseFU(p(ss(RS(S))(j)), res))), r := r(ss(RS(S))(j)) #) ELSE ss(RS(S))(j) ENDIF) #) ELSE RS(S) ENDIF ) ) rho_retire(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p): bool = (EXISTS ( retire: boolean): (retire IMPLIES can_retire(ROB) AND occ_buffer(head(ROB), ROB) AND NOT b(robe(ROB)(head(ROB)))) AND IF NOT (retire AND (int(robe(ROB)(head(ROB))) OR (type_op(op(robe(ROB)(head(ROB)))) = BRANCH AND EXOR(br_pred(robe(ROB)(head(ROB))), v(robe(ROB)(head(ROB))) > 0)))) THEN numinst_p = IF NOT retire THEN numinst ELSE numinst +1 ENDIF AND pc_p = pc AND RAT_p = IF NOT retire THEN RAT ELSE (LAMBDA r: IF al(RAT(r)) = head(ROB) THEN (# b := FALSE, al := al(RAT(r)) #) ELSE RAT(r) ENDIF) ENDIF AND RF_p = IF NOT retire THEN RF ELSE (LAMBDA r: IF r = t(robe(ROB)(head(ROB))) THEN (# v := v(robe(ROB)(head(ROB))) #) ELSE RF(r) ENDIF) ENDIF AND ROB_p = IF NOT retire THEN ROB ELSE (# head := succ(head(ROB)), tail := tail(ROB), wrap := wrap(ROB) AND NOT succ(head(ROB)) = 1, robe := (LAMBDA rb: IF rb = head(ROB) THEN robe(ROB)(rb) WITH [oc := FALSE] ELSIF occ_buffer(rb, ROB) THEN robe(ROB)(rb) WITH [ ss := (LAMBDA (j: TWO): (# st := IF p(ss(robe(ROB)(rb))(j)) = head(ROB) THEN RETIRED ELSE st(ss(robe(ROB)(rb))(j)) ENDIF, v := v(ss(robe(ROB)(rb))(j)), p := p(ss(robe(ROB)(rb))(j)), r := r(ss(robe(ROB)(rb))(j)) #)) ] ELSE robe(ROB)(rb) ENDIF ) #) ENDIF AND RS_p = IF NOT retire THEN RS ELSE (LAMBDA S: IF oc(RS(S)) THEN RS(S) WITH [ ss := (LAMBDA (j: TWO): (# st := IF p(ss(RS(S))(j)) = head(ROB) THEN RETIRED ELSE st(ss(RS(S))(j)) ENDIF, p := p(ss(RS(S))(j)), v := v(ss(RS(S))(j)), r := r(ss(RS(S))(j)) #)) ] ELSE RS(S) ENDIF) ENDIF ELSE % flush everything RF_p = IF int(robe(ROB)(head(ROB))) THEN RF ELSE (LAMBDA r: IF r = t(robe(ROB)(head(ROB))) THEN IF v(robe(ROB)(head(ROB))) > 0 THEN (# v := 1#) ELSE (# v := 0#) ENDIF ELSE RF(r) ENDIF) ENDIF AND RAT_p = (LAMBDA r: (# b:= FALSE, al := B #)) AND ROB_p = (# tail := 1, head := 1, wrap := FALSE, robe := (LAMBDA rb: robe(ROB)(rb) WITH [ b := FALSE, oc := FALSE ]) #) AND RS_p = (LAMBDA S: RS(S) with [oc := FALSE]) AND numinst_p = numinst + 1 AND pc_p = IF (int(robe(ROB)(head(ROB)))) THEN Int_interrupt_addr(pc(robe(ROB)(head(ROB))), type_op(op(robe(ROB)(head(ROB))))) ELSIF v(robe(ROB)(head(ROB))) > 0 THEN br_targ(robe(ROB)(head(ROB))) ELSE pc(robe(ROB)(head(ROB))) + 1 ENDIF ENDIF ) END Spec $$$Spec.prf (|Spec| (|rho_issue_TCC1| "" (SUBTYPE-TCC) NIL) (|rho_writeb_TCC1| "" (SUBTYPE-TCC) NIL) (|rho_writeb_TCC2| "" (SUBTYPE-TCC) NIL) (|rho_writeb_TCC3| "" (SKOSIMP*) (("" (EXPAND "chooseFU") (("" (EXPAND "choose") (("" (NEW-SPLIT-IF -) (("" (REDUCE-ALL) (("" (INST? +) (("" (SIMP) NIL))))))))))))) (|rho_writeb_TCC4| "" (SKOSIMP*) (("" (EXPAND " chooseFU") (("" (NEW-SPLIT-IF -) (("" (INST?) (("" (INST?) (("" (INST?) (("" (REDUCE-ALL) NIL))))))))))))) (|rho_writeb_TCC5| "" (SKOSIMP*) (("" (EXPAND "chooseFU") (("" (NEW-SPLIT-IF -) (("" (INSTBEST) (("" (REDUCE-ALL) NIL)))))))))) $$$InvDefs1.pvs InvDefs1[R, U, Z: posnat, (IMPORTING more_nat_types[1]) B: greater_one_nat]: THEORY % The first of 3 files defining properties which are invariants of Spec BEGIN IMPORTING Spec[R, U, Z, B] RF, RF_p: VAR [REG_ID -> RF_TYPE] RAT, RAT_p: VAR [REG_ID -> RAT_TYPE] ROB, ROB_p: VAR ROB_TYPE RS, RS_p: VAR [SLOT_ID -> RS_TYPE] res, res_p: VAR [FU_ID -> result_TYPE] pc, pc_p: VAR posnat numinst, numinst_p: VAR nat FU: VAR FU_ID S, S2: VAR SLOT_ID r: VAR REG_ID rb: VAR ROB_ID wrapWraps(ROB): boolean = (wrap(ROB) IMPLIES tail(ROB) <= head(ROB)) AND (tail(ROB) < head(ROB) IMPLIES wrap(ROB)) headTailEq(ROB): boolean = ((head(ROB) = tail(ROB) AND wrap(ROB)) IMPLIES (FORALL rb: oc(robe(ROB)(rb)))) AND ((head(ROB) = tail(ROB) AND NOT wrap(ROB)) IMPLIES (FORALL rb: NOT oc(robe(ROB)(rb)))) occTailROBfull(ROB): boolean = oc(robe(ROB)(tail(ROB))) IMPLIES (tail(ROB) = head(ROB) AND wrap(ROB)) freeHeadROBempty(ROB): boolean = NOT oc(robe(ROB)(head(ROB))) IMPLIES (tail(ROB) = head(ROB) AND (FORALL rb: NOT oc(robe(ROB)(rb)))) occEqual(ROB): boolean = (FORALL rb: occ_buffer(rb, ROB) IMPLIES oc(robe(ROB)(rb))) AND (FORALL rb: oc(robe(ROB)(rb)) IMPLIES occ_buffer(rb, ROB)) busyRAT(RAT, ROB): boolean = (FORALL r: b(RAT(r)) IMPLIES oc(robe(ROB)(al(RAT(r)))) AND t(robe(ROB)(al(RAT(r)))) = r AND (FORALL (r2: REG_ID): b(RAT(r2)) AND al(RAT(r)) = al(RAT(r2)) IMPLIES r = r2)) occBuffBusyRAT(RAT, ROB): boolean = (FORALL rb: (oc(robe(ROB)(rb)) AND t(robe(ROB)(rb)) > 0) IMPLIES b(RAT(t(robe(ROB)(rb))))) RATpointsNewestBuff(RAT, ROB): boolean = (FORALL r: b(RAT(r)) IMPLIES (FORALL rb: oc(robe(ROB)(rb)) AND t(robe(ROB)(rb)) = r IMPLIES weakPreceed(rb, al(RAT(r)), ROB))) occRS(RS, ROB): boolean = (FORALL S: oc(RS(S)) IMPLIES oc(robe(ROB)(p(RS(S)))) AND b(robe(ROB)(p(RS(S)))) AND op(RS(S)) = op(robe(ROB)(p(RS(S))))) slotUnique(RS): boolean = (FORALL S, S2: (oc(RS(S)) AND oc(RS(S2)) AND p(RS(S)) = p(RS(S2))) IMPLIES S = S2) END InvDefs1 $$$InvDefs1.prf (|InvDefs1| (|occBuffBusyRAT_TCC1| "" (SUBTYPE-TCC))) $$$Invs1.pvs Invs1[R, U, Z: posnat, (IMPORTING more_nat_types[1]) B: greater_one_nat]: THEORY % The properties defined in InvDefs1 are proved invariant BEGIN IMPORTING InvDefs1[R, U, Z, B] RF, RF_p: VAR [REG_ID -> RF_TYPE] RAT, RAT_p: VAR [REG_ID -> RAT_TYPE] ROB, ROB_p: VAR ROB_TYPE RS, RS_p: VAR [SLOT_ID -> RS_TYPE] res, res_p: VAR [FU_ID -> result_TYPE] pc, pc_p: VAR posnat numinst, numinst_p: VAR nat FU: VAR FU_ID S: VAR SLOT_ID r: VAR REG_ID rb, head, tail: VAR ROB_ID wrapWraps_issue: LEMMA rho_issue(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p) AND wrapWraps(ROB) IMPLIES wrapWraps(ROB_p) wrapWraps_writeb: LEMMA rho_writeb(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p, res) AND wrapWraps(ROB) IMPLIES wrapWraps(ROB_p) wrapWraps_retire: LEMMA rho_retire(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p) AND wrapWraps(ROB) IMPLIES wrapWraps(ROB_p) freeHeadROBempty_issue: LEMMA rho_issue(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p) AND freeHeadROBempty(ROB) IMPLIES freeHeadROBempty(ROB_p) freeHeadROBempty_writeb: LEMMA rho_writeb(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p, res) AND freeHeadROBempty(ROB) IMPLIES freeHeadROBempty(ROB_p) freeHeadROBempty_retire: LEMMA rho_retire(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p) AND freeHeadROBempty(ROB) AND occEqual(ROB) IMPLIES freeHeadROBempty(ROB_p) headTailEq_issue: LEMMA rho_issue(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p) AND headTailEq(ROB) AND occEqual(ROB) AND wrapWraps(ROB) IMPLIES headTailEq(ROB_p) headTailEq_writeb: LEMMA rho_writeb(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p, res) AND headTailEq(ROB) IMPLIES headTailEq(ROB_p) headTailEq_retire: LEMMA rho_retire(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p) AND headTailEq(ROB) AND occEqual(ROB) AND wrapWraps(ROB) IMPLIES headTailEq(ROB_p) occEqual_issue: LEMMA rho_issue(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p) AND occEqual(ROB) AND wrapWraps(ROB) IMPLIES occEqual(ROB_p) occEqual_writeb: LEMMA rho_writeb(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p, res) AND occEqual(ROB) IMPLIES occEqual(ROB_p) occEqual_retire: LEMMA rho_retire(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p) AND occEqual(ROB) AND wrapWraps(ROB) IMPLIES occEqual(ROB_p) busyRAT_issue: LEMMA rho_issue(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p) AND busyRAT(RAT, ROB) AND occEqual(ROB) IMPLIES busyRAT(RAT_p, ROB_p) busyRAT_writeb: LEMMA rho_writeb(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p, res) AND busyRAT(RAT, ROB) IMPLIES busyRAT(RAT_p, ROB_p) busyRAT_retire: LEMMA rho_retire(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p) AND busyRAT(RAT, ROB) IMPLIES busyRAT(RAT_p, ROB_p) occBuffBusyRAT_issue: LEMMA rho_issue(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p) AND occBuffBusyRAT(RAT, ROB) IMPLIES occBuffBusyRAT(RAT_p, ROB_p) occBuffBusyRAT_writeb: LEMMA rho_writeb(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p, res) AND occBuffBusyRAT(RAT, ROB) IMPLIES occBuffBusyRAT(RAT_p, ROB_p) occBuffBusyRAT_retire: LEMMA rho_retire(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p) AND occBuffBusyRAT(RAT, ROB) AND RATpointsNewestBuff(RAT, ROB) IMPLIES occBuffBusyRAT(RAT_p, ROB_p) RATpointsNewestBuff_issue: LEMMA rho_issue(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p) AND RATpointsNewestBuff(RAT, ROB) AND busyRAT(RAT, ROB) AND headTailEq(ROB) AND wrapWraps(ROB) AND occEqual(ROB) IMPLIES RATpointsNewestBuff(RAT_p, ROB_p) RATpointsNewestBuff_writeb: LEMMA rho_writeb(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p, res) AND RATpointsNewestBuff(RAT, ROB) AND busyRAT(RAT, ROB) IMPLIES RATpointsNewestBuff(RAT_p, ROB_p) RATpointsNewestBuff_retire: LEMMA rho_retire(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p) AND RATpointsNewestBuff(RAT, ROB) AND occEqual(ROB) AND headTailEq(ROB) AND wrapWraps(ROB) IMPLIES RATpointsNewestBuff(RAT_p, ROB_p) occTailROBfull: LEMMA headTailEq(ROB) AND wrapWraps(ROB) AND occEqual(ROB) IMPLIES occTailROBfull(ROB) occRS_issue: LEMMA rho_issue(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p) AND occRS(RS, ROB) AND occTailROBfull(ROB) IMPLIES occRS(RS_p, ROB_p) occRS_writeb: LEMMA rho_writeb(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p, res) AND occRS(RS, ROB) IMPLIES occRS(RS_p, ROB_p) occRS_retire: LEMMA rho_retire(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p) AND occRS(RS, ROB) IMPLIES occRS(RS_p, ROB_p) slotUnique_issue: LEMMA rho_issue(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p) AND slotUnique(RS) AND occRS(RS, ROB) AND occEqual(ROB) IMPLIES slotUnique(RS_p) slotUnique_writeb: LEMMA rho_writeb(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p, res) AND slotUnique(RS) IMPLIES slotUnique(RS_p) slotUnique_retire: LEMMA rho_retire(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p) AND slotUnique(RS) IMPLIES slotUnique(RS_p) END Invs1 $$$Invs1.prf (|Invs1| (|wrapWraps_issue| "" (EXPAND-ISSUE "wrapWraps") (("" (SPLIT-ALL) (("" (APPLY (REPEAT (THEN (SPLIT -) (SIMP)))) NIL))))) (|wrapWraps_writeb| "" (EXP-INV-WRITEB :RES F) NIL) (|wrapWraps_retire| "" (APPLY (THEN (EXPAND-RETIRE "wrapWraps") (GRIND))) NIL) (|wrapWraps_extint| "" (EXPAND "rho_extint") (("" (EXPAND " wrapWraps") (("" (SKOSIMP*) (("" (REPLACE*) (("" (SIMP) NIL))))))))) (|freeHeadROBempty_issue| "" (EXP-INV-ISSUE) (("" (GRIND-BEST) NIL))) (|freeHeadROBempty_writeb| "" (EXP-INV-WRITEB :HIDEIEX T) (("" (INST?) NIL))) (|freeHeadROBempty_retire| "" (EXP-INV-RETIRE) (("" (SPLIT-ALL) (("1" (SPLIT-ALL -) (("1" (INST-CP -6 "1 + head(ROB!1)") (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST -7 "rb!1") (("1" (GROUND) NIL))))))))) ("2" (GRIND) NIL))) ("2" (INST-CP -5 "1") (("2" (SIMP) (("2" (SKOSIMP*) (("2" (INST -6 "rb!1") (("2" (GROUND) NIL))))))))))))) (|freeHeadROBempty_extint| "" (EXP-INV-EXTINT) NIL) (|headTailEq_issue| "" (EXPAND-ISSUE "headTailEq" "occEqual" "occ_buffer" "wrapWraps") (("" (APPLY (THEN (SPLIT +) (THEN (SPLIT-ALL) (SKOSIMP*) (SIMP) (GRIND)))) NIL))) (|headTailEq_writeb| "" (EXP-INV-WRITEB) NIL) (|headTailEq_retire| "" (APPLY (THEN (EXP-INV-RETIRE) (THEN (SPLIT-ALL) (GRIND-BEST)))) NIL) (|headTailEq_extint| "" (EXPAND-EXTINT "headTailEq") NIL) (|occEqual_issue| "" (EXPAND-ISSUE "occEqual" "occ_buffer" "wrapWraps") (("" (APPLY (THEN (SPLIT +) (SKOSIMP*) (GRIND))) NIL))) (|occEqual_writeb| "" (EXP-INV-WRITEB :EXPOCC T) NIL) (|occEqual_retire| "" (APPLY (THEN (EXP-INV-RETIRE) (THEN (SPLIT-ALL) (GRIND-BEST)))) NIL) (|occEqual_extint| "" (EXPAND-EXTINT "occEqual" "occ_buffer") NIL) (|busyRAT_issue| "" (EXP-INV-ISSUE :EXPOCC F :SPLIT F) (("" (INST?) (("" (APPLY (THEN (SPLIT +) (SIMP))) (("1" (SPLIT-ALL) NIL) ("2" (SPLIT-ALL) (("2" (INST? -8) (("2" (EXPAND "occ_buffer") (("2" (SIMP) (("2" (REDUCE-ALL) NIL))))))))) ("3" (SKOSIMP*) (("3" (NEW-SPLIT-IF -) (("1" (EXPAND "occ_buffer") (("1" (INST? -9) (("1" (SIMP) (("1" (REDUCE-ALL) NIL))))))) ("2" (NEW-SPLIT-IF -) (("1" (REVEAL -1) (("1" (INST -1 "r2!1") (("1" (INST -9 "tail(ROB!1)") (("1" (EXPAND "occ_buffer") (("1" (SIMP) (("1" (REDUCE-ALL) NIL))))))))))) ("2" (INST -6 "r2!1") (("2" (SIMP) NIL))))))))))))))) (|busyRAT_writeb| "" (EXP-INV-WRITEB :SPLIT F :HIDEIEX T) (("" (INST?) (("" (SIMP) NIL))))) (|busyRAT_retire| "" (EXP-INV-RETIRE :SPLIT F) (("" (INST?) (("" (CASE "retire!1") (("1" (SIMP) (("1" (REDUCE-ALL) (("1" (INST?) (("1" (SIMP) NIL))))))) ("2" (SIMP) NIL))))))) (|busyRAT_extint| "" (EXPAND-EXTINT "busyRAT") NIL) (|occBuffBusyRAT_issue| "" (EXPAND-ISSUE "occBuffBusyRAT") (("" (GRIND) NIL))) (|occBuffBusyRAT_writeb| "" (EXP-INV-WRITEB :HIDEIEX T) (("" (INST?) (("" (SIMP) NIL))))) (|occBuffBusyRAT_retire| "" (EXP-INV-RETIRE) (("1" (GRIND-BEST) NIL) ("2" (REDUCE-IF) (("2" (INST?) (("2" (SPLIT-ALL) (("2" (INSTBEST) (("2" (SIMP) (("2" (INSTBEST) (("2" (SIMP) NIL))))))))))))))) (|occBuffBusyRAT_extint| "" (EXP-INV-EXTINT) NIL) (|RATpointsNewestBuff_issue| "" (APPLY (THEN (EXP-INV-ISSUE) (SPLIT-ALL))) (("1" (GRIND-BEST) NIL) ("2" (GRIND-BEST) NIL) ("3" (INSTBEST) (("3" (INSTBEST) (("3" (INSTBEST) NIL))))) ("4" (GRIND-BEST) NIL) ("5" (SPLIT-ALL -) (("1" (INSTBEST) (("1" (INSTBEST) (("1" (INSTBEST) (("1" (INSTBEST) (("1" (SIMP) (("1" (SIMP) NIL))))))))))) ("2" (INSTBEST) (("2" (INSTBEST) (("2" (INSTBEST) (("2" (INSTBEST) (("2" (SIMP) NIL))))))))))) ("6" (SPLIT-ALL -) (("1" (GRIND-BEST) NIL) ("2" (GRIND-BEST) NIL) ("3" (GRIND-BEST) NIL) ("4" (GRIND-BEST) NIL))))) (|RATpointsNewestBuff_writeb| "" (EXP-INV-WRITEB :HIDEIEX T) (("" (GRIND-BEST) NIL))) (|RATpointsNewestBuff_retire| "" (EXP-INV-RETIRE) (("" (HIDE 1) (("" (INSTBEST) (("" (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF) (("1" (INST? :WHERE +) (("1" (SIMP) NIL))) ("2" (NEW-SPLIT-IF) (("1" (INSTBEST) (("1" (SIMP) NIL))) ("2" (INST? :WHERE +) (("2" (SIMP) NIL))))))) ("2" (SPLIT-ALL) (("1" (INST? :WHERE +) (("1" (GRIND-BEST) NIL))) ("2" (INST? :WHERE +) (("2" (GRIND-BEST) NIL))) ("3" (INSTBEST) (("3" (GRIND-BEST) NIL))) ("4" (INST? :WHERE +) (("4" (GRIND-BEST) NIL))) ("5" (INST? :WHERE +) (("5" (SIMP) NIL))) ("6" (INST? :WHERE +) (("6" (SIMP) NIL))))))))))))) (|RATpointsNewestBuff_extint| "" (EXP-INV-EXTINT) NIL) (|occTailROBfull| "" (GRIND) NIL) (|activeRes_writeb| "" (EXP-INV-WRITEB :SPLIT F) (("" (INSTBEST) (("" (EXPAND "enabled") (("" (REPLACE*) (("" (SIMP) (("" (REDUCE-ALL) (("" (HIDE -4 -6) (("" (INST?) (("" (SIMP) (("" (SIMP) (("" (APPLY (THEN (SPLIT +) (SIMP))) (("1" (GRIND-BEST) NIL) ("2" (SKOSIMP*) (("2" (GRIND-BEST) NIL))))))))))))))))))))))))) (|chosenFUunique| "" (EXPAND "rho_writeb") (("" (EXPAND "activeRes") (("" (EXPAND "chosenFUunique") (("" (EXPAND "chooseFU") (("" (SKOSIMP*) (("" (REPLACE -7) (("" (REPLACE -8) (("" (HIDE -1 -2 -5 -6 -7 -8) (("" (SIMP) (("" (INSTBEST) (("" (INSTBEST) (("" (EXPAND "enabled") (("" (SPLIT-IF-SIMP) (("1" (SKOSIMP*) (("1" (HIDE -9 -1 -2) (("1" (REVEAL -1 -2 -3) (("1" (SIMP) (("1" (SPLIT +) (("1" (SIMP) (("1" (EXPAND "choose") (("1" (USE "epsilon_ax[FU_ID[R, U, Z, B]]") (("1" (SPLIT -) (("1" (SIMP) (("1" (REVEAL -6) (("1" (INST -1 "epsilon(LAMBDA (FU_1773: FU_ID[R, U, Z, B]): a(res!1(FU_1773)) AND p(res!1(FU_1773)) = p(res!1(FU!1)))") (("1" (EXPAND "enabled") (("1" (CASE "not (exists (FU : FU_ID): epsilon(LAMBDA (FU_1773: FU_ID[R, U, Z, B]): a(res!1(FU_1773)) AND p(res!1(FU_1773)) = p(res!1(FU!1))) = FU)") (("1" (INST 1 "epsilon(LAMBDA (FU_1773: FU_ID[R, U, Z, B]): a(res!1(FU_1773)) AND p(res!1(FU_1773)) = p(res!1(FU!1)))") NIL) ("2" (SKOSIMP*) (("2" (REPLACE -1) (("2" (EXPAND "slotUnique") (("2" (HIDE -1) (("2" (REPLACE*) (("2" (SIMP) (("2" (REDUCE-ALL) (("2" (INST -20 "iex!1(FU!3)" "iex!1(FU!1)") (("2" (SIMP) NIL))))))))))))))))))))))))))) ("2" (INST 1 "FU!1") (("2" (SIMP) NIL))))))))))) ("2" (SIMP) NIL))))))))))) ("2" (INST? +) (("2" (SIMP) NIL))))))))))))))))))))))))))))) (|writeb_prop| "" (SKOSIMP*) (("" (EXPAND "wb_prop") (("" (LEMMA "activeRes_writeb") (("" (INST?) (("" (SIMP) (("" (LEMMA "chosenFUunique") (("" (INST?) (("" (SIMP) NIL))))))))))))))) (|occRS_issue| "" (EXP-INV-ISSUE :SPLIT T) (("1" (GRIND-BEST) NIL) ("2" (GRIND-BEST) NIL) ("3" (GRIND-BEST) NIL))) (|occRS_writeb| "" (EXP-INV-WRITEB :HIDEIEX T :SPLIT F) (("" (INST?) (("" (SPLIT-ALL) NIL))))) (|occRS_retire| "" (APPLY (THEN (EXP-INV-RETIRE :SPLIT T) (THEN (SPLIT-ALL) (GRIND-BEST)))) NIL) (|occRS_extint| "" (EXP-INV-EXTINT :SPLIT T) NIL) (|slotUnique_issue| "" (EXP-INV-ISSUE) (("" (INST? :WHERE 1) (("" (APPLY (THEN (SPLIT-ALL -) (GRIND-BEST))) NIL))))) (|slotUnique_writeb| "" (EXP-INV-WRITEB :HIDEIEX T) (("" (HIDE -1) (("" (INST? :WHERE 1) (("" (SPLIT-ALL -) NIL))))))) (|slotUnique_retire| "" (EXP-INV-RETIRE) (("" (INST? :WHERE +) (("" (SPLIT-ALL -) NIL))))) (|slotUnique_extint| "" (EXP-INV-EXTINT) NIL) (|occRSops_issue| "" (APPLY (THEN (EXP-INV-ISSUE) (THEN (SPLIT-ALL) (INSTBEST) (INSTBEST) (INSTBEST) (INSTBEST) (INSTBEST) (SIMP)))) (("" (APPLY (REPEAT* (THEN (INSTBEST) (SIMP)))) NIL))) (|occRSops_writeb| "" (EXP-INV-WRITEB :SPLIT F :HIDEIEX T) (("" (INST?) (("" (REDUCE-ALL) (("" (LIFT-IF) (("" (SIMP) (("" (REDUCE-ALL) (("" (HIDE -4) (("" (SPLIT 6) (("1" (SIMP) (("1" (NEW-SPLIT-IF) (("1" (SKOSIMP*) (("1" (GRIND-BEST) NIL))))))) ("2" (SIMP) (("2" (NEW-SPLIT-IF) (("2" (SKOSIMP*) (("2" (GRIND-BEST) NIL))))))))))))))))))))))) (|occRSops_retire| "" (APPLY (THEN (EXP-INV-RETIRE) (THEN (SPLIT-ALL) (INSTBEST) (INSTBEST) (INSTBEST) (INSTBEST) (SIMP)))) (("" (CASE "retire!1") (("1" (SIMP) (("1" (REDUCE-ALL) (("1" (NEW-SPLIT-IF -7) (("1" (NEW-SPLIT-IF -) (("1" (NEW-SPLIT-IF -) (("1" (SPLIT -) (("1" (SIMP) (("1" (GROUND) NIL))) ("2" (GROUND) NIL))))))))))))) ("2" (SIMP) NIL))))) (|occRSops_extint| "" (EXPAND "rho_extint") (("" (EXPAND "occTailROBfull") (("" (EXPAND "occRSops") (("" (SKOSIMP*) (("" (REPLACE*) (("" (SIMP) NIL)))))))))))) $$$Invs2.pvs Invs2[R, U, Z: posnat, (IMPORTING more_nat_types[1]) B: greater_one_nat]: THEORY % The properties defined in InvDefs2 are proved invariant BEGIN IMPORTING Invs1[R, U, Z, B], InvDefs2[R, U, Z, B] RF, RF_p: VAR [REG_ID -> RF_TYPE] RAT, RAT_p: VAR [REG_ID -> RAT_TYPE] ROB, ROB_p: VAR ROB_TYPE RS, RS_p: VAR [SLOT_ID -> RS_TYPE] res, res_p: VAR [FU_ID -> result_TYPE] pc, pc_p: VAR posnat numinst, numinst_p: VAR nat FU: VAR FU_ID S: VAR SLOT_ID r: VAR REG_ID rb, head, tail: VAR ROB_ID activeRes_writeb: LEMMA rho_writeb(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p, res) AND occRS(RS, ROB) AND occEqual(ROB) IMPLIES activeRes(res, RS, ROB, RS_p, ROB_p) chosenFUunique: LEMMA rho_writeb(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p, res) AND activeRes(res, RS, ROB, RS_p, ROB_p) AND slotUnique(RS) IMPLIES chosenFUunique(res) writeb_prop: LEMMA rho_writeb(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p, res) AND occRS(RS, ROB) AND occEqual(ROB) AND slotUnique(RS) IMPLIES wb_prop(res, RS, ROB, RS_p, ROB_p) RS_ROB_opsEqual_issue: LEMMA rho_issue(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p) AND RS_ROB_opsEqual(RS, ROB) AND occRS(RS, ROB) AND occTailROBfull(ROB) IMPLIES RS_ROB_opsEqual(RS_p, ROB_p) RS_ROB_opsEqual_writeb: LEMMA rho_writeb(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p, res) AND RS_ROB_opsEqual(RS, ROB) AND occRS(RS, ROB) AND occEqual(ROB) IMPLIES RS_ROB_opsEqual(RS_p, ROB_p) RS_ROB_opsEqual_retire: LEMMA rho_retire(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p) AND RS_ROB_opsEqual(RS, ROB) AND occRS(RS, ROB) AND occEqual(ROB) IMPLIES RS_ROB_opsEqual(RS_p, ROB_p) busyROBoccRS_issue: LEMMA rho_issue(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p) AND busyROBoccRS(RS, ROB) IMPLIES busyROBoccRS(RS_p, ROB_p) busyROBoccRS_writeb: LEMMA rho_writeb(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p, res) AND busyROBoccRS(RS, ROB) AND occEqual(ROB) IMPLIES busyROBoccRS(RS_p, ROB_p) busyROBoccRS_retire: LEMMA rho_retire(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p) AND busyROBoccRS(RS, ROB) IMPLIES busyROBoccRS(RS_p, ROB_p) opsMatchROB_issue: LEMMA rho_issue(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p) AND opsMatchROB(ROB) AND headTailEq(ROB) AND occTailROBfull(ROB) AND occEqual(ROB) AND busyRAT(RAT, ROB) IMPLIES opsMatchROB(ROB_p) opsMatchROB_writeb: LEMMA rho_writeb(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p, res) AND opsMatchROB(ROB) AND occEqual(ROB) AND occRS(RS, ROB) AND slotUnique(RS) IMPLIES opsMatchROB(ROB_p) opsMatchROB_retire: LEMMA rho_retire(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p) AND opsMatchROB(ROB) AND occEqual(ROB) IMPLIES opsMatchROB(ROB_p) busyOperandsNearest_issue: LEMMA rho_issue(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p) AND busyOperandsNearest(ROB) AND headTailEq(ROB) AND occEqual(ROB) AND occTailROBfull(ROB) AND busyRAT(RAT, ROB) AND RATpointsNewestBuff(RAT, ROB) IMPLIES busyOperandsNearest(ROB_p) busyOperandsNearest_writeb: LEMMA rho_writeb(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p, res) AND busyOperandsNearest(ROB) AND occEqual(ROB) IMPLIES busyOperandsNearest(ROB_p) busyOperandsNearest_retire: LEMMA rho_retire(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p) AND busyOperandsNearest(ROB) IMPLIES busyOperandsNearest(ROB_p) writeBoperandsNearest_issue: LEMMA rho_issue(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p) AND writeBoperandsNearest(ROB) AND headTailEq(ROB) AND occEqual(ROB) AND occTailROBfull(ROB) AND busyRAT(RAT, ROB) AND RATpointsNewestBuff(RAT, ROB) IMPLIES writeBoperandsNearest(ROB_p) writeBoperandsNearest_writeb: LEMMA rho_writeb(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p, res) AND writeBoperandsNearest(ROB) AND busyOperandsNearest(ROB) AND occEqual(ROB) AND occRS(RS, ROB) AND slotUnique(RS) IMPLIES writeBoperandsNearest(ROB_p) writeBoperandsNearest_retire: LEMMA rho_retire(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p) AND writeBoperandsNearest(ROB) AND occEqual(ROB) IMPLIES writeBoperandsNearest(ROB_p) retiredOperandsMatchRF_issue: LEMMA rho_issue(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p) AND retiredOperandsMatchRF(RF, ROB) AND headTailEq(ROB) AND occEqual(ROB) AND occBuffBusyRAT(RAT, ROB) IMPLIES retiredOperandsMatchRF(RF_p, ROB_p) retiredOperandsMatchRF_writeb: LEMMA rho_writeb(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p, res) AND retiredOperandsMatchRF(RF, ROB) AND occEqual(ROB) IMPLIES retiredOperandsMatchRF(RF_p, ROB_p) retiredOperandsMatchRF_retire: LEMMA rho_retire(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p) AND retiredOperandsMatchRF(RF, ROB) AND writeBoperandsNearest(ROB) AND opsMatchROB(ROB) AND freeHeadROBempty(ROB) AND occEqual(ROB) IMPLIES retiredOperandsMatchRF(RF_p, ROB_p) END Invs2 $$$Invs2.prf (|Invs2| (|activeRes_writeb| "" (EXP-INV-WRITEB :SPLIT F) (("" (INSTBEST) (("" (REPLACE*) (("" (SIMP) (("" (REDUCE-ALL) (("" (HIDE -4 -6) (("" (INST?) (("" (SIMP) (("" (SIMP) (("" (APPLY (THEN (SPLIT +) (SIMP))) (("1" (GRIND-BEST) NIL) ("2" (SKOSIMP*) (("2" (GRIND-BEST) NIL))))))))))))))))))))))) (|chosenFUunique| "" (EXPAND "rho_writeb") (("" (EXPAND "activeRes") (("" (EXPAND "chosenFUunique") (("" (EXPAND "chooseFU") (("" (SKOSIMP*) (("" (REPLACE -7) (("" (REPLACE -8) (("" (HIDE -1 -2 -5 -6 -7 -8) (("" (SIMP) (("" (INSTBEST) (("" (INSTBEST) (("" (EXPAND "enabled") (("" (SPLIT-IF-SIMP) (("1" (SKOSIMP*) (("1" (HIDE -9 -1 -2) (("1" (REVEAL -1 -2 -3) (("1" (SIMP) (("1" (SPLIT +) (("1" (SIMP) (("1" (EXPAND "choose") (("1" (USE "epsilon_ax[FU_ID[R, U, Z, B]]") (("1" (SPLIT -) (("1" (SIMP) (("1" (REVEAL -6) (("1" (INST -1 "epsilon(LAMBDA (FU_1773: FU_ID[R, U, Z, B]): a(res!1(FU_1773)) AND p(res!1(FU_1773)) = p(res!1(FU!1)))") (("1" (EXPAND "enabled") (("1" (CASE "not (exists (FU : FU_ID): epsilon(LAMBDA (FU_1773: FU_ID[R, U, Z, B]): a(res!1(FU_1773)) AND p(res!1(FU_1773)) = p(res!1(FU!1))) = FU)") (("1" (INST 1 "epsilon(LAMBDA (FU_1773: FU_ID[R, U, Z, B]): a(res!1(FU_1773)) AND p(res!1(FU_1773)) = p(res!1(FU!1)))") NIL) ("2" (SKOSIMP*) (("2" (REPLACE -1) (("2" (EXPAND "slotUnique") (("2" (HIDE -1) (("2" (REPLACE*) (("2" (SIMP) (("2" (REDUCE-ALL) (("2" (INST -20 "iex!1(FU!3)" "iex!1(FU!1)") (("2" (SIMP) NIL))))))))))))))))))))))))))) ("2" (INST 1 "FU!1") (("2" (SIMP) NIL))))))))))) ("2" (SIMP) NIL))))))))))) ("2" (INST? +) (("2" (SIMP) NIL))))))))))))))))))))))))))))) (|writeb_prop| "" (SKOSIMP*) (("" (EXPAND "wb_prop") (("" (LEMMA "activeRes_writeb") (("" (INST?) (("" (SIMP) (("" (LEMMA "chosenFUunique") (("" (INST?) (("" (SIMP) NIL))))))))))))))) (|RS_ROB_opsEqual_issue| "" (EXP-INV-ISSUE :SPLIT F) (("" (INSTBEST) (("" (INSTBEST) (("" (SPLIT-ALL) NIL))))))) (|RS_ROB_opsEqual_writeb| "" (EXP-INV-WRITEB :SPLIT F :EXPOCC F :HIDEIEX T) (("" (INST?) (("" (INST?) (("" (HIDE -1) (("" (REDUCE-ALL) (("" (INST? -) (("" (INST? -) (("" (SIMP) NIL))))))))))))))) (|RS_ROB_opsEqual_retire| "" (EXP-INV-RETIRE :SPLIT F :EXPOCC F) (("" (INSTBEST) (("" (INSTBEST) (("" (INSTBEST) (("" (APPLY (THEN (SPLIT-ALL) (GRIND-BEST))) NIL))))))))) (|RS_ROB_opsEqual_extint| "" (EXP-INV-EXTINT) NIL) (|busyROBoccRS_issue| "" (EXP-INV-ISSUE) (("" (INST?) (("" (SPLIT -2) (("1" (SKOSIMP*) (("1" (INST 1 "S!1") (("1" (SPLIT-ALL) NIL))))) ("2" (SIMP) (("2" (REDUCE-ALL) (("2" (INST? +) (("2" (SIMP) NIL))))))) ("3" (REDUCE-ALL) (("3" (INST? +) (("3" (SIMP) NIL))))))))))) (|busyROBoccRS_writeb| "" (EXP-INV-WRITEB :SPLIT F :HIDEIEX T) (("" (HIDE -1) (("" (INST?) (("" (REDUCE-ALL) (("" (INST? +) (("" (SIMP) (("" (INST?) (("" (INST?) (("" (SPLIT-ALL) NIL))))))))))))))))) (|busyROBoccRS_retire| "" (EXP-INV-RETIRE) (("" (INST -2 "rb!1") (("" (NEW-SPLIT-IF) NIL))))) (|busyROBoccRS_extint| "" (EXPAND "busyROBoccRS") (("" (EXP-INV-EXTINT) NIL))) (|opsMatchROB_issue| "" (APPLY (THEN (EXP-INV-ISSUE) (INSTBEST) (SIMP))) (("1" (SPLIT-ALL) (("1" (GRIND-BEST) NIL))) ("2" (SPLIT-ALL) (("2" (GRIND-BEST) NIL))) ("3" (SPLIT-ALL) (("3" (CLEAN-UP) (("3" (INST? -7) (("3" (GRIND-BEST) NIL))))))) ("4" (SPLIT-ALL) (("4" (INSTBEST) (("4" (CLEAN-UP) (("4" (SIMP) (("4" (NEW-SPLIT-IF -) (("1" (INST?) (("1" (INST? :WHERE -8) (("1" (SIMP) (("1" (SIMP) NIL))))))) ("2" (INST?) (("2" (INST? :WHERE -7) (("2" (SIMP) NIL))))))))))))))) ("5" (SPLIT-ALL) NIL) ("6" (SPLIT-ALL) (("6" (GRIND-BEST) NIL))) ("7" (SPLIT-ALL) (("1" (APPLY (REPEAT* (THEN (INSTBEST) (SIMP)))) NIL) ("2" (GRIND-BEST) NIL) ("3" (INST?) (("3" (SIMP) NIL))) ("4" (INST?) (("4" (SIMP) NIL))))))) (|opsMatchROB_writeb| "" (LEMMA "writeb_prop") (("" (SKOSIMP*) (("" (INST?) (("" (SIMP) (("" (HIDE -1) (("" (EXP-INV-WRITEB :EXPOCC F :SPLIT F :HIDEIEX F) (("" (HIDE -1) (("" (INST?) (("" (INST? -4 :COPY? T) (("" (INST -4 "p(ss(robe(ROB!1)(rb!1))(j!1))") (("" (HIDE -1) (("" (NEW-SPLIT-IF) (("1" (SKOSIMP*) (("1" (INST?) (("1" (REDUCE-ALL) (("1" (SPLIT -) (("1" (SIMP) NIL) ("2" (SIMP) (("2" (SPLIT +) (("1" (PROPAX) NIL) ("2" (SIMP) NIL) ("3" (SIMP) NIL))))))))))))) ("2" (NEW-SPLIT-IF) (("1" (REDUCE-ALL) (("1" (NEW-SPLIT-IF -) (("1" (NEW-SPLIT-IF) (("1" (INSTBEST +) NIL))) ("2" (NEW-SPLIT-IF) (("2" (INSTBEST +) NIL))))))) ("2" (SPLIT -) (("1" (REDUCE-ALL) (("1" (NEW-SPLIT-IF -) (("1" (NEW-SPLIT-IF) (("1" (SKOSIMP*) (("1" (INST? +) (("1" (SIMP) NIL))))))) ("2" (NEW-SPLIT-IF) (("2" (SKOSIMP*) (("2" (INST? +) (("2" (SIMP) NIL))))))))))) ("2" (REDUCE-ALL) (("2" (CLEAN-UP) (("2" (CASE "not (EXISTS (FU: FU_ID[R, U, Z, B]): a(res!1(FU)) AND p(res!1(FU)) = p(ss(robe(ROB!1)(rb!1))(j!1)))") (("1" (NEW-SPLIT-IF -) NIL) ("2" (SKOSIMP*) (("2" (REVEAL -11) (("2" (EXPAND "wb_prop") (("2" (EXPAND "chosenFUunique") (("2" (SIMP) (("2" (INST? -) (("2" (EXPAND "activeRes") (("2" (INST?) (("2" (NEW-SPLIT-IF) NIL))))))))))))))))))))))))))))))))))))))))))))))))))) (|opsMatchROB_retire| "" (EXP-INV-RETIRE :EXPOCC F) (("" (INSTBEST) (("" (APPLY (THEN (SPLIT 3) (SPLIT-ALL))) (("1" (INSTBEST) (("1" (INSTBEST) (("1" (SIMP) NIL))))) ("2" (SPLIT-ALL -) NIL) ("3" (INST -9 "1 + head(ROB!1)") (("3" (SIMP) NIL))) ("4" (INST? - :WHERE +) (("4" (INST? - :WHERE +) (("4" (SIMP) NIL))))) ("5" (SPLIT-ALL -) NIL) ("6" (INST? - :WHERE +) (("6" (INST? - :WHERE +) (("6" (SIMP) NIL))))) ("7" (SPLIT-ALL -) (("1" (SPLIT -) (("1" (SIMP) (("1" (SPLIT -) (("1" (PROPAX) NIL) ("2" (SIMP) NIL))))) ("2" (SIMP) NIL))) ("2" (SPLIT -) (("1" (SIMP) (("1" (SPLIT -) (("1" (PROPAX) NIL) ("2" (SIMP) NIL))))) ("2" (SIMP) NIL))))) ("8" (INST? - :WHERE +) (("8" (INST? - :WHERE +) (("8" (SIMP) NIL))))) ("9" (INST? - :WHERE +) (("9" (INST? - :WHERE +) (("9" (SIMP) NIL))))))))))) (|opsMatchROB_extint| "" (EXP-INV-EXTINT) NIL) (|busyOperandsNearest_issue| "" (EXP-INV-ISSUE :SPLIT F) (("" (INST?) (("" (APPLY (THEN (SPLIT +) (SIMP))) (("1" (SPLIT-ALL) (("1" (INST?) (("1" (SIMP) NIL))))) ("2" (LIFT-IF) (("2" (INST?) (("2" (INST?) (("2" (SPLIT-ALL -) NIL))))))) ("3" (APPLY (THEN (REPEAT (INSTBEST)))) (("3" (SPLIT-ALL -) (("3" (INST?) (("3" (INST?) NIL))))))) ("4" (INST? -8) (("4" (INST? -9) (("4" (INST? -6 :COPY? T) (("4" (INST? -5 :COPY? T) (("4" (SPLIT-ALL) (("4" (NEW-SPLIT-IF -) (("1" (INST?) (("1" (INST?) (("1" (SIMP) (("1" (SIMP) NIL))))))) ("2" (INST?) (("2" (INST?) (("2" (SIMP) NIL))))))))))))))))) ("5" (APPLY (THEN (REPEAT (INSTBEST)))) (("5" (SPLIT-ALL) NIL))) ("6" (SKOSIMP*) (("6" (INST-CP -7 "rb!1") (("6" (INST-CP -9 "rb!1") (("6" (INST? -12) (("6" (INST? -13) (("6" (SPLIT-ALL) (("1" (INST -4 "rb2!1") (("1" (GROUND) NIL))) ("2" (INST -4 "rb2!1") (("2" (GROUND) NIL))) ("3" (INST -4 "rb2!1") (("3" (GROUND) NIL))) ("4" (NEW-SPLIT-IF -) NIL) ("5" (INST -4 "rb2!1") (("5" (GROUND) NIL))) ("6" (NEW-SPLIT-IF -) NIL) ("7" (INST?) (("7" (INST? :WHERE +) (("7" (SIMP) NIL))))) ("8" (INST?) (("8" (INST?) (("8" (SIMP) (("8" (GROUND) NIL))))))))))))))))))))))))) (|busyOperandsNearest_writeb| "" (SKOSIMP*) (("" (EXP-INV-WRITEB :SPLIT F :EXPOCC F) (("" (HIDE -1 -2) (("" (INST?) (("" (INST-CP -3 "rb!1") (("" (INST -3 "p(ss(robe(ROB!1)(rb!1))(j!1))") (("" (SIMP) (("" (LIFT-IF -6) (("" (CASE "not st(ss(robe(ROB!1)(rb!1))(j!1)) = BUSY") (("1" (SIMP) NIL) ("2" (SIMP) (("2" (REDUCE-ALL) (("2" (SPLIT +) (("1" (SIMP) (("1" (SKOSIMP*) (("1" (NEW-SPLIT-IF -12) (("1" (NEW-SPLIT-IF -) (("1" (INST? +) NIL))))))))) ("2" (SIMP) NIL) ("3" (SKOSIMP*) (("3" (INST? -) (("3" (SIMP) (("3" (GROUND) NIL))))))))))))))))))))))))))))))) (|busyOperandsNearest_retire| "" (APPLY (THEN (EXP-INV-RETIRE :EXPOCC F) (INSTBEST) (SIMP))) (("1" (SPLIT-ALL -) NIL) ("2" (SPLIT-ALL -) NIL) ("3" (SPLIT-ALL -) (("3" (GROUND) NIL))) ("4" (GROUND) (("1" (SPLIT-ALL -) NIL) ("2" (SPLIT-ALL -) NIL))) ("5" (SPLIT -4) (("1" (SIMP) (("1" (INST -5 "rb2!1") (("1" (APPLY (THEN (SPLIT-ALL) (GROUND))) NIL))))) ("2" (SIMP) NIL) ("3" (APPLY (THEN (SPLIT-ALL) (GROUND))) NIL))))) (|busyOperandsNearest_extint| "" (EXP-INV-EXTINT) NIL) (|writeBoperandsNearest_issue| "" (EXP-INV-ISSUE :SPLIT F) (("" (INSTBEST) (("" (INST? -8) (("" (INST? -9) (("" (INST-CP -6 "rb!1") (("" (APPLY (THEN (SPLIT +) (SIMP))) (("1" (SPLIT-ALL) NIL) ("2" (SPLIT-ALL -) NIL) ("3" (NEW-SPLIT-IF -11) (("3" (NEW-SPLIT-IF -) (("3" (REDUCE-ALL) (("3" (INST?) NIL))))))) ("4" (SPLIT-ALL) (("4" (GRIND-BEST) NIL))) ("5" (SPLIT-ALL -) NIL) ("6" (SPLIT-ALL) NIL) ("7" (SKOSIMP*) (("7" (CASE "oc(robe(ROB!1)(rb!1)) AND st(ss(robe(ROB!1)(rb!1))(j!1)) = WRITE_B") (("1" (SIMP) (("1" (INST -9 "rb2!1") (("1" (SPLIT-ALL) (("1" (NEW-SPLIT-IF -) NIL) ("2" (NEW-SPLIT-IF -) NIL))))))) ("2" (SPLIT-ALL) (("1" (INST?) (("1" (INST? :WHERE -5) (("1" (SIMP) NIL))))) ("2" (INST?) (("2" (INST? :WHERE -4) (("2" (SIMP) (("2" (GROUND) NIL))))))))))))))))))))))))) (|writeBoperandsNearest_writeb| "" (SKOSIMP*) (("" (LEMMA "writeb_prop") (("" (INST?) (("" (SIMP) (("" (EXPAND "wb_prop") (("" (SIMP) (("" (HIDE -1 -7 -8) (("" (HIDE -1 -2 -3 -4 -5) (("" (REVEAL -1) (("" (REVEAL -2 -3 -4 -5) (("" (EXP-INV-WRITEB :SPLIT F :EXPOCC F) (("" (HIDE -1 -2) (("" (INSTBEST) (("" (INSTBEST) (("" (APPLY (THEN (SPLIT +) (SIMP))) (("1" (SPLIT-ALL) NIL) ("2" (LIFT-IF) (("2" (SIMP) (("2" (REDUCE-ALL) (("2" (INST?) (("2" (INST?) (("2" (SPLIT +) (("1" (INST? -) (("1" (SIMP) NIL))) ("2" (INSTBEST +) NIL))))))))))))) ("3" (INST-CP -4 "rb!1") (("3" (INST-CP -4 "p(ss(robe(ROB!1)(rb!1))(j!1))") (("3" (SIMP) (("3" (CASE "st(ss(robe(ROB!1)(rb!1))(j!1)) = WRITE_B ") (("1" (SIMP) (("1" (CLEAN-UP) (("1" (REDUCE-ALL) (("1" (NEW-SPLIT-IF) (("1" (SKOSIMP*) (("1" (REVEAL -17) (("1" (EXPAND "activeRes") (("1" (INST?) (("1" (INSTBEST) (("1" (INSTBEST) (("1" (INST?) (("1" (SIMP) NIL))))))))))))))))))))))) ("2" (SIMP) (("2" (CASE "st(ss(robe(ROB!1)(rb!1))(j!1)) = BUSY") (("1" (SIMP) (("1" (CLEAN-UP) (("1" (LIFT-IF) (("1" (SIMP) (("1" (REDUCE-ALL) (("1" (SPLIT-ALL) (("1" (INSTBEST +) NIL))))))))))))) ("2" (LIFT-IF) (("2" (SIMP) NIL))))))))))))))) ("4" (SKOSIMP*) (("4" (SIMP) (("4" (CASE "st(ss(robe(ROB!1)(rb!1))(j!1)) = WRITE_B") (("1" (SIMP) (("1" (INST?) (("1" (CLEAN-UP) (("1" (REDUCE-ALL) NIL))))))) ("2" (LIFT-IF) (("2" (SIMP) (("2" (REDUCE-ALL) (("2" (INST? +) (("2" (SPLIT-ALL) (("1" (INST -4 "rb2!1") (("1" (SIMP) (("1" (GROUND) NIL))))) ("2" (INST -4 "rb2!1") (("2" (GROUND) NIL))))))))))))))))))))))))))))))))))))))))))))))))) (|writeBoperandsNearest_retire| "" (EXP-INV-RETIRE :SPLIT F :EXPOCC F) (("" (INSTBEST) (("" (NEW-SPLIT-IF) (("1" (CLEAN-UP) (("1" (REDUCE-IF) (("1" (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF) (("1" (SKOSIMP*) (("1" (INST? -) (("1" (SIMP) (("1" (NEW-SPLIT-IF) NIL))))))))))))))) ("2" (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF) (("1" (INST -8 "1 + head(ROB!1)") (("1" (SIMP) (("1" (NEW-SPLIT-IF -) NIL))))) ("2" (NEW-SPLIT-IF -) (("2" (NEW-SPLIT-IF -) (("1" (INST -8 "rb!1") (("1" (SIMP) NIL))) ("2" (NEW-SPLIT-IF) (("1" (SKOSIMP*) (("1" (INST -7 "rb2!1") (("1" (SPLIT-ALL) (("1" (SPLIT -7) (("1" (SIMP) NIL) ("2" (SIMP) (("2" (SPLIT -2) (("1" (PROPAX) NIL) ("2" (SIMP) NIL))))) ("3" (SIMP) NIL))))))))) ("2" (SPLIT 2) (("1" (SPLIT -2) (("1" (SIMP) (("1" (SPLIT -2) (("1" (PROPAX) NIL) ("2" (SIMP) NIL))))) ("2" (SIMP) NIL))) ("2" (SKOSIMP*) (("2" (INST -6 "rb2!1") (("2" (SPLIT-ALL) (("2" (SPLIT -) (("1" (SIMP) (("1" (SPLIT -) (("1" (SIMP) (("1" (SPLIT -) (("1" (PROPAX) NIL) ("2" (SIMP) NIL) ("3" (SIMP) NIL) ("4" (SIMP) NIL))))) ("2" (SIMP) (("2" (SPLIT -) (("1" (SIMP) NIL) ("2" (SIMP) NIL))))))))) ("2" (SIMP) NIL))))))))))))))))))) ("2" (SPLIT-ALL) (("1" (INST -7 "1") (("1" (SIMP) (("1" (NEW-SPLIT-IF -) NIL))))) ("2" (INST -10 "rb2!1") (("2" (SIMP) NIL))) ("3" (INST? -11) (("3" (SIMP) NIL))) ("4" (INST?) (("4" (SIMP) NIL))))))))))))) (|writeBoperandsNearest_extint| "" (EXP-INV-EXTINT) NIL) (|retiredOperandsMatchRF_issue| "" (EXP-INV-ISSUE :SPLIT F) (("" (INSTBEST) (("" (APPLY (THEN (SPLIT +) (SIMP))) (("1" (SPLIT-ALL) NIL) ("2" (SKOSIMP*) (("2" (SPLIT -4) (("1" (SIMP) (("1" (INSTBEST) (("1" (SPLIT-ALL) (("1" (SPLIT-ALL -) (("1" (GRIND-BEST) NIL) ("2" (GRIND-BEST) NIL) ("3" (GRIND-BEST) NIL))) ("2" (GRIND-BEST) NIL) ("3" (GRIND-BEST) NIL))))))) ("2" (SPLIT-ALL) (("1" (INST -11 "head(ROB!1)") (("1" (SIMP) NIL))) ("2" (INST -10 "rb2!1") (("2" (SIMP) NIL))))) ("3" (SPLIT-ALL) (("1" (INST -11 "head(ROB!1)") (("1" (SIMP) NIL))) ("2" (INST -10 "rb2!1") (("2" (SIMP) NIL))))))))))))))) (|retiredOperandsMatchRF_writeb| "" (EXP-INV-WRITEB :SPLIT F :EXPOCC F :HIDEIEX T) (("" (HIDE -1) (("" (INST?) (("" (INST?) (("" (INST?) (("" (SPLIT +) (("1" (SPLIT-ALL) NIL) ("2" (SKOSIMP*) (("2" (SIMP) (("2" (SPLIT -) (("1" (SIMP) (("1" (INST?) (("1" (SPLIT-ALL) NIL))))) ("2" (SPLIT-ALL) NIL))))))))))))))))))) (|retiredOperandsMatchRF_retire| "" (EXP-INV-RETIRE :EXPOCC F) (("1" (APPLY (REPEAT* (INSTBEST))) (("1" (SPLIT-ALL) (("1" (SPLIT-ALL -) (("1" (GRIND-BEST) NIL) ("2" (GRIND-BEST) NIL) ("3" (GRIND-BEST) NIL))))))) ("2" (APPLY (REPEAT* (INSTBEST))) (("2" (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF) (("1" (GRIND-BEST) NIL) ("2" (SPLIT-ALL) (("2" (INST -5 "rb2!1") (("2" (GROUND) NIL))))))) ("2" (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF) (("1" (REDUCE-IF) (("1" (CASE "st(ss(robe(ROB!1)(rb!1))(j!1)) = RETIRED") (("1" (SIMP) (("1" (INST -11 "rb2!1") (("1" (GROUND) NIL))))) ("2" (SIMP) (("2" (REDUCE-IF) (("2" (SIMP) (("2" (CLEAN-UP) (("2" (SPLIT-ALL -) (("2" (INST -5 "rb2!1") (("2" (GROUND) NIL))))))))))))))))) ("2" (SPLIT-ALL) (("2" (CASE "not st(ss(robe(ROB!1)(rb!1))(j!1)) = RETIRED") (("1" (REPLACE 1) (("1" (REDUCE-IF) (("1" (REDUCE-IF) (("1" (CLEAN-UP) (("1" (SPLIT-ALL -) (("1" (INST -13 "rb2!1") (("1" (GROUND) NIL))))))))))))) ("2" (SIMP) (("2" (INST -10 "rb2!1") (("2" (GROUND) NIL))))))))))) ("2" (APPLY (REPEAT* (REDUCE-IF))) (("2" (SIMP) (("2" (APPLY (THEN (CASE "st(ss(robe(ROB!1)(rb!1))(j!1)) = RETIRED") (SIMP))) (("1" (INST -9 "rb2!1") (("1" (GROUND) NIL))) ("2" (APPLY (REPEAT* (THEN (REDUCE-IF) (SIMP)))) (("2" (INST -13 "rb2!1") (("2" (CLEAN-UP) (("2" (GROUND) NIL))))))))))))))))))))) (|retiredOperandsMatchRF_extint| "" (EXP-INV-EXTINT) NIL)) $$$Invs3.pvs Invs3[R, U, Z: posnat, (IMPORTING more_nat_types[1]) B: greater_one_nat]: THEORY % The properties defined in InvDefs3 are proved invariant BEGIN IMPORTING Invs2[R, U, Z, B], InvDefs3[R, U, Z, B] RF, RF_p: VAR [REG_ID -> RF_TYPE] RAT, RAT_p: VAR [REG_ID -> RAT_TYPE] ROB, ROB_p: VAR ROB_TYPE RS, RS_p: VAR [SLOT_ID -> RS_TYPE] res: VAR [FU_ID -> result_TYPE] pc, pc_p: VAR posnat numinst, numinst_p: VAR nat FU: VAR FU_ID S: VAR SLOT_ID r: VAR REG_ID rb, head, tail: VAR ROB_ID numOcc_issue: LEMMA rho_issue(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p) AND numOcc(ROB) AND occEqual(ROB) AND wrapWraps(ROB) IMPLIES numOcc(ROB_p) numOcc_writeb: LEMMA rho_writeb(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p, res) AND numOcc(ROB) IMPLIES numOcc(ROB_p) numOcc_retire: LEMMA rho_retire(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p) AND numOcc(ROB) AND occEqual(ROB) IMPLIES numOcc(ROB_p) busyOpBusyROB_issue: LEMMA rho_issue(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p) AND busyOpBusyROB(ROB) IMPLIES busyOpBusyROB(ROB_p) busyOpBusyROB_writeb: LEMMA rho_writeb(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p, res) AND busyOpBusyROB(ROB) AND RS_ROB_opsEqual(RS, ROB) AND occEqual(ROB) IMPLIES busyOpBusyROB(ROB_p) busyOpBusyROB_retire: LEMMA rho_retire(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p) AND busyOpBusyROB(ROB) IMPLIES busyOpBusyROB(ROB_p) robeMatchesProg_issue: LEMMA rho_issue(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p) AND robeMatchesProg(ROB, numinst) IMPLIES robeMatchesProg(ROB_p, numinst_p) robeMatchesProg_writeb: LEMMA rho_writeb(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p, res) AND robeMatchesProg(ROB, numinst) IMPLIES robeMatchesProg(ROB_p, numinst_p) robeMatchesProg_retire: LEMMA rho_retire(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p) AND robeMatchesProg(ROB, numinst) IMPLIES robeMatchesProg(ROB_p, numinst_p) completedROBEcorrectVal_issue: LEMMA rho_issue(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p) AND completedROBEcorrectVal(ROB, numinst) IMPLIES completedROBEcorrectVal(ROB_p, numinst_p) completedROBEcorrectVal_writeb: LEMMA rho_writeb(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p, res) AND completedROBEcorrectVal(ROB, numinst) AND busyOpBusyROB(ROB) AND occEqual(ROB) AND occRS(RS, ROB) AND RS_ROB_opsEqual(RS, ROB) AND slotUnique(RS) IMPLIES completedROBEcorrectVal(ROB_p, numinst_p) completedROBEcorrectVal_retire: LEMMA rho_retire(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p) AND completedROBEcorrectVal(ROB, numinst) IMPLIES completedROBEcorrectVal(ROB_p, numinst_p) headROBEcorrectVal_issue: LEMMA rho_issue(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p) AND headROBEcorrectVal(RF, ROB, numinst) AND completedROBEcorrectVal(ROB, numinst) IMPLIES headROBEcorrectVal(RF_p, ROB_p, numinst_p) headROBEcorrectVal_writeb: LEMMA rho_writeb(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p, res) AND headROBEcorrectVal(RF, ROB, numinst) AND retiredOperandsMatchRF(RF, ROB) AND opsMatchROB(ROB) AND completedROBEcorrectVal(ROB, numinst) AND busyOpBusyROB(ROB) AND occEqual(ROB) AND occRS(RS, ROB) AND RS_ROB_opsEqual(RS, ROB) AND slotUnique(RS) IMPLIES headROBEcorrectVal(RF_p, ROB_p, numinst_p) headROBEcorrectVal_retire: LEMMA rho_retire(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p) AND headROBEcorrectVal(RF, ROB, numinst) AND completedROBEcorrectVal(ROB, numinst) AND writeBoperandsNearest(ROB) AND occEqual(ROB) AND opsMatchROB(ROB) AND retiredOperandsMatchRF(RF, ROB) AND freeHeadROBempty(ROB) IMPLIES headROBEcorrectVal(RF_p, ROB_p, numinst_p) intBrMatch_issue: LEMMA rho_issue(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p) AND intBrMatch(ROB, numinst) AND occTailROBfull(ROB) IMPLIES intBrMatch(ROB_p, numinst_p) intBrMatch_writeb: LEMMA rho_writeb(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p, res) AND intBrMatch(ROB, numinst) AND occEqual(ROB) AND occRS(RS, ROB) AND slotUnique(RS) IMPLIES intBrMatch(ROB_p, numinst_p) intBrMatch_retire: LEMMA rho_retire(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p) AND intBrMatch(ROB, numinst) IMPLIES intBrMatch(ROB_p, numinst_p) robeMatchesBr_issue: LEMMA rho_issue(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p) AND robeMatchesBr(ROB, numinst, pc) AND occTailROBfull(ROB) AND wrapWraps(ROB) AND headTailEq(ROB) AND freeHeadROBempty(ROB) AND occEqual(ROB) IMPLIES robeMatchesBr(ROB_p, numinst_p, pc_p) robeMatchesBr_writeb: LEMMA rho_writeb(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p, res) AND robeMatchesBr(ROB, numinst, pc) IMPLIES robeMatchesBr(ROB_p, numinst_p, pc_p) robeMatchesBr_retire: LEMMA rho_retire(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p) AND robeMatchesBr(ROB, numinst, pc) IMPLIES robeMatchesBr(ROB_p, numinst_p, pc_p) AllInvariants_theta: LEMMA Theta(pc, RF, RS, RAT, ROB, numinst) IMPLIES AllInvariants(RF, RS, RAT, ROB, numinst, pc) AllInvariants_issue: LEMMA rho_issue(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p) AND AllInvariants(RF, RS, RAT, ROB, numinst, pc) IMPLIES AllInvariants(RF_p, RS_p, RAT_p, ROB_p, numinst_p, pc_p) AllInvariants_writeb: LEMMA rho_writeb(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p, res) AND AllInvariants(RF, RS, RAT, ROB, numinst, pc) IMPLIES AllInvariants(RF_p, RS_p, RAT_p, ROB_p, numinst_p, pc_p) AllInvariants_retire: LEMMA rho_retire(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p) AND AllInvariants(RF, RS, RAT, ROB, numinst, pc) IMPLIES AllInvariants(RF_p, RS_p, RAT_p, ROB_p, numinst_p, pc_p) END Invs3 $$$Invs3.prf (|Invs3| (|numOcc_issue| "" (EXP-INV-ISSUE :SPLIT F) (("" (APPLY (REPEAT* (INSTBEST))) (("" (NEW-SPLIT-IF) (("1" (SPLIT-ALL -) NIL) ("2" (NEW-SPLIT-IF) (("1" (SPLIT-ALL -) NIL) ("2" (SPLIT-ALL -) NIL))))))))) (|numOcc_writeb| "" (EXP-INV-WRITEB :HIDEIEX T) (("" (GRIND-BEST) NIL))) (|numOcc_retire| "" (EXP-INV-RETIRE) (("" (INST -2 "rb!1") (("" (INST -3 "rb!1") (("" (INST -4 "rb!1") (("" (SPLIT-ALL) NIL))))))))) (|busyOpBusyROB_issue| "" (EXP-INV-ISSUE) (("1" (GRIND-BEST) NIL) ("2" (GRIND-BEST) NIL))) (|busyOpBusyROB_writeb| "" (EXP-INV-WRITEB :EXPOCC F :SPLIT F) (("" (INST? -3) (("" (INST? -5) (("" (INST? -6) (("" (NEW-SPLIT-IF) (("" (HIDE -4) (("" (SKOSIMP*) (("" (GRIND-BEST) NIL))))))))))))))) (|busyOpBusyROB_retire| "" (EXP-INV-RETIRE) (("" (GRIND-BEST) NIL))) (|robeMatchesProg_issue| "" (EXP-INV-ISSUE :SPLIT F) (("" (INSTBEST) (("" (SPLIT-ALL) NIL))))) (|robeMatchesProg_writeb| "" (EXP-INV-WRITEB :SPLIT F :HIDEIEX T) (("" (HIDE -1) (("" (INSTBEST) (("" (GROUND) NIL))))))) (|robeMatchesProg_retire| "" (EXP-INV-RETIRE :SPLIT F) (("" (INSTBEST) (("" (SPLIT-ALL) NIL))))) (|completedROBEcorrectVal_issue| "" (EXP-INV-ISSUE) (("1" (GRIND-BEST) NIL) ("2" (GRIND-BEST) NIL))) (|completedROBEcorrectVal_writeb| "" (SKOSIMP*) (("" (LEMMA "writeb_prop") (("" (INST?) (("" (SIMP) (("" (HIDE -2 -3 -4 -5 -6 -7 -8) (("" (REVEAL -1 -2 -3 -4 -5 -6) (("" (EXP-INV-WRITEB :EXPOCC F :SPLIT F) (("" (INST? -3) (("" (INST-CP -4 "rb!1" "1") (("" (INST -4 "rb!1" "2") (("" (INST? -6) (("" (INST? -7) (("" (SIMP) (("" (SPLIT-IF-SIMP) (("1" (SKOSIMP*) (("1" (SPLIT +) (("1" (SIMP) (("1" (INSTBEST) (("1" (EXPAND "wb_prop") (("1" (EXPAND "chosenFUunique") (("1" (SIMP) (("1" (INST -14 "FU!1") (("1" (REPLACE -3) (("1" (REPLACE -14) (("1" (HIDE -13) (("1" (REPLACE -5 :HIDE? T) (("1" (SIMP) (("1" (INST?) (("1" (INST-CP -11 "iex!1(FU!1)" "1") (("1" (INST -11 "iex!1(FU!1)" "2") (("1" (SPLIT-ALL) NIL))))))))))))))))))))))))))))) ("2" (SIMP) NIL))))) ("2" (REPLACE 1) (("2" (PROPAX) NIL))))))))))))))))))))))))))))))) (|completedROBEcorrectVal_retire| "" (EXP-INV-RETIRE) (("" (INST -2 "rb!1") (("" (NEW-SPLIT-IF -3) (("1" (SPLIT-ALL) NIL) ("2" (SPLIT-ALL) NIL))))))) (|headROBEcorrectVal_issue| "" (LEMMA " completedROBEcorrectVal_issue") (("" (SKOSIMP*) (("" (INST?) (("" (SIMP) (("" (HIDE -2) (("" (REVEAL -1) (("" (EXP-INV-ISSUE) (("1" (INSTBEST) (("1" (INSTBEST) (("1" (SIMP) (("1" (SPLIT-ALL) NIL))))))) ("2" (INSTBEST) (("2" (INSTBEST) (("2" (SPLIT-ALL) NIL))))))))))))))))))) (|headROBEcorrectVal_writeb| "" (LEMMA "completedROBEcorrectVal_writeb") (("" (SKOSIMP*) (("" (INST?) (("" (SIMP) (("" (EXPAND "completedROBEcorrectVal") (("" (EXPAND "headROBEcorrectVal") (("" (INST?) (("" (SIMP) (("" (SPLIT +) (("1" (CASE "(forall (j:TWO): v(RF_p!1(r(ss(robe(ROB_p!1)(head(ROB_p!1)))(j)))) = v(ss(robe(ROB_p!1)(head(ROB_p!1)))(j)))") (("1" (INST-CP -1 "1") (("1" (INST -1 "2") (("1" (SIMP) NIL))))) ("2" (HIDE -1 2) (("2" (HIDE -2 -5) (("2" (EXP-INV-WRITEB :SPLIT F) (("2" (HIDE -1 -2) (("2" (INST?) (("2" (INST?) (("2" (NEW-SPLIT-IF) NIL))))))))))))))) ("2" (SIMP) NIL))))))))))))))))))) (|headROBEcorrectVal_retire| "" (LEMMA "completedROBEcorrectVal_retire") (("" (LEMMA "opsMatchROB_retire") (("" (LEMMA "retiredOperandsMatchRF_retire") (("" (SKOSIMP*) (("" (INST?) (("" (INST?) (("" (INST?) (("" (SIMP) (("" (HIDE -4) (("" (REVEAL -1) (("" (EXPAND "headROBEcorrectVal") (("" (EXPAND "retiredOperandsMatchRF") (("" (EXPAND "opsMatchROB") (("" (EXPAND "completedROBEcorrectVal") (("" (HIDE -6 -9 -10) (("" (INST? -4) (("" (SIMP) (("" (SPLIT +) (("1" (SIMP) (("1" (HIDE -5) (("1" (CASE "(forall (j:TWO): st(ss(robe(ROB_p!1)(head(ROB_p!1)))(j)) = RETIRED)") (("1" (INST-CP -1 "1") (("1" (INST -1 "2") (("1" (INST-CP -4 "head(ROB_p!1)" "1") (("1" (INST -4 "head(ROB_p!1)" "2") (("1" (SIMP) (("1" (SIMP) NIL))))))))))) ("2" (SKOSIMP*) (("2" (INST? -3) (("2" (SIMP) (("2" (EXPAND "preceed") (("2" (PROPAX) NIL))))))))))))))) ("2" (SIMP) NIL))))))))))))))))))))))))))))))))))))) (|intBrMatch_issue| "" (EXP-INV-ISSUE) (("1" (INST?) (("1" (SPLIT-ALL) NIL))) ("2" (INST?) (("2" (NEW-SPLIT-IF) (("2" (SPLIT-ALL) NIL))))))) (|intBrMatch_writeb| "" (SKOSIMP*) (("" (LEMMA "writeb_prop") (("" (INST?) (("" (SIMP) (("" (HIDE -2 -3 -4 -5 -6) (("" (REVEAL -1 -2 -3 -4 -5) (("" (EXP-INV-WRITEB :SPLIT F :EXPOCC F) (("" (INST? -3) (("" (INST? -5) (("" (SIMP) (("" (SPLIT-IF-SIMP) (("1" (SPLIT +) (("1" (SKOSIMP*) (("1" (HIDE -1 -2) (("1" (EXPAND "wb_prop") (("1" (EXPAND "chosenFUunique") (("1" (INSTBEST) (("1" (SIMP) (("1" (INST -11 "FU!1") (("1" (REPLACE -2) (("1" (REPLACE -11) (("1" (HIDE -10) (("1" (APPLY (THEN (REPLACE*) (SIMP))) (("1" (INST?) (("1" (INST?) (("1" (SPLIT-ALL) NIL))))))))))))))))))))))))))) ("2" (SIMP) NIL))) ("2" (REPLACE 1) (("2" (HIDE -1 -2) (("2" (GROUND) NIL))))))))))))))))))))))))))) (|intBrMatch_retire| "" (EXP-INV-RETIRE :SPLIT F) (("" (INST -2 "rb!1") (("" (SPLIT-ALL -) NIL))))) (|robeMatchesBr_issue| "" (EXP-INV-ISSUE :SPLIT F) (("" (CASE "Sn!1 > 0") (("1" (SIMP) (("1" (CASE "oc(robe(ROB!1)(rb!1))") (("1" (INST?) (("1" (SIMP) (("1" (INST -11 "succ(rb!1)") (("1" (INST-CP -12 "succ(rb!1)") (("1" (INST -12 "rb!1") (("1" (EXPAND "succ") (("1" (SPLIT-ALL) (("1" (GROUND) NIL) ("2" (GROUND) NIL) ("3" (GROUND) NIL) ("4" (GROUND) NIL))))))))))))))) ("2" (INST-CP -10 "rb!1") (("2" (SPLIT-ALL) (("1" (INST?) (("1" (INST?) (("1" (INST?) (("1" (SIMP) NIL))))))) ("2" (INST?) (("2" (INST?) (("2" (INST?) (("2" (SIMP) NIL))))))) ("3" (INST?) (("3" (INST?) NIL))) ("4" (INST?) (("4" (INST?) NIL))) ("5" (CLEAN-UP) (("5" (INST?) (("5" (INST?) (("5" (INST?) (("5" (SIMP) NIL))))))))) ("6" (INST?) (("6" (INST?) (("6" (INST?) (("6" (SIMP) NIL))))))) ("7" (INST?) (("7" (INST?) (("7" (INST?) (("7" (SIMP) NIL))))))) ("8" (INST?) (("8" (INST?) (("8" (INST?) (("8" (SIMP) NIL))))))) ("9" (INST?) (("9" (INST?) NIL))) ("10" (INST?) (("10" (SIMP) (("10" (INST?) NIL))))))))))))) ("2" (REPLACE 1) (("2" (SIMP) (("2" (INST?) (("2" (SIMP) NIL))))))))))) (|robeMatchesBr_writeb| "" (EXP-INV-WRITEB :SPLIT F) (("" (INST? -3) (("" (SPLIT-ALL) NIL))))) (|robeMatchesBr_retire| "" (EXP-INV-RETIRE :SPLIT F) (("" (INST -2 "rb!1") (("" (SPLIT-ALL) NIL))))) (|AllInvariants_theta| "" (SKOSIMP*) (("" (EXPAND "Theta") (("" (EXPAND "AllInvariants") (("" (SPLIT +) (("1" (GRIND-BEST) NIL) ("2" (GRIND-BEST) NIL) ("3" (GRIND-BEST) NIL) ("4" (GRIND-BEST) NIL) ("5" (GRIND-BEST) NIL) ("6" (EXPAND "busyRAT") (("6" (SKOSIMP*) (("6" (INST?) (("6" (INST?) (("6" (SIMP) NIL))))))))) ("7" (GRIND-BEST) NIL) ("8" (GRIND-BEST) NIL) ("9" (GRIND-BEST) NIL) ("10" (GRIND-BEST) NIL) ("11" (GRIND-BEST) NIL) ("12" (GRIND-BEST) NIL) ("13" (GRIND-BEST) NIL) ("14" (GRIND-BEST) NIL) ("15" (GRIND-BEST) NIL) ("16" (GRIND-BEST) NIL) ("17" (GRIND-BEST) NIL) ("18" (GRIND-BEST) NIL) ("19" (GRIND-BEST) NIL) ("20" (GRIND-BEST) NIL) ("21" (GRIND-BEST) NIL) ("22" (GRIND-BEST) NIL) ("23" (GRIND-BEST) NIL))))))))) (|AllInvariants_issue| "" (EXPAND "AllInvariants") (("" (SKOSIMP*) (("" (LEMMA "wrapWraps_issue") (("" (LEMMA "headTailEq_issue") (("" (LEMMA "occTailROBfull") (("" (INST?) (("" (INST?) (("" (INST?) (("" (SIMP) (("" (LEMMA "occTailROBfull") (("" (INST? :WHERE +) (("" (SIMP) (("" (LEMMA "occEqual_issue") (("" (LEMMA "freeHeadROBempty_issue") (("" (LEMMA "busyRAT_issue") (("" (INST?) (("" (INST?) (("" (INST?) (("" (SIMP) (("" (LEMMA "occBuffBusyRAT_issue") (("" (LEMMA "RATpointsNewestBuff_issue") (("" (LEMMA "occRS_issue") (("" (LEMMA "slotUnique_issue") (("" (LEMMA "occRSops_issue") (("" (INST?) (("" (INST?) (("" (INST?) (("" (INST?) (("" (INST?) (("" (SIMP) (("" (LEMMA "RS_ROB_opsEqual_issue") (("" (LEMMA "busyROBoccRS_issue") (("" (LEMMA "opsMatchROB_issue") (("" (INST?) (("" (INST?) (("" (INST?) (("" (SIMP) (("" (LEMMA "busyOperandsNearest_issue") (("" (LEMMA "writeBoperandsNearest_issue") (("" (LEMMA "retiredOperandsMatchRF_issue") (("" (INST?) (("" (INST?) (("" (INST?) (("" (SIMP) (("" (LEMMA "busyOpBusyROB_issue") (("" (LEMMA "numOcc_issue") (("" (LEMMA "robeMatchesProg_issue") (("" (LEMMA "completedROBEcorrectVal_issue") (("" (LEMMA "headROBEcorrectVal_issue") (("" (LEMMA "intBrMatch_issue") (("" (LEMMA "robeMatchesBr_issue") (("" (INST?) (("" (INST?) (("" (INST?) (("" (INST?) (("" (INST?) (("" (INST?) (("" (INST?) (("" (SIMP) NIL))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (|AllInvariants_writeb| "" (EXPAND "AllInvariants") (("" (SKOSIMP*) (("" (LEMMA "wrapWraps_writeb") (("" (LEMMA "headTailEq_writeb") (("" (LEMMA "occTailROBfull") (("" (INST?) (("" (INST?) (("" (INST?) (("" (SIMP) (("" (LEMMA "occTailROBfull") (("" (INST? :WHERE +) (("" (SIMP) (("" (LEMMA "occEqual_writeb") (("" (LEMMA "freeHeadROBempty_writeb") (("" (LEMMA "busyRAT_writeb") (("" (INST?) (("" (INST?) (("" (INST?) (("" (SIMP) (("" (LEMMA "occBuffBusyRAT_writeb") (("" (LEMMA "RATpointsNewestBuff_writeb") (("" (LEMMA "occRS_writeb") (("" (LEMMA "slotUnique_writeb") (("" (LEMMA "occRSops_writeb") (("" (INST?) (("" (INST?) (("" (INST?) (("" (INST?) (("" (INST?) (("" (SIMP) (("" (LEMMA "RS_ROB_opsEqual_writeb") (("" (LEMMA "busyROBoccRS_writeb") (("" (LEMMA "opsMatchROB_writeb") (("" (INST?) (("" (INST?) (("" (INST?) (("" (SIMP) (("" (LEMMA "busyOperandsNearest_writeb") (("" (LEMMA "writeBoperandsNearest_writeb") (("" (LEMMA "retiredOperandsMatchRF_writeb") (("" (INST?) (("" (INST?) (("" (INST?) (("" (SIMP) (("" (LEMMA "busyOpBusyROB_writeb") (("" (LEMMA "numOcc_writeb") (("" (LEMMA "robeMatchesProg_writeb") (("" (LEMMA "completedROBEcorrectVal_writeb") (("" (LEMMA "headROBEcorrectVal_writeb") (("" (LEMMA "intBrMatch_writeb") (("" (LEMMA "robeMatchesBr_writeb") (("" (INST?) (("" (INST?) (("" (INST?) (("" (INST?) (("" (INST?) (("" (INST?) (("" (INST?) (("" (SIMP) NIL))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (|AllInvariants_retire| "" (EXPAND "AllInvariants") (("" (SKOSIMP*) (("" (LEMMA "wrapWraps_retire") (("" (LEMMA "headTailEq_retire") (("" (LEMMA "occTailROBfull") (("" (INST?) (("" (INST?) (("" (INST?) (("" (SIMP) (("" (LEMMA "occTailROBfull") (("" (INST? :WHERE +) (("" (SIMP) (("" (LEMMA "occEqual_retire") (("" (LEMMA "freeHeadROBempty_retire") (("" (LEMMA "busyRAT_retire") (("" (INST?) (("" (INST?) (("" (INST?) (("" (SIMP) (("" (LEMMA "occBuffBusyRAT_retire") (("" (LEMMA "RATpointsNewestBuff_retire") (("" (LEMMA "occRS_retire") (("" (LEMMA "slotUnique_retire") (("" (LEMMA "occRSops_retire") (("" (INST?) (("" (INST?) (("" (INST?) (("" (INST?) (("" (INST?) (("" (SIMP) (("" (LEMMA "RS_ROB_opsEqual_retire") (("" (LEMMA "busyROBoccRS_retire") (("" (LEMMA "opsMatchROB_retire") (("" (INST?) (("" (INST?) (("" (INST?) (("" (SIMP) (("" (LEMMA "busyOperandsNearest_retire") (("" (LEMMA "writeBoperandsNearest_retire") (("" (LEMMA "retiredOperandsMatchRF_retire") (("" (INST?) (("" (INST?) (("" (INST?) (("" (SIMP) (("" (LEMMA "busyOpBusyROB_retire") (("" (LEMMA "numOcc_retire") (("" (LEMMA "robeMatchesProg_retire") (("" (LEMMA "completedROBEcorrectVal_retire") (("" (LEMMA "headROBEcorrectVal_retire") (("" (LEMMA "intBrMatch_retire") (("" (LEMMA "robeMatchesBr_retire") (("" (INST?) (("" (INST?) (("" (INST?) (("" (INST?) (("" (INST?) (("" (INST?) (("" (INST?) (("" (SIMP) NIL)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) $$$Refine.pvs Refine[R, U, Z: posnat, (IMPORTING more_nat_types[1]) B: greater_one_nat]: THEORY % The proof that Spec (DES) refines seq according to the refinement rule of the paper. BEGIN IMPORTING Invs3[R, U, Z, B], seq[R] reg, reg_p: VAR [REG_ID -> VALUE] RF, RF_p: VAR [REG_ID -> RF_TYPE] RAT, RAT_p: VAR [REG_ID -> RAT_TYPE] ROB, ROB_p: VAR ROB_TYPE RS, RS_p: VAR [SLOT_ID -> RS_TYPE] res, res_p: VAR [FU_ID -> result_TYPE] pca, pca_p, pc, pc_p: VAR posnat numinst, numinst_p, numinsta, numinsta_p: VAR nat FU: VAR FU_ID S, S2: VAR SLOT_ID r: VAR REG_ID rb, rb2: VAR ROB_ID extintdelay: VAR bool obsType: TYPE = [# registers: [REG_ID -> VALUE], numinst: nat, pc: posnat #] rhostar(reg, pca, numinsta, pc, ROB, numinst, reg_p, pca_p, numinsta_p, pc_p, numinst_p): boolean = IF numinst /= numinst_p THEN IF int_interrupt(pca, numinsta + 1) THEN pca_p = Int_interrupt_addr(pca, type_op(op(prog(pca)))) AND reg_p = reg AND numinsta_p = numinsta + 1 ELSE pca_p = IF type_op(op(prog(pca))) = BRANCH AND branch_act(pca, numinsta + 1) THEN br_target(prog(pca)) ELSE pca + 1 ENDIF AND reg_p = (LAMBDA r: IF r = t(prog(pca)) THEN IF type_op(op(prog(pca))) = BRANCH THEN IF branch_act(pca, numinsta + 1) THEN 1 ELSE 0 ENDIF ELSE do_op(op(prog(pca)), reg(src(prog(pca))(1)), reg(src(prog(pca))(2))) ENDIF ELSE reg(r) ENDIF) AND numinsta_p = numinsta + 1 ENDIF ELSE pca_p = pca AND reg_p = reg AND numinsta_p = numinsta ENDIF reg_I(RF): [REG_ID -> VALUE] = (LAMBDA r: 0) rho_c(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p, res): boolean = rho_issue(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p) OR rho_writeb(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p, res) OR rho_retire(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p) OC(pc, RF, ROB, numinst): obsType = (# registers := (LAMBDA r: v(RF(r))), numinst := numinst, pc := IF NOT (head(ROB) = tail(ROB) AND NOT wrap(ROB)) THEN pc(robe(ROB)(head(ROB))) ELSE pc ENDIF #) OA(reg, pca, numinsta): obsType = (# registers := reg, numinst := numinsta, pc := pca #) alpha(pc, RF, RS, RAT, ROB, numinst, reg, pca, numinsta): bool = OC(pc, RF, ROB, numinst) = OA(reg, pca, numinsta) R1: LEMMA rho_c(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p, res) IMPLIES (EXISTS (reg_p, pca_p, numinsta_p): rhostar(reg, pca, numinsta, pc, ROB, numinst, reg_p, pca_p, numinsta_p, pc_p, numinst_p)) R2: LEMMA rhostar(reg, pca, numinsta, pc, ROB, numinst, reg_p, pca_p, numinsta_p, pc_p, numinst_p) IMPLIES seq.rho(pca, reg, numinsta, pca_p, reg_p, numinsta_p) R3_theta: LEMMA seq.THETA(pca, reg, numinsta) AND Spec.Theta(pc, RF, RS, RAT, ROB, numinst) IMPLIES alpha(pc, RF, RS, RAT, ROB, numinst, reg, pca, numinsta) R3_issue: LEMMA rho_issue(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p) AND rhostar(reg, pca, numinsta, pc, ROB, numinst, reg_p, pca_p, numinsta_p, pc_p, numinst_p) AND wrapWraps(ROB) AND alpha(pc, RF, RS, RAT, ROB, numinst, reg, pca, numinsta) IMPLIES alpha(pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p, reg_p, pca_p, numinsta_p) R3_writeb: LEMMA rho_writeb(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p, res) AND rhostar(reg, pca, numinsta, pc, ROB, numinst, reg_p, pca_p, numinsta_p, pc_p, numinst_p) AND alpha(pc, RF, RS, RAT, ROB, numinst, reg, pca, numinsta) IMPLIES alpha(pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p, reg_p, pca_p, numinsta_p) R3_retire: LEMMA rho_retire(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p) AND rhostar(reg, pca, numinsta, pc, ROB, numinst, reg_p, pca_p, numinsta_p, pc_p, numinst_p) AND headROBEcorrectVal(RF, ROB, numinst) AND robeMatchesProg(ROB, numinst) AND intBrMatch(ROB, numinst) AND robeMatchesBr(ROB, numinst, pc) AND occTailROBfull(ROB) AND wrapWraps(ROB) AND headTailEq(ROB) AND freeHeadROBempty(ROB) AND occEqual(ROB) AND alpha(pc, RF, RS, RAT, ROB, numinst, reg, pca, numinsta) IMPLIES alpha(pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p, reg_p, pca_p, numinsta_p) R3_rho: LEMMA rho_c(pc, RF, RS, RAT, ROB, numinst, pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p, res) AND rhostar(reg, pca, numinsta, pc, ROB, numinst, reg_p, pca_p, numinsta_p, pc_p, numinst_p) AND AllInvariants(RF, RS, RAT, ROB, numinst, pc) AND alpha(pc, RF, RS, RAT, ROB, numinst, reg, pca, numinsta) IMPLIES alpha(pc_p, RF_p, RS_p, RAT_p, ROB_p, numinst_p, reg_p, pca_p, numinsta_p) R4: LEMMA alpha(pc, RF, RS, RAT, ROB, numinst, reg, pca, numinsta) IMPLIES OC(pc, RF, ROB, numinst) = OA(reg, pca, numinsta) END Refine $$$Refine.prf (|Refine| (|rhostar_TCC1| "" (SUBTYPE-TCC) NIL) (|rhostar_TCC2| "" (SUBTYPE-TCC) NIL) (R1 "" (SKOSIMP*) (("" (CASE "numinst!1 = numinst_p!1") (("1" (INST 1 "reg!1" "pca!1" "numinsta!1") (("1" (GRIND) NIL))) ("2" (CASE "int_interrupt(pca!1, numinsta!1+1)") (("1" (INST 2 "reg!1" "Int_interrupt_addr(pca!1, type_op(op(prog(pca!1))))" "numinsta!1 + 1") (("1" (GRIND) NIL))) ("2" (INST 3 "(LAMBDA r: IF r = t(prog(pca!1)) THEN IF type_op(op(prog(pca!1))) = BRANCH THEN IF branch_act(pca!1, numinsta!1 + 1) THEN 1 ELSE 0 ENDIF ELSE do_op(op(prog(pca!1)), reg!1(src(prog(pca!1))(1)), reg!1(src(prog(pca!1))(2))) ENDIF ELSE reg!1(r) ENDIF)" "IF type_op(op(prog(pca!1))) = BRANCH AND branch_act(pca!1, numinsta!1+1) THEN br_target(prog(pca!1)) ELSE pca!1 + 1 ENDIF" "numinsta!1 + 1") (("2" (GRIND) NIL))))))))) (R2 "" (EXPAND "rhostar") (("" (EXPAND "rho") (("" (SKOSIMP*) (("" (SPLIT-ALL -) (("1" (INST 2 "false") (("1" (SIMP) NIL))) ("2" (INST 3 "false ") (("2" (SIMP) NIL))) ("3" (INST 1 "true") (("3" (SIMP) NIL))) ("4" (INST 3 "false") (("4" (SIMP) NIL))) ("5" (INST 4 "false") (("5" (SIMP) (("5" (SPLIT-ALL) (("5" (APPLY-EXTENSIONALITY 2 :HIDE? T) (("5" (SPLIT-ALL) NIL))))))))) ("6" (INST 2 "true") (("6" (SIMP) NIL))))))))))) (|R3_theta| "" (EXPAND "THETA") (("" (EXPAND "Theta") (("" (EXPAND "alpha") (("" (EXPAND "OC") (("" (EXPAND "OA") (("" (SKOSIMP*) (("" (SIMP) (("" (APPLY-EXTENSIONALITY 2 :HIDE? T) (("" (GRIND) NIL))))))))))))))))) (|R3_issue| "" (EXPAND "rhostar") (("" (EXPAND "alpha") (("" (EXPAND "OC") (("" (EXPAND "OA") (("" (EXP-INV-ISSUE) (("" (SPLIT-ALL) NIL))))))))))) (|R3_writeb| "" (EXPAND "rhostar") (("" (EXPAND "alpha") (("" (EXPAND "OC") (("" (EXPAND "OA") (("" (EXP-INV-WRITEB) (("" (SPLIT-ALL -) NIL))))))))))) (|R3_retire| "" (EXPAND "rhostar") (("" (EXPAND "alpha") (("" (EXPAND "OC") (("" (EXPAND "OA") (("" (SKOSIMP*) (("" (EXP-INV-RETIRE :SPLIT F) (("1" (INST-CP -4 "head(ROB!1)" "1") (("1" (INST -4 "head(ROB!1)" "2") (("1" (INST?) (("1" (INST?) (("1" (CASE "retire!1") (("1" (CASE "not oc(robe(ROB!1)(head(ROB!1)))") (("1" (SIMP) (("1" (SIMP) (("1" (INST?) NIL))))) ("2" (CASE "b(robe(ROB!1)(head(ROB!1)))") (("1" (SIMP) NIL) ("2" (SIMP) (("2" (EXPAND "EXOR") (("2" (CLEAN-UP) (("2" (SPLIT -5) (("1" (SIMP) (("1" (REPLACE*) (("1" (APPLY (THEN (SPLIT 5) (APPLY-EXTENSIONALITY 1 :HIDE? T) (SPLIT-ALL))) NIL))))) ("2" (SIMP) (("2" (REPLACE*) (("2" (APPLY (THEN (SPLIT 6) (APPLY-EXTENSIONALITY 1 :HIDE? T) (SIMP))) (("1" (SPLIT-IF-SIMP -8) (("1" (SPLIT-IF-SIMP -) (("1" (CLEAN-UP) (("1" (SPLIT-ALL) (("1" (NEW-SPLIT-IF -32) (("1" (REPLACE -31 :DIR RL) (("1" (SIMP) NIL))))) ("2" (REPLACE -28 :DIR RL) (("2" (SIMP) NIL))))))) ("2" (REPLACE -31 :DIR RL :HIDE? T) (("2" (NEW-SPLIT-IF -32) NIL))))) ("2" (REPLACE -28 :DIR RL :HIDE? T) (("2" (NEW-SPLIT-IF -29) (("2" (SPLIT-ALL) NIL))))))) ("2" (NEW-SPLIT-IF -30) (("2" (NEW-SPLIT-IF -27) (("1" (INST -2 "succ(head(ROB!1))") (("1" (EXPAND "succ") (("1" (SPLIT-ALL) NIL))))) ("2" (INST -1 "succ(head(ROB!1))") (("2" (EXPAND "succ") (("2" (SPLIT-ALL) NIL))))))))))))))))))))))))))) ("2" (SIMP) (("2" (CLEAN-UP) (("2" (REPLACE*) (("2" (SIMP) NIL))))))))))))))))) ("2" (INST-CP -7 "head(ROB!1)" "1") (("2" (INST -7 "head(ROB!1)" "2") (("2" (INST?) (("2" (INST?) (("2" (CASE "not oc(robe(ROB!1)(head(ROB!1)))") (("1" (SIMP) (("1" (SIMP) (("1" (INST?) NIL))))) ("2" (SIMP) (("2" (CLEAN-UP) (("2" (NEW-SPLIT-IF -6) (("1" (REPLACE -30 :DIR RL :HIDE? T) (("1" (NEW-SPLIT-IF -) (("1" (SPLIT-ALL) NIL) ("2" (SPLIT-ALL) (("1" (NEW-SPLIT-IF -33) NIL) ("2" (NEW-SPLIT-IF -32) NIL))))))) ("2" (REPLACE -28 :DIR RL :HIDE? T) (("2" (NEW-SPLIT-IF -) (("1" (NEW-SPLIT-IF -32) NIL) ("2" (NEW-SPLIT-IF -31) (("2" (REVEAL -7) (("2" (SIMP) (("2" (EXPAND "EXOR") (("2" (SIMP) NIL))))))))))))))))))))))))))))))))))))))))) (|R3_rho| "" (SKOSIMP*) (("" (EXPAND "rho_c") (("" (SPLIT -) (("1" (LEMMA "AllInvariants_issue") (("1" (LEMMA "R3_issue") (("1" (INST?) (("1" (INST?) (("1" (INST?) (("1" (SIMP) (("1" (EXPAND "AllInvariants") (("1" (PROPAX) NIL))))))))))))))) ("2" (SIMP) (("2" (LEMMA "AllInvariants_writeb") (("2" (LEMMA "R3_writeb") (("2" (INST?) (("2" (INST?) (("2" (INST?) (("2" (SIMP) NIL))))))))))))) ("3" (LEMMA "AllInvariants_retire") (("3" (LEMMA "R3_retire") (("3" (INST?) (("3" (INST?) (("3" (INST?) (("3" (SIMP) (("3" (EXPAND "AllInvariants") (("3" (SIMP) NIL))))))))))))))))))))) (R4 "" (SKOSIMP*) (("" (EXPAND "alpha") (("" (PROPAX) NIL)))))) $$$more_nat_types.pvs more_nat_types[m: posnat]: THEORY BEGIN upto_nz : TYPE = {i: upto[m] | NOT i = 0} CONTAINING m greater_one_nat : TYPE = {i : posnat | NOT i = 1} containing 2 END more_nat_types $$$more_nat_types.prf (|more_nat_types| (|upto_nz_TCC1| "" (SUBTYPE-TCC) NIL) (|upto_nz_TCC2| "" (SUBTYPE-TCC) NIL) (|greater_one_nat_TCC1| "" (SUBTYPE-TCC) NIL))