Circuits can be simplified for combinational equivalence checking by transforming internal functions, while preserving their ranges. In this paper, we investigate how to effectively apply the idea to improve equivalence checking. We propose new heuristics to identify groups of nets in a cut, and elaborate detailed aspects of the new equivalence checking method. With a given miter, we identify a group of nets in a cut and transform the function of each net into a more compact representation with less variables. These new compact parametric representations preserve the range of nets as well as of the cut. This transformation significantly reduces the size of intermediate BDDs and enables the verification to be conclusive for many designs which state-of-the-art equivalence checkers fail to verify. Iterative groupings and transformations are performed until no grouping is possible for a cut. Then we proceed to the next cut and continue until the compare point is reached. Our experimental results show the effectiveness of our strategy and new grouping heuristics on the new method.

Computing the set of states reachable in one step from a given set of states, i.e. image computation, is a crucial step in several symbolic verification algorithms, including model checking and reachability analysis. So far, the best methods for quantification scheduling in image computation, with a conjunctively partitioned transition relation, have been restricted to a linear schedule. This results in a loss of flexibility during image computation. We view image computation as a problem of constructing an optimal parse tree for the image set. The optimality of a parse tree is defined by the largest BDD that is encountered during the computation of the tree. We present dynamic and static versions of a new algorithm, VarScore, which exploits the flexibility offered by the parse tree approach to the image computation. We show by extensive experimentation that our techniques outperform the best known techniques so far.

We develop algorithms for exploring the reachable state-space of hardware designs that can be partitioned into control and data. The core procedure is a symbolic algorithm that tries to visit as many controller states as is computationally feasible. Here, we describe heuristics for making this traversal efficient. Experiments demonstrate that our approach is capable of achieving significantly greater coverage of the control state-space than conventional symbolic reachability analysis.

We present Ketchum, a tool that was developed to improve the productivity of simulation-based functional verification by providing two capabilities: (1) automatic test generation and (2) unreachability analysis. Given a set of "interesting" signals in the design under test (DUT), automatic test generation creates input stimuli that drive the DUT through as many different combinations (called coverage states) of these signals as possible to thoroughly exercise the DUT. Unreachability analysis identifies as many unreachable coverage states as possible.

The knowledge of the reachable states of a sequential circuit can dramatically speed up optimization and model checking. However, since exact reachability analysis may be intractable, approximate techniques are often preferable. H. Cho et al. (1996) presented the machine-by-machine (MBM) and frame-by-frame (FBF) methods to perform approximate finite state machine (FSM) traversal. FBF produces tighter upper bounds than MBM; however, it usually takes much more time and it may have convergence problems. In this paper, we show that there exists a class of methods-least fixpoint approximations-that compute the same results as RFBF ("reached FBF", one of the FBF methods). We show that one member of this class, which we call "least fixpoint MBM" (LMBM), is as efficient as MBM, but provably more accurate. Therefore, the trade-off that existed between MBM and RFBF has been eliminated. LMBM can compute RFBF-quality approximations for all the large ISCAS-89 benchmark circuits in a total of less than 9000 seconds.

We develop a verification paradigm called saturated simulation, that is applicable to designs which can be decomposed into a set of interacting controllers. The core procedure is a symbolic algorithm that explores the space of controller interactions; heuristics for making this traversal efficient are described. Experiments demonstrate that our procedure explores substantially more of the controller interactions, and is more efficient than conventional symbolic reachability analysis.

Efficient techniques for the manipulation of Binary Decision Diagrams (BDDs) are key to the success of formal verification tools. Recent advances in reachability analysis and model checking algorithms have emphasized the need for efficient algorithms for the approximation and decomposition of BDDs. In this paper we present a new algorithm for approximation and analyze its performance in comparison with existing techniques. We also introduce a new decomposition algorithm that produces balanced partitions. The effectiveness of our contributions is demonstrated by improved results in reachability analysis for some hard problem instances.

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 present heuristic algorithms for finding a minimum BDD size cover of an incompletely specified function, assuming the variable ordering is fixed.In some algorithms based on BDDs, incompletely specified functions arise for which any cover of the function will suffice.Choosing a cover that has a small BDD representation may yield significant performance gains.We present a systematic study of this problem, establishing a unified framework for heuristic algorithms, proving optimality in some cases,and presenting experimental results.

Two-phase logic design is a technique that has long been used in the IC industry to increase data throughput and improve silicon efficiency. The approach to this technique has often been adhoc due to its departure from the formal techniques of edge-triggered design taught in universities. This paper presents a formal and structured approach to two-phase logic design that we have been successfully using in the design of embedded controllers at National Semiconductor since 1990. It is both rigorous and fully compatible with HSIS, a formal verification tool from UC Berkeley.>

Article A unified approach to language containment and fair CTL model checking Share on Authors: Ramin Hojati View Profile , Thomas R. Shiple View Profile , Robert K. Brayton View Profile , Robert P. Kurshan View Profile Authors Info & Claims DAC '93: Proceedings of the 30th international Design Automation ConferenceJuly 1993 Pages 475–481https://doi.org/10.1145/157485.164985Online:01 July 1993Publication History 7citation260DownloadsMetricsTotal Citations7Total Downloads260Last 12 Months1Last 6 weeks0 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 SiteGet Access

A method for reducing the complexity of CTL model checking on a system of interacting finite state machines is described. The method consists essentially of reducing each component machine with respect to the property to be verified, and then verifying the property on the composition of the reduced components. The procedure is fully automatic and produces an exact result. The potential of the approach is assessed on real-world examples, and the method is demonstrated on a circuit.>

A description is given of CLEO, an automatic CMOS layout generator that takes as input an arbitrary sized circuit schematic and produces a CMOS layout as one or more horizontal rows of vertically oriented transistors. The layout can be controlled by specifying geometric constraints such as the number of rows desired, their specific heights and widths, and pins located on the region boundary. The tool was designed to lay out random logic sections of custom CMOS chips and is typically used with circuits ranging between 25 and 500 logic gates. CLEO obtains density close to handcrafted layout.>