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 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.