Search

Symbolic trajectory evaluation is an industrial-strength formal hardware verification method, based on symbolic simulation, which has been highly successful in data-path verification, especially for microprocessor execution units. It is a ‘model-checking’ method in the basic sense that properties, expressed in a simple temporal logic, are verified by (symbolic) exploration of formal models of sequential circuits. Its defining characteristic is that it operates by symbolic simulation over abstractions of sets of states that only partially delineate the circuit states in the set. These abstract state sets are ordered in a lattice by information content, based on a three-valued domain for values on circuit nodes (true, false, and don’t know). The algorithm operates over families of these abstractions encoded by Boolean formulas, providing a flexible, specification-driven mechanism for partitioned data abstraction. We provide a basic introduction to symbolic trajectory evaluation and its extensions, and some details of how it is deployed in industrial practice. The aim is to get across the essence and value of the method in clear and accessible terms.

The success of Conflict Driven Clause Learning (CDCL) for Boolean satisfiability has inspired adoption in other domains. We present a novel lifting of CDCL to program analysis called Abstract Conflict Driven Learning for Programs (ACDLP). ACDLP alternates between model search, which performs over-approximate deduction with constraint propagation, and conflict analysis, which performs under-approximate abduction with heuristic choice. We instantiate the model search and conflict analysis algorithms to an abstract domain of template polyhedra, strictly generalizing CDCL from the Boolean lattice to a richer lattice structure. Our template polyhedra can express intervals, octagons and restricted polyhedral constraints over program variables. We have implemented ACDLP for automatic bounded safety verification of C programs. We evaluate the performance of our analyser by comparing with CBMC, which uses Boolean CDCL, and Astr´ee, a commercial abstract interpretation tool. We observe two orders of magnitude reduction in the number of decisions, propagations, and conflicts as well as a 1.5x speedup in runtime compared to CBMC. Compared to Astr´ee, ACDLP solves twice as many benchmarks and has much higher precision. This is the first instantiation of CDCL with a template polyhedra abstract domain.