Formal checking of properties in complex systems using abstractions

Only very small designs can be verified currently using property checking due to state-space explosion. Abstractions have been developed to simplify the design in an attempt to address this problem. However, the properties themselves may involve large state spaces, and practical property checking is generally confined to the control behavior. This paper describes an elegant technique for verifying properties of complex designs where the abstraction is applied to both the property and the design, thereby allowing us to verify properties which may deal with the data space. We demonstrate the technique on a processor by checking properties which are intractable using existing model checking techniques