Speeding up Model Checking by Exploiting Explicit and Hidden Verification Constraints

Constraints represent a key component of state-of-the-art verification tools based on compositional approaches and assume--guarantee reasoning. In recent years, most of the research efforts on verification constraints have focused on defining formats and techniques to encode, or to synthesize, constraints starting from the specification of the design. In this paper, we analyze the impact of constraints on the performance of model checking tools, and we discuss how to effectively exploit them. We also introduce an approach to explicitly derive verification constraints hidden in the design and/or in the property under verification. Such constraints may simply come from true design constraints, embedded within the properties, or may be generated in the general effort to reduce or partition the state space. Experimental results show that, in both cases, we can reap benefits for the overall verification process in several hard-to-solve designs, where we obtain speed-ups of more than one order of magnitude.