Verification of data-insensitive circuits: An in-order-retirement case study

There is a large class of circuits (including pipeline and out-of-order execution components) which can be formally verified while completely ignoring the precise characteristics (e.g. word-size) of the data manipulated by the circuits. In the literature, this is often described as the use of uninterpreted functions, implying that the concrete operations applied to the data are abstracted into unknown and featureless functions. In this paper, we briefly introduce an abstract unifying model for such data-insensitive circuits, and claim that the development of such models, perhaps even a theory of circuit schemas, can significantly contribute to the development of efficient and comprehensive verification algorithms combining deductive as well as enumerative methods.

As a case study, we present in this paper an algorithm for out-of-order execution with in-order retirement and show it to be a refinement of the sequential instruction execution algorithm. Refinement is established by deductively proving (using PVS) that the register files of the out-of-order algorithm and the sequential algorithm agree at all times if the two systems are synchronized at instruction retirement time.

FMCAD'98 Formal Methods in Computer-Aided Design