The paper presents a new computational model of Herbrand
engines which combines finite-state control with uninterpreted
data and function registers, thus yielding a finite representation of
infinite-state machines. Herbrand engines are used to provide a
high-level model of out-of-order execution in the design of
micro-processors. The problem of verifying that a highly parallel
design for out-of-order execution correctly implements the Instruction
Set Architecture is reduced to establishing the equivalence of two
Herbrand engines. We show that, for a reasonably restricted class of
such engines, the equivalence problem is decidable, and present two
algorithms for solving this problem.
Ultimately, the appropriate statement of correctness is that the
out-of-order execution produces the same final state (and all relevant
intermediate actions, such as writes to memory) as a purely sequential
machine running the same algorithm.
International Conference on Concurrency Theory