Exploiting Boolean Satisfiability Solvers for High Performance Bit-Level Model Checking

Digital systems are nowadays ubiquitous and often comprise an extremely high level of complexity. Guaranteeing the correct behavior of such systems has become an ever more pressing need for manufacturers. Correctness of digital systems can be addressed resorting to formal verification techniques such as model checking. A major issue of model checking techniques, however, is scalability. Recent performance advances in Boolean Satisfiability (SAT) solvers, brought about a leap in the scalability of those techniques. SAT-based model checking algorithms, however, still suffer from non-negligible applicability issues when confronted with the complexity of many industrial-scale designs. In this dissertation we present several approaches to improve performance and scalability of SAT-based model checking algorithms, focusing in particular on interpolation and IC3. Each of the presented approaches addresses scalability from a different perspective. The first approach focuses on the interaction between IC3 and the underlying SAT solver. IC3, in fact, proves to be highly sensitive to the way its SAT queries are handled. We propose and compare different strategies for SAT solvers management in IC3. The second approach consists of a novel interpolation-based algorithm that specifically targets the limited flexibility and incrementality of the original interpolation method. The proposed algorithm overcomes such limitations through the use of an incremental data structure for overapproximated reachability as well as techniques to better control the precision of the computed overapproximations. The third approach addresses interpolants compaction, proposing a novel SAT-based technique that relies on proof-based abstraction to achieve considerable compaction rates. Each of the proposed approaches was experimentally evaluated and proved to increase scalability of SAT-based model checking algorithms, in particular when considered in the context of portfolio-based model checking tools