SM86.Scoreboard

261def scoreboardStep =
262  (lambda unrestricted pending : (family ScoreboardMasks) .
263    (lambda unrestricted pendingReads : (family ScoreboardMasks) .
264    (lambda unrestricted summary : (family SM86OpSummary) .
265      (eliminate SM86OpSummary
266        (lambda unrestricted current : (family SM86OpSummary) . (family ScoreboardStep))
267        summary
268        (branch SM86OpSummaryValue reads writes predicateWrites waitKeys setKeys stall latency variable minimum control .
269          (let unrestricted retired = (sbMasksRetire (scoreboardWaitMaskOf control) pending)
270          in (let unrestricted readsRetired = (sbMasksRetire (scoreboardWaitMaskOf control) pendingReads)
271          in (let unrestricted hazard =
272                (naturalOr
273                  (naturalOr (sbMasksAnyPending retired reads) (sbMasksAnyPending retired writes))
274                  (naturalOr (sbMasksAnyPending readsRetired writes)
275                    (naturalAnd (sbRegistersNonempty reads)
276                      (sbReadBarrierOccupied readsRetired (scoreboardReadBarrierOf control)))))
277          in (let unrestricted declared = (scoreboardWriteBarrierOf control)
278          in (let unrestricted declaredRead = (scoreboardReadBarrierOf control)
279          in (let unrestricted barrier =
280                (nat-eliminate
281                  (lambda unrestricted current : Nat . Nat)
282                  (nat-eliminate
283                    (lambda unrestricted current : Nat . Nat)
284                    zero
285                    (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Nat . scoreboardNever))
286                    variable)
287                  (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Nat . declared))
288                  declared)
289          in
290            (constructor ScoreboardStep ScoreboardStepValue
291              hazard
292              (nat-eliminate
293                (lambda unrestricted current : Nat . (family ScoreboardMasks))
294                retired
295                (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : (family ScoreboardMasks) .
296                  (sbMasksIssue barrier writes retired)))
297                barrier)
298              (nat-eliminate
299                (lambda unrestricted current : Nat . (family ScoreboardMasks))
300                readsRetired
301                (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : (family ScoreboardMasks) .
302                  (sbMasksIssue
303                    (naturalSelect (naturalIsZero declaredRead) scoreboardNever declaredRead)
304                    reads readsRetired)))
305                (naturalAnd (naturalOr variable (naturalNonzero declaredRead))
306                  (sbRegistersNonempty reads)))))))))))))))