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, high-level 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.