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.