Formal Verification of Pipelined Microprocessors
List of Known Errors

White rows denote grammar/spelling/formatting errors, red rows denote content errors, green rows denote content updates and clarifications.

PageLine*/FigureCorrection
13 -1 "{-2n-1,...,2n-1-1}" instead of "{0,...,2n-1}"
23 -5 "[a]<[b]?1:0" instead of "a<b?1:0"
31 -11 "I_branch_eq(I) = (GPRa=0)" instead of "I_branch_eq(I)(GPRa=0)"
31 -1 .GPR[15](c)" instead of "δ.GPR[I_RD(I)](c)"
57 -7 "I_branch_eq(IR) = ..." instead of "I_branch_eq(Iw) ⊕ ..."
61 10 f4GPRwa(IR) = 15 if (I_j(IR)I_jr(IR))I_link(IR), I_RD(IR) otherwise
116 Fig. 4.10 "R1hit[4]" instead of "hit[4]"
227 8 line too long
240 -1 "a generic" instead of "A generic"
242 Fig. 6.1 Alignment of "IF" and "Decode Issue" in their boxes
242 1 "algorithm is..." instead of "algorithms is..."
242 8 Blank between "buffer" and "[SP88]" missing
243 18 "such as IBM's PowerPC" instead of "such as the IBM's PowerPC"
248 9 "with D(i,x)=r and r≠0." instead of "with D(i,x)=r.", i.e., D(i,x)=0 means that destination operand x is not used.
249 -11 "issue_with_result(i)" instread of "issue_with_result(T)"
251 Fig. 6.3
Line 5:"for reservation stations RS[rs] with issue_rs(T, rs)
Line 9-16:"RS[rs]" instead of "RS"
Line 22: Insert
if issue_with_result(i) then
  ROB[ROBtail].valid:=1
  ROB[ROBtail].result:=issue_result(i)
else
  ROB[ROBtail].valid:=0
endif
270 6 "≠ ROBtailT'" instead of "≠ ROBtail(T')"
271 -12 "ROBheadT'" instead of "ROBhead(T')"
271 -8 "ROBheadT'" instead of "ROBhead(T')"
300 -12 "∃ T''' ≥ T: Tout(..." instead of "∃ T''' ≥ Tout(..."
304 Fig. 6.11 dotted line in box of IR.1 has to be moved to the left
309 2 "[KMP99]" instead of "[MPK00]"
309 5 "Parts of the hardware" instead of "The parts of the hardware"
309 12 "Despite of that" instead of "Despite that"
309 * Too much space after "et al."
325 -2, -3 Hex and binary for IR[31:26] inconsistent
* = negative line numbers are counted from the bottom of the page.

Please report errors to kroening@handshake.de.