404def sm86FixedLatencyHazard =
405 (lambda unrestricted program : (family SM86Program) .
406 (app (app (app
407 (eliminate SM86Program
408 (lambda unrestricted current : (family SM86Program) .
409 (pi unrestricted ordinal : Nat . (pi unrestricted now : Nat . (pi unrestricted pending : (family ScoreboardPending) . Nat))))
410 program
411 (branch SM86ProgramEnd .
412 (lambda unrestricted ordinal : Nat . (lambda unrestricted now : Nat . (lambda unrestricted pending : (family ScoreboardPending) . zero))))
413 (branch SM86ProgramNext instruction tail induction .
414 (lambda unrestricted ordinal : Nat . (lambda unrestricted now : Nat . (lambda unrestricted pending : (family ScoreboardPending) .
415 (eliminate SM86OpSummary
416 (lambda unrestricted current : (family SM86OpSummary) . Nat)
417 (sm86OpSummaryOfBody (sm86InstructionBodyOf instruction))
418 (branch SM86OpSummaryValue readsBody writesBody predicateWrites waitKeys setKeys stall latency variable minimum control .
419 (let unrestricted reads =
420 (stdListAppend Nat readsBody (stdListAppend Nat (sm86GuardKeys instruction) waitKeys))
421 in (let unrestricted writes = (stdListAppend Nat writesBody predicateWrites)
422 in (let unrestricted issued =
423 (flIssue setKeys (naturalAdd now sm86BarrierSetCycles) (flPrune pending now))
424 in (nat-eliminate
425 (lambda unrestricted current : Nat . Nat)
426 (induction (succ ordinal)
427 (naturalAdd now (naturalSelect (naturalNonzero stall) stall 1))
428 (nat-eliminate
429 (lambda unrestricted current : Nat . (family ScoreboardPending))
430 issued
431 (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : (family ScoreboardPending) .
432 (flIssue writes (naturalAdd now latency) issued)))
433 latency))
434 (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Nat . ordinal))
435 (naturalOr (naturalLess (naturalSelect (naturalNonzero stall) stall 1) minimum)
436 (naturalOr (flLate pending reads now) (flLate pending writes now))))))))))))))
437 1) 0) (constructor ScoreboardPending ScoreboardPendingEnd)))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.