Abstraction as a Practical Debugging Tool

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.