Verifying micro-architecture simulators using event traces

Contemporary micro-architecture research inherently relies on cycle-accurate simulators to test new ideas. Typical simulator implementations involve tens of thousands of lines of high-level code. Although general software engineering verification and validation techniques can be applied, the mere complexity of simulators makes using formal techniques difficult and calls for domain-specific knowledge to be a part of the verification process. This domain-specific information includes modeling the pipeline stages and the timing behavior of instructions with respect to these stages. We present an approach to simulator verification that uses domain-specific information to effectively capture a potential mismatch between the assumed architecture model and its simulator. We first discuss how a simulator-generated event trace can be fed into an automatically generated verification program from a first-order logic specification to verify that the simulator obeys the invariants. We then show techniques that extract simulator behavior from traces and present the results to the user in the form of graphs and rules. While the former seeks an assurance of implementation correctness by checking that the model invariants hold, the latter attempts to derive an extended model of the implementation and hence enables a deeper understanding of what was implemented. Our techniques are applicable to any micro-architecture simulator. We present the application of our techniques to hand-written simulators as well as to those generated from an architecture specification language. © 2014 ACM