## Herbrand Automata for Hardware Verification

*
W. Damm,
A. Pnueli*,
and S. Ruah
The paper presents the new computational model of *Herbrand
Engines* which combines finite-state control with uninterpreted
data and function registers, thus yielding a finite representation of
infi-nite-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 program.

In R. De Simone and D. Sangiorgi, editors, *Proceedings of the 9th
International Conference on Concurrency * (CONCUR 1998), Lecture
Notes in Computer Science. Springer-Verlag, 1998.

PostScript updated, improved, and extended text.
© 1998 Springer-Verlag.