Checking the equivalence of a system-level model against an RTL design is a major challenge. The reason is that usually the system-level model is written by a system architect, whereas the RTL implementation is created by a hardware designer. This approach leads to two models that are significantly different. Checking the equivalence of real-life designs requires strong solver technology. The challenges can only be overcome with a combination of bit-level and word-level reasoning techniques, combined with the right orchestration. In this paper, we discuss solver technology that has shown to be effective on many real-life equivalence checking problems.

When designers create RTL models from a system-level specification, arrays in the system-level model are often implemented as memories in the RTL. Knowing the correspondence between ESL arrays and RTL memories can significantly reduce the complexity of a formal equivalence check between the ESL model and the RTL. In practice, however, handling memory mappings in ESL-RTL equivalence checking is non-trivial for the following reasons: First, because of a lack of bit-accurate data-types in the systemlevel language, the information stored in an array location may be stored in a compressed form in the RTL. Second, a single array in the ESL model may be implemented by multiple memories in the RTL and/or corresponding data items may be stored in different locations. And last but not least, due to timing differences between the ESL model and the RTL, the correspondence between arrays and memories may not hold in every clock cycle. In this paper, we propose an approach to ESL-RTL equivalence checking which can deal with all of these difficulties.

This thesis shows that designers definitely do want proofs. The first author saw ample evidence of that at Motorola, where he managed a verification CAD group, and at Synopsys, where he was involved in verification tools, customers, and in verification projects with our DesignWare component groups. Our talk will discuss some success we had with our DesignWare team.

Simulation by random vectors is meaningful only if the vectors meet certain requirements on the environment that drives the design under verification. When that environment is modeled by constraints, we face the problem of solving constraints efficiently. We present an efficient algorithm for simplifying conjunctive Boolean constraints defined over state and input variables, and apply it to constrained random simulation vector generation using binary decision diagrams (BDDs). The method works by extracting "hold-constraints" from the system of constraints. Hold-constraints are deterministic and trivially resolvable. They can be used to simplify the original constraints as well as refine the conjunctive partition. Experiments demonstrate significant reductions in the time and space required for constructing the conjunction BDDs, and the time spent in vector generation during simulation.

Despite a number of solid advances in simulation and verification techniques over the last twenty years, semiconductor chip designs continue to see large increases in the cost of verification - both in terms of human resources and time. Most of these increases are due to the growing size and complexity of the chip designs. Many of these designs are complete systems in their own right thus enlarging the scope of the verification problem. Formal verification has held out the most promise for reducing the magnitude of the verification task. Indeed, most major microprocessor teams - at IBM, Intel and Motorola - have routinely hosted formal verification experts since the early '90s. ASIC vendors and their tool providers have been closely following these developments into a number of initiatives and new startup companies driven by that very promise of formal verification. Despite these developments, simulation continues to be the final source of signoff - if not confidence - in chip tapeouts. Why is this so? Formal verification is an important technology to be left at the margins of the validation task. Will formal verification eliminate or limit unit level verification and provide the necessary glue for a realistic validation flow? Will the testbenches be replaced by constraints and assertions? Can validation effort be reused? This panel will explore the issues related to building practical validation flows, and the technologies that the designer community can realistically look forward to materializing in their lifetimes.

Modeling design environment with constraints instead of a traditional testbench is advantageous in a hybrid verification framework that encompasses simulation and formal verifica-tion. This movement is gaining popularity in industry and sparks research in the constraint-based environment mod-eling and stimulus generation problem. We present an ap-proach, called constraint synthesis, to this problem. Con-straint synthesis falls in the general category of parametric Boolean equation solving but is novel in utilizing don’t care information unique to hardware constraints and heuristic variable removal to simplify the solution. Experimental re-sults have demonstrated the effectiveness of the proposed approach.

We study the problem of optimizing synchronous sequential circuits. There have been previous efforts to optimize such circuits. However, all previous attempts make implicit or explicit assumptions about the design or the environment of the design. For example, it is widespread practice to assume the existence of a hardware reset line and consequently a fixed power-up state; in the absence of the same, a common premise is that the design's environment will apply an initializing sequence. We review the concept of safe replaceability which does away with these assumptions and the delay-safe replaceability notion, which is applicable when the design's output is not used for a certain number of cycles after power-up. We then develop procedures for optimizing the combinational next-state and output logic, as well as routines for reencoding the state space and removing state bits under these replaceability criteria. Experimental results demonstrate the effectiveness of our algorithms.

We present an algorithm for simplifying the solution of conjunctive Boolean constraints of state and input variables, in the context of constrained random vector generation using BDDs. The basis of our approach is extraction of "hold-constraints" from constraint system. Hold-constraints are deterministic and trivially resolvable; in addition, they can be used to simplify the original constraints as well as refine the conjunctive partition. Experiments demonstrate significant reduction in the time and space needed for constructing the conjunction BDDs, and the time spent in vector generation during simulation.

We address the problem of developing suitable criteria for design replacement in the context of sequential logic synthesis. There have been previous efforts to characterize replacements for such designs. However, all previous attempts either make implicit or explicit assumptions about the design or the environment of the design. For example, it is widespread practice to assume the existence of a hardware reset line and, consequently, a fixed power-up state; in the absence of the same, a common premise is that the design's environment will apply an initializing sequence. We present the notion of safe replaceability, which does away with these assumptions, and prove a number of properties that hold of it. Most importantly, we show that the notion is sound, i.e., if design D/sub 1/ is a safe replacement for design D/sub 0/, then no environment can determine if D/sub 1/ is used in place of D/sub 0/ and that the notion is complete, i.e., if D/sub 1/ is not a safe replacement for D/sub 0/ then there exists an environment that can detect if D/sub 1/ is used in place of D/sub 0/. Completeness is important for logic synthesis and verification because it specifies the maximum allowable flexibility for replacement. When the design's output is not used for a certain number of cycles after power up, then safe replaceability can be relaxed to obtain what we refer to as delay safe replaceability; we analyze properties of this notion too. Since our work, many papers have used this notion effectively for sequential optimization.

Constraining and input biasing are frequently used techniques in functional verification methodologies based on randomized simulation generation. Constraints confine the simulation to a legal input space, while input biasing, which can be considered as a probabilistic constraint, makes it easier to cover interesting "corner" cases. In this paper, we propose to use constraints and biasing to form a simulation environment instead of using an explicit testbench in hierarchical functional verification. Both constraints and input biasing can depend on the state of the design and thus are very expressive in modeling the environment. We present a novel method that unifies the handling of constraints and biasing via the use of Binary Decision Diagrams (BDDs). The distribution of input vectors under the effect of constraints and input biasing are determined by what we refer to as the constrained probabilities. A BDD representing the constraints is first built, then an algorithm is applied to bias the branching probabilities in the BDD. During simulation, this annotated BDD is used to generate input vectors whose distribution matches their predetermined constrained probabilities. The simulation generation is a one-pass process, i.e., no backtracking or retry is needed. Also, we describe a partitioning method to minimize the size of BDDs used in simulation generation. Our techniques were used in the verification of a set of commercial designs; experimental results demonstrated their effectiveness.

RDCs (Reachability Don’t Cares) can have a dramatic impact on the cost of CTL model checking [18]. Unfortunately, RDCs, being a global property, are often much more difficult to compute than the satisfying set of typical CTL formulas. We address this problem through the use of Approximate Reachability Don’t Cares (ARDCs), computed with the algorithms developed for the VERITAS sequential synthesis package [4, 5]. Approximate Reachable states represent an upper bound on the set of true reachable states, and thus a lower bound on the set of unreachable (Don’t Care) states. ARDCs can be 10X to 100X (or much more for very large circuits) cheaper to compute than RDCs, and in some cases have the same dramatic effect on CTL model checking as the real RDCs. We also discuss the application of ARDCs to the problem of exact computation of the RDCs themselves. Experiments on industrial benchmarks show that order of magnitude speedups are possible, and occur frequently. The experimental results presented strongly support our claim that ARDCs play a safe and important way out of a serious dilemma: RDCs are necessary for tractable model checking of many large circuits, but the computation of the RDCs themselves is often intractable. We include, and theoretically justify, significant extensions of the VERITAS algorithms, and show that they can be up to an order of magnitude faster, while computing a virtually identical upper bound. 1

We present our experiences with the formal verification of an automotivechip used to control the safety features in a car. We useda BDD based model checker in our work. We describe our verificationmethodology for verifying a very complicated property on arelatively large design. We also describe the bugs that were foundand present our views on how to make model checking an effectiveintegrated part of the design flow for complex hardware systems.

We describe a project in which the IBM/Motorola 60/spl times/ bus protocol was incrementally modeled at an abstract level in Verilog and verified using Motorola's Verdict model checker. The primary purpose of the modeling activity was to acquaint verification personnel with details of the 60/spl times/ bus protocol and to document specific properties of the 60/spl times/ bus that are necessary to guarantee compliance with hand-written protocol documentation. Our Verilog 60/spl times/ bus model documents the 60/spl times/ bus protocol for other Motorola business units.

Commercial design verification is a complex activity involving many abstraction levels (such as architectural, register transfer, gate, switch, circuit, fabrication), many different aspects of design (such as timing, speed, functional, power, reliability and manufacturability) and many different design styles (such as ASIC, full custom, semi-custom, memory, cores, and asynchronous). We present a representative design flow and methodology that is common to many commercial integrated circuit design environments and that concentrates on functional validation using informal verification (e.g., simulation, emulation and ATPG) and formal verification (e.g., logic checking and sequential verification).

Retiming has been proposed as an optimization step for sequential circuits represented at the net-list level.Retiming moves the latches across the logic gates and in doing so changes the number of latches and the longest path delay between the latches.In this paper we show by example that retiming a design may lead to differing simulation results when the retimed design replaces the original design.We also show, by example, that retiming may not preserve the testability of a sequential test sequence for a given stuck-at fault as measured by a simulator.We identify the cause of the problem as forward retiming moves across multiple-fanout points in the circuit.The primary contribution of this paper is to show that, while an accurate logic simulation may distinguish the retimed circuit from the original circuit, a conservative three-valued simulator cannot do so.Hence, retiming is a safe operation when used in a design methodology based on conservative three-valued simulation starting each latch with the unknown value.

Retiming is sometimes used to optimize gate-level sequential designs. This technique allows memory elements to be moved across combinational elements. Unfortunately, retiming may cause the environment of a design to wait for a few additional clock cycles after power-up to guarantee the same behavior as the original design. Leiserson and Saxe [1] presented a bound on this number of clock cycles; in this paper, we tighten this bound. A smaller bound allows the environment of a design to wait for fewer clock cycles. 1 Introduction Retiming, first formulated by Leiserson and Saxe [1] in the context of systolic systems, is a method for moving memory elements or registers (implemented by edge-triggered latches or flip-flops) across combinational logic to achieve a minimum clock period, a minimum area, or a combination of these cost functions. It has earlier been shown [2] that retiming can change the sequential behavior of a design. Given a sequential circuit with some registers, each regi...

In order to reliably predict the behavior of a finite state machine (FSM) M or to generate acceptance tests for sequential designs, it is necessary to drive M to a predictable state or set of states. One possible way of accomplishing this is to have a special reset circuit to force all the latches to a specific state. However, if the circuit can be driven to a predictable state by applying an input sequence, the area required for reset circuitry can be saved. A synchronizing sequence for an FSM M is an input sequence which, when applied to any initial state of M, will drive M to a single specific state, called a reset state. An efficient and exact method for computing synchronizing sequences based on the efficient image and pre-image computation methods using binary decision diagrams is presented. The method is exact in the sense that it is a decision procedure: Given enough time and memory, the method can compute a synchronizing sequence if M has one; otherwise, the method says that M is not resettable. The theoretical heart of the proposed method is Universal Alignment, which is an analysis of the product of an FSM with itself. Algorithms and their related theorems are presented to perform the following: decide whether M has a synchronizing sequence (i.e., M is resettable), calculate a synchronizing sequence for M, calculate the set of all reset states, decide whether a specific state is a reset state. New results on the resettability of some benchmark circuits are reported.>

computing synchronizing sequences is an important step in experimental results that show the viability of the proposed method for much larger circuits than were tractable by previous exact methods.

A theory of sequential hardware equivalence is presented. This theory includes the notions of gate-level model (GLM), hardware finite state machine (HFSM), quotient machine, state equivalence ( approximately ), alignability, resetability, essential resetability, isomorphism, and sequential hardware equivalence. The theory is motivated by (1) the observation that it is impossible to control the initial state of a machine when it is powered on and (2) the desire to decide equivalence of two designs based solely on their netlists and logic device models, without knowledge of intended initial states or intended environments. Algorithms based upon a binary decision diagram (BDD) implementation of predicate calculus over Boolean domains are presented. This calculus is employed to calculate properties of hardware designs. Experimental results based upon these algorithms as implemented in the MCC sequential equivalence tool (SET) are presented.>

A synchronous sequential design is resettable if there is a finite sequence of primary input vectors (called a reset or synchronizing sequence) and a single state (called a reset state) such that application of the reset sequence to any initial state of the design drives the design into the reset state. New, efficient algorithms are presented to decide if a design is essentially and actually resettable, to find essential and actual reset sequences, to find the set of essential reset states and an actual reset state, and to check that an alleged essential or actual reset sequence essentially or actually resets a design. These algorithms are based on the results of a theory of design equivalence presented by C. Pixley (1990), and C. Pixley and G. Beihl (1991). The algorithms are implemented in the MCC CAD Sequential Equivalence Tool and future optimizations among well-established lines promise greater speed and applicability to much larger designs.>

Efficient decision procedures based on binary decision diagrams (BDDs) have recently been developed for formal verification of hardware. A novel application of these procedures is presented. An algorithm is described for deciding whether a gate-level design satisfies a finite state machine specification. The unique feature of this method is that it does not require knowing the state encoding and, in fact, derives the encoding from the specification and a net-list description of the design. This algorithm is related to the algorithms that implement a computational theory of sequential hardware equivalence, as realized in the MCC-CAD sequential equivalence tool (SET). This theory of sequential hardware equivalence does not require knowledge of an initial state of the design.>