Verification is a critical task in the development of correct computing systems. Simulation remains the predominantly used technique to identify design flaws, due to its scalability. However, simulation intrinsically suffers from low functional coverage, hence often fails to identify all design flaws. Formal verification (FV) is a promising approach to overcome the coverage limitations of simulation, due to its exhaustiveness - which enables it to identify intricate design flaws too complex to practically find using simulation. However, automated FV techniques have scalability drawbacks that limit the size of design components that can be formally verified. One of the key strengths of FV techniques is their use of symbolic reasoning, to efficiently explore a huge number of individual scenarios that would be intractable using simulation. When used in an incomplete manner, the scalability challenges of these algorithms are lessened, enabling efficient and relatively scalable semi-formal bug hunting. Nonetheless, to yield a robust industrial-strength solution, the individual components of such a system - many being heuristic - must be highly tuned, and integrated and orchestrated in an intricate manner. In this paper, we overview the various components useful in a scalable semi-formal search framework, introducing several novel powerful techniques and providing experimental data to illustrate the strengths, weaknesses, and complementary nature of the various techniques.

Verification benefits from removing logic that is not relevant for a proof. Techniques for doing this are known as localization abstraction. Abstraction is often performed by selecting a subset of gates to be included in the abstracted model; the signals feeding into this subset become unconstrained cut-points. In this paper, we propose several improvements to substantially increase the scalability of automated abstraction. In particular, we show how a better integration between the BMC engine and the SAT solver is achieved, resulting in a new hybrid abstraction engine, that is faster and uses less memory. This engine speeds up computation by constant propagation and circuit-based structural hashing while collecting UNSAT cores for the intermediate proofs in terms of a subset of the original variables. Experimental results show improvements in the abstraction depth and size.

The ability of logic transformations to enhance safety property checking has been well-established, and many industrial-strength verification solutions accordingly rely upon a variety of synthesis and abstraction techniques for speed and scalability. However, little prior work has addressed the applicability of such transformations in the domain of liveness checking. In this paper, we provide the theoretical foundation to enable the efficient use of a variety of (possibly customized) transformations in a liveness-checking framework. We demonstrate the practical utility of this theory on a variety of complex verification problems.

The process of sequential redundancy identification is the cornerstone of sequential synthesis and equivalence checking frameworks. The scalability of the proof obligations inherent in redundancy identification hinges not only upon the ability to cross-assume those redundancies, but also upon the way in which these assumptions are leveraged. In this paper, we study the technique of speculative reduction for efficiently modeling redundancy assumptions. We provide theoretical and experimental evidence to demonstrate that speculative reduction is fundamental to the scalability of the redundancy identification process under various proof techniques. We also propose several techniques to speed up induction-based redundancy identification. Experiments demonstrate the effectiveness of our techniques in enabling substantially faster redundancy identification, up to six orders of magnitude on large designs.

Sequential equivalence checking (SEC) technologies, capable of demonstrating the behavioral equivalence of two designs, have grown dramatically in capacity over the past decades. The ability to efficiently identify and leverage internal equivalence points to reduce the domain of the overall SEC problem is central to SEC scalability. However, conditionally equivalent designs - within which internal equivalence may not exist under sequential observability don't care conditions - are notoriously difficult for automated SEC tools. This paper constitutes one of the first attempts to advance the scalability of SEC for conditionally equivalent designs through automated invariant generation, which enables an inductive solution to an otherwise highly-noninductive problem. Through careful software engineering and various heuristics, this technique has been demonstrated capable of yielding orders of magnitude speedup on difficult industrial conditional SEC problems, in cases constituting the only method that we have found to achieve an automated solution.

This paper addresses the presence of logic which has relevance only during initial time frames in a hardware design. We examine transient logic in the form of signals which settle to deterministic constants after some prefix number of time frames, as well as primary inputs used to enumerate complex initial states which thereafter become irrelevant. Experience shows that a large percentage of hardware designs (industrial and benchmarks) have such logic, and this creates overhead in the overall verification process. In this paper, we present automated techniques to detect and eliminate such irrelevant logic, enabling verification efficiencies in terms of greater logic reductions, deeper Bounded Model Checking (BMC), and enhanced proof capability using induction and interpolation.

We consider the problem of optimal netlist simplification in the presence of constraints. Because constraints restrict the reachable states of a netlist, they may enhance logic minimization techniques such as redundant gate elimination which generally benefit from unreachability invariants. However, optimizing the logic appearing in a constraint definition may weaken its state-restriction capability, hence prior solutions have resorted to suboptimally neglecting certain valid optimization opportunities. We develop the theoretical foundation, and corresponding efficient implementation, to enable the optimal simplification of netlists with constraints. Experiments confirm that our techniques enable a significantly greater degree of redundant gate elimination than prior approaches (often greater than 2x), which has been key to the automated solution of various difficult verification problems.

This work presents a technology-independent synthesis optimization that is effective in reducing the total number of state elements of a design. It works by identifying and eliminating dependent state elements which may be expressed as functions of other registers. For scalability, we rely exclusively on SAT- based analysis in this process. To enable optimal identification of all dependent state elements, we integrate an inductive invariant generation framework. We introduce numerous techniques to heuristically enhance the reduction potential of our method, and experiments confirm that our approach is scalable and is able to reduce state element count by 12% on average in large industrial designs, even after other aggressive optimizations such as min- register retiming have been applied. The method is effective in simplifying later verification efforts.

The concept of applying partial fencing to logic built-in self test (LBIST) hardware structures for the purpose of using partially good chips is well known in the chip design industry. Deceptively difficult though is the task of verifying that any particular implementation of partial fencing logic actually provides the desired behavior of blocking down-stream impact of all signals from fenced interfaces, and also ensuring that the partial fencing does not inadvertently preclude any common logic from being fully tested. In this paper we discuss a case study for a verification method which exploits the power of formal verification to prove that any given partial fencing design satisfies all behavioral expectations. We describe the details of the verification method and discuss the benefits of using this approach versus using traditional simulation methods. We also discuss the testbenches created as part of applying this new method. Furthermore, we discuss the formal verification algorithms that were employed during application of the method along with the tuning that was done to enable efficient completion of the verification tasks at hand.

Pervasive logic is a broad term applied to the variety of logic present in hardware designs, yet not a part of their primary functionality. Examples of pervasive logic include initialization and self-test logic. Because pervasive logic is intertwined with the functionality of chips, the verification of such logic tends to require very deep sequential analysis of very large slices of the design. For this reason, pervasive logic verification has hitherto been a task for which formal algorithms were not considered applicable. In this paper, we discuss several pervasive logic verification tasks for which we have found the proper combination of algorithms to enable formal analysis. We describe the nature of these verification tasks, and the testbenches used in the verification process. We furthermore discuss the types of algorithms needed to solve these verification tasks, and the type of tuning we performed on these algorithms to enable this analysis

High-end hardware design flows mandate a variety of sequential transformations to address needs such as performance, power, post-silicon debug and test. Industrial demand for robust sequential equivalence checking (SEC) solutions is thus becoming increasingly prevalent. In this paper, we discuss the role of SEC within IBM. We motivate the need for a highly-automated scalable solution, which is robust against a variety of design transformations - including those that alter initialization sequences. This motivation has caused us to embrace the paradigm of SEC with respect to designated initial states. We furthermore describe the diverse set of algorithms comprised within our SEC framework, which we have found necessary for the automated solution of the most complex SEC problems. Finally, we provide several experiments illustrating the necessity of our diverse algorithm flow to efficiently solve difficult SEC problems involving a variety of design transformations.

We present several improvements to general-purpose sequential redundancy removal. (1) We propose using a robust variety of synergistic transformation and verification algorithms to process the individual proof obligations. This enables greater speed and scalability, and identifies a significantly greater degree of redundancy, than prior approaches. (2) We generalize upon traditional redundancy removal and utilize the speculatively-reduced model to enhance bounded search, without needing to complete any proofs.