Learning from Constraints for Formal Property Checking

Constraints are commonly used in both simulation and formal verification in order to specify expected input conditions and state transitions. Constraint solving is a process to determine input vectors which satisfy the set of constraints during constrained random simulation. Even though constraints are used in formal property checking to restrict the search space, constraint solving has never had direct application to formal property checking. There are often many simple, yet powerful, invariants that can be learned from constraint solving during constrained random simulation. These invariants are shown in this paper to significantly simplify the formal verification problem. We use approximate constraint solving to compute an approximate set of valid input vectors. The approximate set of valid input vectors are a strict superset of the set of all legal input vectors. We use BDD techniques to compute these input vectors during constrained random simulation, then process the resulting BDDs for learning invariants which can be used during formal property checking. This paper presents efficient BDD algorithms to learn invariants from the BDDs generated from approximate constraint solving. We also present how these learned invariants can be applied to the formal property checking. Experimental results show that invariants learned during constraint solving can significantly improve the performance of formal property checking with many industrial designs.