Generating and Model Checking a Hierarchy of Abstract Models

The use of automatic model checking algorithms to verify detailed gate or switch level designs of circuits is very attractive because the method is automatic and such models can accurately capture detailed functional, timing, and even subtle electrical behaviour of circuits. The use of binary decision diagrams has extended by orders of magnitude the size of circuits that can be so verified, but there are still very significant limitations due to the computational complexity of the problem. Verifying abstract versions of the model is attractive to reduce computational costs but this poses the problem of how to build abstractions easily without losing the accuracy of the low-level model. This paper proposes a method of bridging the gap between detailed designs and abstract models,..