Automating Hazard Checking in Transaction-Level Microarchitecture Models

Traditional hardware modeling using RTL presents a time-stationary view of the design state space which can be used to specify temporal properties for model checking. However, highlevel information in terms of computation being performed on units of data (transactions) is not directly available. In contrast, transaction-level microarchitecture models view the computation as sequences of (data-stationary) transactions. This makes it easy to specify properties which involve both transaction sequencing and temporal ordering (e.g. data hazards). In RTL models, additional book-keeping state must be manually introduced in order to specify and check these properties. We show here that a transaction-level microarchitecture model can help automate checks for such properties via the automated creation of the book-keeping structures, and illustrate this for a simple pipeline using SMV. A key challenge in model-checking the transactionlevel microarchitecture is representing the dynamic transaction state space. We describe an encoding as well as a fixed point computation for this.