Rechnergestütztes Beweisen (Hofmann, WS 2005/06)

2005-12-22 VL 20

Out-of-order execution
======================

ALU

Inputs: op1, op2, dest, opcode, stall

Ist stall gesetzt, wird opcode als NOP interpretiert.

Sei dest(t), op1(t), op2(t), opcode(t) die zur Zeit t anliegende
Eingabe.

Intention: Zur Zeit t+2 gilt
 
  reg(dest(t)) = opcode(t)(reg(op1(t)),reg(op2(t)))

Zur Zeit t werden reg(op1(t)) und reg(op2(t)) in opreg1 und opreg2
geschrieben. 

Zur Zeit t+1 wird das Ergebnis in wbreg geschrieben.
Zur Zeit t+2 wird wbreg nach reg(dest(t)) geschrieben.

Stimmen opj(t+i) und dest(t) überein (i=1,2), so muss das Ergebnis
direkt in opregj geschrieben werden.


Modellierung in PVS:
--------------------

Zeit            : nat
Einzelne Leitung: [nat -> bit]
Eingabe         : Funktionskonstante (unimplementiert)

Interne Leitung/Ausgabe: 

a) entweder: implementierte Fkt

  Bsp.:   stall   : [nat->bit]
          stall_d0:bit
          stall_d(n):bit = IF n=0 THEN stall_d0 ELSE stall(n-1) ENDIF

  Vorteil: rewriting besser möglich, Tests möglich
  Nachteil: Neigt dazu, Implementierungsdetails vorwegzunehmen.

b) oder: unspezifizierte Fkt + Axiome

  Bsp.:  stall,stall_d : [nat->bit]
         stall_d_def : AXIOM = FORALL (t:nat):stall(t)=stall_d(t+1)

Komplexere Daten wie Adressen, Registerinhalte, Opcodes, werden als
unspezifierte Typen modelliert.  Funktion der ALU wird als
unspezifierte Funktion 

  aluop : [opcode,data,data -> data]

modelliert.


pipe_rec[addr,data,opcodes:NONEMPTY_TYPE]: THEORY
 

Funktionaler Update:

beh(t-1)`regfile WITH [(beh(t-1)`dstndd) := beh(t-1)`wbreg ]

Falls x Rekordtyp hat, z.B. x : [# f1:t1, f2:t2 #], und y:t1
dann  

  x WITH [f1 := y] : [# f1:t1, f2:t2 #]

(x WITH [f1 := y])`f1 = y
(x WITH [f1 := y])`f2 = x`f2

Falls f : [t1->t2] und v:t1, w:t2

f WITH [v := w] : [t1 -> t2]

(f WITH [v := w])(x) = IF x=v THEN w ELSE f(x) ENDIF