Novel Approaches to Hardware Safety Checking and Certificate Minimization
Ryan Berryhill · TSpace (University of Toronto) · 2020
Verification is an ever-growing challenge in hardware design due to the complexity of modern designs. As a result, formal verification methodologies are seeing rapid adoption in the industry. Formal verification of safety properties is an essential verification task and a key component of algorithms that verify other types of properties. Due to the computational resources required, scalability is a significant concern in this area. Additionally, when a safety property passes verification, safety verification algorithms return only a machine-checkable certificate, which may leave the user with little confidence that the property passes for the “right” reasons rather than, for instance, because the property itself is written incorrectly. This dissertation presents contributions aimed at improving the scalability of formal safety verification algorithms and addressing the lack of feedback from such algorithms. The first contribution is an algorithm called Truss that extends the state-of-the-art safety verification algorithm IC3 with novel heuristics and reasoning capabilities to achieve better runtime performance. Experiments demonstrate a significant speedup relative to the state of the art. The second contribution is a set of techniques to minimize machine-checkable certificates of safety produced by IC3 and similar algorithms. Given such a certificate represented by a Boolean formula, the algorithms find minimal subformulas that are also valid certificates, called minimal safe inductive subformulas (MSISes). Experiments are presented comparing the techniques and demonstrating theireffectiveness. The third contribution is a set of techniques to produce and minimize inductive validity cores (IVCs), which are abstractions of the circuit that are sufficient to prove the given property. Several techniques are presented to compute all minimal IVCs for a safety property and are evaluated experimentally. The final contribution is a set of results related to the computational complexity of the certificate minimization problems noted above. Results are presented showing that two decision problems related to MSIS computation are D P -complete and Σ P2 -complete, respectively, while similar problems for MIVC computation are in PSPACE. The results are also extended to cover a more general class of problems related to finding minimal subsets subject to a monotone predicate (MSMPs).