SAT-Based Scalable Formal Verification Solutions
Description
Functional verification has become an important aspect of the chip design process. Significant resources, both in industry and academia, are devoted to the design complexity and verification endeavors.
SAT-Based Scalable Formal Verification Solutions discusses in detail several of the latest and interesting scalable SAT-based techniques including: Hybrid SAT Solver, Customized Bounded/Unbounded Model Checking, Distributed Model Checking, Proofs and Proof-based Abstraction Methods, Verification of Embedded Memory System & Multi-clock Systems, and Synthesis for Verification Paradigm. These techniques have been designed and implemented in a verification platform Verisol (formally called DiVer) and have been used successfully in industry. This book provides algorithmic details and engineering insights into devising scalable approaches for an effective realization. It also includes the authors' practical experiences and recommendations in verifying the large industry designs using VeriSol.
The book is primarily written for researchers, scientists, and verification engineers who would like to gain an in-depth understanding of scalable SAT-based verification techniques. The book will also be of interest for CAD tool developers who would like to incorporate various SAT-based advanced techniques in their products.
More details
Other editions
Additional editions
Content
5 SAT-BASED BOUNDED MODEL CHECKING (p. 79-80)
5.1 Introduction
Bounded Model Checking (BMC) has been gaining ground as a falsification engine, mainly due to its improved scalability compared to other formal techniques. In BMC, the focus is on finding counterexamples (bugs) of a bounded length k. For a given design and correctness property, the problem is translated effectively to a propositional formula such that the formula is true if and only if a counterexample of length k exists [66, 67]. Such a translation basically involves unrolling the circuit of the transition relation for the required number of time frames as illustrated in Figure 5.1 (with k=d). Essentially, d copies of circuit are made and then clauses are built at each time frame for the unrolled circuit and the property to be reasoning is needed to ensure completeness when no counterexample can be found up to a certain bound [66, 67]. However, with increasing depth the problem size, comprising the unrolled circuit and translated property, grows linearly [111] with the size of the model, thereby the making the Boolean reasoning increasingly difficult for large bounds, in general. The standard translation for these properties is monolithic, i.e., the entire propositional formula is generated for a given k and then the formula is checked for satisfiability using a standard SAT solver. Such a monolithic translation provides little scope for an incremental formulation within a k-instance BMC problem. Therefore, the past efforts [153, 154] on incremental learning for BMC have been limited to sharing of constraints across k-instances only.
Outline
In this chapter, we discuss several enhancements proposed in the last few years to make the standard BMC procedure [66, 67] scale with large industry designs. The first key improvement that we discuss is dynamic circuit simplification [45] in Section 5.2. This is performed on the iterative array model of the unrolled transition relation, where an on-the-fly circuit reduction algorithm, discussed in Chapter 3, is applied not only within a single time frame but also across time frames to reduce the associated Boolean formula.
The second key enhancement we discuss is SAT-based incremental learning in Section 5.3. This is used to improve the overall verification time by re-using the SAT results from the previous runs. Next, we discuss a lightweight and goal-directed effective BDD-based learning scheme in Section 5.4, where learned clauses generated by BDDbased analysis are added to the SAT solver on-the-fly, to supplement its other learning mechanisms. We also discuss several heuristics for guiding the SAT search process to improve the performance of the BMC engine.
Based on the above simplification and learning techniques, we discuss the use of customized property translations, in Section 5.5, for commonly occurring LTL formulas such as safety and liveness, with novel features that utilize partitioning, learning, and incremental formulation [46]. Such customized translations allow not only incremental learning across kinstances, but also within k-instances of BMC problems and thereby, greatly improve overall performance. Moreover, in comparison to the standard translation, customized translations provide additional opportunities for deriving completeness bounds for nested properties (this is discussed in more detail in Chapter 10).
