Model checking has become a formal sign-off requirement in the verification plans of many hardware designs. For design sizes encountered in practice, compositional assume-guarantee reasoning is often necessary to achieve satisfactory results. However, many pitfalls exist that can create unsound or unexpected results for users of commercial model checking tools. Users need to watch out for circularity in properties, for dead-ends getting trimmed by tools, as well as understand the differences in proof composition for liveness and safety properties. We present many real design examples to illustrate these points, as well as describe our experiences with compositional reasoning in practice.

Formal verification technology has today advanced to the stage that it can complement or replace simulation effort for selected hardware designs. Yet the completion of a formal verification effort is rarely a requirement for hardware tapeout. Simulation remains the primary verification methodology, and means of deciding when verification is complete. In this paper we discuss how formal verification can be deployed using simulation-based coverage in a simulation-based verification schedule.

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 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.

We are concerned with optimizing gate-level netlists containing “black boxes,” that is, components whose functionality is not available to the optimization tool. We establish a notion of equivalence for gate-level netlists containing black boxes, and prove that it is sound and complete. We show that conventional approaches to optimizing such netlists fail to fully exploit the don't care flexibility available for synthesis. Based on our new notion of equivalence, we introduce a procedure that computes the complete don't care set. Experiments indicate that our procedure can achieve more minimization than conventional synthesis.

This paper describes a new BDD-based logic optimization system, BDS. It is based on a recently developed theory for BDD-based logic decomposition, which supports both algebraic and Boolean factorization. New techniques, which are crucial to the manipulation of BDDs in a partitioned Boolean network environment, are described in detail. The experimental results show that BDS has a capability to handle very large circuits. It offers a superior runtime advantage over SIS, with comparable results in terms of circuit area and often improved delay.

Previous researchers have suggested the use of "lighthouses" to act as guides in directed state space search. The drawback of using lighthouses is that the user has to manually, derive them, through a potentially laborious examination of the design. Additionally specifying a large number of lighthouses results in wasted effort during the search. We present approaches to automatically generate high-quality lighthouses for hard-to-cover targets.

We present a logical formalism for expressing properties of continuous-time Markov chains. The semantics for such properties arise as a natural extension of previous work on discrete-time Markov chains to continuous time. The major result is that the verification problem is decidable; this is shown using results in algebraic and transcendental number theory.

Retiming combined with combinational optimization is a powerful sequential synthesis method. However, this methodology has not found wide application because formal sequential verification is not practical and current simulation methodology requires the correspondence of latches disallowing any movement of latches. We present a practical verification technique which permits such sequential synthesis for a class of circuits. In particular, we require certain constraints to be met on the feedback paths of the latches involved in the retiming process. For a general circuit, we can satisfy these constraints by fixing the location of some latches, e.g., by making them observable. We show that equivalence checking after performing repeated retiming and synthesis on this class of circuit reduces to a combinational verification problem. We also demonstrate that our methodology covers a large class of circuits by applying it to a set of benchmarks and industrial designs.

A unified logic optimization method efficient at handling both AND/OR-intensive and XOR-intensive functions is proposed. The method is based on iterative BDD decomposition using various dominators. Detail analysis of decomposable BDD structures leading to AND/OR, XOR and MUX decompositions are presented. Experiment shows that our synthesis results for AND/OR-intensive functions are comparable to those of SIS, and results for XOR-intensive functions are comparable to those of techniques targetting specifically XOR decomposition.

Existing literature on combinational equivalence checking concentrates on comparing combinational blocks and assumes that a latch mapping (register mapping) has already been constructed. We describe an algorithm for automatically constructing a latch mapping. It is based on the functionality of the circuits being compared rather than on heuristics. As a result, if two circuits are combinationally equivalent, then our algorithm is guaranteed to find a latch mapping. Our empirical results show that the method is practical on large circuits. 1. Introduction When applied to a pair of sequential circuits, combinational equivalence checking typically consists of two steps. The first step is to construct a latch mapping (also known as a register mapping). This identifies corresponding latches in the two designs to be compared. It is then possible to break the circuits into corresponding combinational blocks. The second step is to verify whether the corresponding combinational blocks are equ...

Article Free Access Share on Tight integration of combinational verification methods Authors: Jerry R. Burch Cadence Berkeley Labs, 2001 Addison St, 3rd Floor, Berkeley, CA Cadence Berkeley Labs, 2001 Addison St, 3rd Floor, Berkeley, CAView Profile , Vigyan Singhal Cadence Berkeley Labs, 2001 Addison St, 3rd Floor, Berkeley, CA Cadence Berkeley Labs, 2001 Addison St, 3rd Floor, Berkeley, CAView Profile Authors Info & Claims ICCAD '98: Proceedings of the 1998 IEEE/ACM international conference on Computer-aided designNovember 1998 Pages 570–576https://doi.org/10.1145/288548.289088Published:01 November 1998Publication History 29citation215DownloadsMetricsTotal Citations29Total Downloads215Last 12 Months9Last 6 weeks7 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

Retiming and resynthesis transformations can be used for optimizing the area, power, and delay of sequential circuits. Even though this technique has been known for more than a decade, its exact optimization capability has not been formally established. We show that retiming and resynthesis can exactly implement 1-step equivalent state transition graph transformations. This result is the strongest to date. We also show how the notions of retiming and resynthesis can be moderately extended to achieve more powerful state transition graph transformations. Our work will provide theoretical foundation for practical retiming and resynthesis based optimization and verification. 1 Introduction In combinational synthesis [1, 8], the positions of the latches are fixed and the logic is optimized for area, delay, or power. In retiming [5], the latches are moved across combinational gates. Retiming can change the number of latches (and hence the area) and the minimum cycle time (i.e., the clock r...

We define a notion of equivalence for designs containingblack boxes i.e., components whose functionality is notknown; these arise naturally in the course of hierarchicaldesign. Using this notion, we describe a sound andcomplete methodology for optimizing such designs.

We propose an algorithm for area optimisation of sequential circuits through redundancy removal. The algorithm finds compatible redundancies by implying values over nets in the circuit. The potentially exponential cost of state space traversal is avoided and the redundancies found can all be removed at once. The optimised circuit is a safe delayed replacement of the original circuit. The algorithm computes a set of compatible sequential redundancies and simplifies the circuit by propagating them through the circuit. We demonstrate the efficacy of the algorithm even for large circuits through experimental results on benchmark circuits.

Retiming is often used to optimize synchronous sequential circuits for area or delay or both. If the latches that are retimed have a hardware reset value, the initial state of the circuit must also be retimed, i.e. an initial state must be derived for the retimed circuit. Previously, it has been suggested that this can be avoided if the hardware reset signals are represented explicitly. However, it was thought that this adds unnecessary area and restricts the space of possible retimings. We demonstrate that this is not the case. In addition, we show that this methodology does not require the restriction that all reset signals be asserted at the beginning of circuit operation-a restriction that was imposed by existing algorithms for determining the retimed initial state. Finally we show how our explicit reset (ER) framework enables us to retime when some latches may be driven by different hardware resets, and some others may not have any hardware resets. We also consider the case where the resets are asynchronous. We expect these solutions to the "retimed initial state" problem to help increase the practical applicability of retiming.

For circuits where there may be latches with no reset line, we show how to replace some of them with combinational logic. All previous work in sequential optimization by latch removal assumes a designated initial state. Without this assumption, the design can power up in any state and earlier techniques are not applicable. We present an algorithm for identifying and replacing redundant latches by combinational logic such that no environment of the design can detect the change. The new design preserves the steady state behavior as well as all initializing sequences of the old design. We report experimental results on benchmark circuits and demonstrate savings in area without adverse impact on delay.

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.

Computing the set of reachable states of a finite state machine, is an important component of many problems in the synthesis and formal verification of digital systems. The process of design is usually iterative, and the designer may modify and recompute information many times, and reachability is called each time the designer modifies the system because current methods for reachability analysis are not incremental. Unfortunately, the representation of the reachable states that is currently used in synthesis and verification, is inherently non updatable (O. Coudert and J.C. Madre, 1990). We solve this problem by presenting alternate ways to represent the reachable set, and incremental algorithms that can update the new representation each time the designer changes the system. The incremental algorithms use the reachable set computed at a previous iteration, and information about the changes to the system to update it, rather than compute the reachable set from the beginning. This results in computational savings, as demonstrated by the results.

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...

Article Free Access Share on HSIS: a BDD-based environment for formal verification Authors: A. Aziz Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , F. Balarin Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , S.-T. Cheng Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , R. Hojati Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , T. Kam Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , S. C. Krishnan Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , R. K. Ranjan Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , T. R. Shiple Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , V. Singhal Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , S. Tasiran Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , H.-Y. Wang Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , R. K. Brayton Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , A. L. Sangiovanni-Vincentelli Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile Authors Info & Claims DAC '94: Proceedings of the 31st annual Design Automation ConferenceJune 1994 Pages 454–459https://doi.org/10.1145/196244.196467Published:06 June 1994Publication History 39citation325DownloadsMetricsTotal Citations39Total Downloads325Last 12 Months36Last 6 weeks17 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

We address the problem of compositional minimization of collections of interacting finite state machines that arise in the context of formal verification of hardware designs by language containment. Typically much of the behavior of the system is redundant with respect to a given property being verified, and so the system can be replaced by substantially simpler representations. We show that these redundancies can be captured by computing states that are input-output equivalent in the presence of fairness. Since computing complete equivalences is computationally expensive, we propose a spectrum of approximations which are efficiently computable. Directly minimizing the entire system requires forming the complete product machine, which can be very large, and hence we describe procedures that hierarchically minimize the system with respect to explicit and BDD representations. We present experimental results on some standard verification examples to show that our algorithms allow the product machine to be represented by very small implicit or explicit representations. We conclude with some further directions.>

Synchronous Boolean relations can represent sequential don't-care information in synchronous systems. These relations allow greater flexibility in expressing don't-care information than ordinary Boolean relations. Synchronous relations can be used to specify sequential designs at the finite state machine level as well as at the level of combinational elements and latches. The main objective of this paper is to present a heuristic approach to find a minimal implementation for a given synchronous relation. We also show that the synchronous relation formulation can also be used to find a minimal sum-of-products form which implements a function that is compatible with an arbitrary set of Boolean relations.>