Utility of transaction-level hardware models in refinement checking

Verifying a cycle-accurate RTL model against its functional specification using refinement checking uses a joint execution model to compare the executions of the two models. Creating and instrumenting such a joint execution model manually can be tedious and error-prone. In this paper, we illustrate the use of transaction-based models (e.g. [1]) in simplifying the process of creating and instrumenting joint execution models for refinement checking. We first show how transaction-based specification and implementation models allow simple refinement relations to be written using model variables and constructs. We then show how a joint encoding of the two models can be generated together with assertions expressing the specified refinement relation. This approach avoids the manual bookkeeping otherwise needed for coordinating the executions of the design and the specification, and exchanging information between the two models. We illustrate the ideas on a toy example.