SAT-Based Scalable Formal Verification Solutions

Verification ensures that the design meets the specification and has become an indispensable part of a product development cycle of a digital hardware design. Cost of chip failure is enormous due to high cost of respins and delayed tape-out, resulting in loss of opportunity to launch product on time in a highly competitive market. With the increasing design complexity of digital hardware, functional verification has become increasingly on the critical path of the cycle [1], requiring expensive and time-consuming efforts, as much as 70% of the product development cycle. As per the 2002/2004 functional verification study conducted by Collett International Research (as reported by EETimes.com [2]), functional/logic flaws account for 75% causes for respins of more than two-thirds of IC/ASIC designs to reach volume. Of these 75% flaws, more than 80% are due to design errors and remaining are due to incorrect/incomplete specification, internal and external IPs. Market forces mandate scalable verification solutions and radical shifts in design methodology to overcome the difficulty in verifying complex designs. Not surprisingly, traditional “black-box” verification methodology is giving way to “white-box” verification methodology, where more than half of the engineers in the design team are verification engineers who are getting involved in the early phase of design and specification.

Model checking is a method to verify whether a model obtained from hardware or software system satisfies a formal specification, written as temporal logic formulas such as Linear Time Logic (LTL) [87] or Computational Tree Logic (CTL) [88, 89].

Many traditional tasks in computer-aided design such as equivalence or property checking, logic synthesis, static timing analysis, and automatic testpattern generation require an efficient representation of combinational circuits in terms of a network of Boolean primitives. Many practical problems derived from the above-mentioned applications have a high degree of structural redundancy.

The Boolean Satisfiability (SAT) problem has extensive applications in VLSI CAD. Recent advances in SAT solvers based on Conjunctive Normal Form (CNF) representation have resulted in significantly improved performance. In particular, innovative techniques for decision variable selection [38], Boolean constraint propagation (BCP) [36, 38], and backtracking with conflict analysis based learning [37, 38] have led to highperformance CNF-based SAT solvers like Chaff [38]. For circuit application domains such as Automatic Test Pattern Generation (ATPG) [143], equivalence checking [39], and Bounded Model Checking (BMC) [66], the Boolean reasoning problem is typically derived from the circuit structure. This has also led to interest in circuit-based SAT solvers [39, 143-145], which use circuit specific knowledge to guide the search.

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 checked, which is then fed to a SAT-solver. In practice, the bound k can be increased incrementally to find the shortest counterexample. A separate 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.

Designs with large embedded memories are quite common and have wide application. However, these embedded memories add further complexity to formal verification tasks due to an exponential increase in state space with each additional memory bit. In typical BMC approaches [45, 66, 109, 178], the search space increases with each time-frame unrolling of a design. With explicit modeling of large embedded memories, the search space frequently becomes prohibitively large to analyze beyond a small depth. In order to make BMC more useful, it is important to have some abstraction of these memories. However, for finding real bugs, it is sufficient that the abstraction techniques capture the memory semantics [179] without explicitly modeling each memory bit.

Current System-on-Chip (SoC) designs are essentially multi-clock systems with multiple clock domains, gated clocks, and latches. Further, the intellectual property (IP) blocks building SoC, with their own clock generators, mandate the requirement for synchronous primitives between the resulting asynchronous clock domains. To meet the high performance and low power requirements [183], multi-clock systems have become the norm of current designs, taking over the single global clock synchronous designs. Routing single clock over a large die incurs large skew delays, unacceptable for high-performance designs. With low power stringent requirements, it is difficult to reduce the clock skews for a distributed clock simply by increasing the power of the clock drivers. For power-conscious designs, designers often use gated clocks to reduce or disable the switching activity of certain portions of the design. Each of these design styles increases the verification complexity in terms of increased number of state bits and deeper bug traces. The following design features and specification of clocked systems pose additional challenges to the existing verification efforts.

SAT-based Bounded Model Checking (BMC) [45, 66, 109, 178] has been shown to be more robust and scalable compared to symbolic model checking methods based on Binary Decision Diagrams (BDDs) [12, 17]. Unlike BDD-based methods, BMC focuses on finding bugs of bounded length, successively increasing the bound to search for longer traces. Although BMC can find bugs in larger designs than BDD-based methods, the correctness of a property is guaranteed only for the analysis bound. A completeness bound has been proposed [66, 67, 72], to provide a proof of correctness for safety properties based on the longest loop-free path between states. Unfortunately, the longest loop-free path can be exponentially longer than the reachable diameter of the state space (for example the longest loopfree path for an n-bit counter is 2ⁿ while the reachable diameter is 1). One can use inductive invariants like reachability constraints [73] to obtain proofs earlier than the longest loop-free path. Alternatively, one can obtain a shorter completeness bound, i.e., the longest shortest backward diameter, for BMC using SAT-based fixed-point computations [67], described in the procedure Fixed_point_EF (see Figure 2.10). Such an approach uses cubewise enumeration of SAT solutions, as described in the procedure All_sat (see Figure 2.9), for computing exisitential quantifications.

Verifying modern designs requires robust and scalable approaches in order to meet more demanding time-to-market requirements. We present our SAT-based model checking platform VeriSol [53] based on robust and scalable algorithms (as discussed in Parts I-IV) that are tightly integrated for verifying large scale industry designs. We briefly discuss and analyze the strengths and weaknesses of various verification engines in VeriSol as each addresses the capacity and performance issues inherent in verifying large designs. Using several industry case studies, we describe the interplay of these engines highlighting their contribution at each step of verification. We also discuss the various modeling issues in handling complex features in real designs.

To overcome increasing demand for shorter time-to-market and complex designs, significant efforts are being made in high-level synthesis methodologies, design languages and verification methodologies to leverage the expressive power of high-level models and reduce the design cycle time. However, with progression through each stage in the design cycle from abstraction to realization, part of the high-level information gets lost; which can adversely affect the performance and optimality of the verification solution at that stage.