Abstraction as a Practical Debugging Tool

S. Ray

In M. S. Abadir, L. Wang, and J. Bhadra, editors, Proceedings of the 9th International Workshop on Microprocessor Test and Verification, Common Challenges and Solutions (MTV 2008), Austin, TX, December 2008, pages 45-48. IEEE Computer Society

© 2009 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.


We present a procedure for automatically constructing an abstract state model of a hardware design using the definition of the state transition function for the design and a description of the set of observations to be preserved in the abstraction. The procedure iteratively constructs the abstract model by refining a mapping from the states of the original design to the states of the abstraction. The resulting abstraction is guaranteed to be a conservative approximation of the design. We discuss our implementation of the procedure and different design trade-offs involved in making it effective.

Relevant files