Although model checking is an exhaustive formal verification method, a bug can still escape detection if the erroneous behavior does not violate any verified property.We propose a coverage metric to estimate the "completeness" of a set of properties verified by model checking.A symbolic algorithm is presented to compute this metric for a subset of the CTL property specification language.It has the same order of computational complexity as a model checking algorithm.Our coverage estimator has been applied in the course of some real-world model checking projects.We uncovered several coverage holes including one that eventually led to the discovery of a bug that escaped the initial model checking effort.

Article Free Access Share on Word level model checking—avoiding the Pentium FDIV error Authors: E. M. Clarke School of Computer Science, Carnegie Mellon University, Pittsburgh, PA School of Computer Science, Carnegie Mellon University, Pittsburgh, PAView Profile , M. Khaira Intel Development Labs., Intel Corporation, 5200 NE Elam Young Pkwy, Hillsboro, OR Intel Development Labs., Intel Corporation, 5200 NE Elam Young Pkwy, Hillsboro, ORView Profile , X. Zhao School of Computer Science, Carnegie Mellon University, Pittsburgh, PA and Intel Development Labs., Intel Corporation, 5200 NE Elam Young Pkwy, Hillsboro, OR School of Computer Science, Carnegie Mellon University, Pittsburgh, PA and Intel Development Labs., Intel Corporation, 5200 NE Elam Young Pkwy, Hillsboro, ORView Profile Authors Info & Claims DAC '96: Proceedings of the 33rd annual Design Automation ConferenceJune 1996 Pages 645–648https://doi.org/10.1145/240518.240640Published:01 June 1996Publication History 20citation393DownloadsMetricsTotal Citations20Total Downloads393Last 12 Months52Last 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

Model checking is an automatic technique for verifying sequential circuit designs and protocols. An efficient search procedure is used to determine whether or not the specification is satisfied. If it is not satisfied, our technique will produce a counterexample execution trace that shows the cause of the problem. We describe an efficient algorithm to produce counterexamples and witnesses for symbolic model checking algorithms. This algorithm is used in the SMV model checker and works quite well in practice. We also discuss how to extend our technique to more complicated specifications.

Functions that map boolean vectors into the integers are important for the design and verification of arithmetic circuits. MTBDDs and BMDs have been proposed for representing this class of functions. We discuss the relationship between these methods and describe a generalization called hybrid decision diagrams which is often much more concise. We show how to implement arithmetic operations efficiently for hybrid decision diagrams. In practice, this is one of the main limitations of BMDs since performing arithmetic operations on functions expressed in this notation can be very expensive. In order to extend symbolic model checking algorithms to handle arithmetic properties, it is essential to be able to compute the BDD for the set of variable assignments that satisfy an arithmetic relation. In our paper, we give an efficient algorithm for this purpose. Moreover, we prove that for the class of linear expressions, the time complexity of our algorithm is linear in the number of variables.

We show very efficient methods to compute Walsh spectrum for logic functions with large numbers of inputs (30 or more) using Binary Decision Diagrams. The BUD structure is extended to have any integer values as leaf (constant) nodes. The result is an efficient representation for integer vectors and integer matrices. The proposed procedure works directly on an extended BDD for the logic function, and computes the full Walsh spectrum in the form of an extended BDD. The algorithm presented is a more efficient version of the matrix-multiplication method. Our method embeds the Walsh transform matrix implicitly into program code with recursive calls, which results in a significant speed improvement. Our algorithm has the same complexity as the fastest known Walsh algorithm, and utilizes a much more efficient data structure than traditional truth tables. Furthermore, in cases where the complete set of spectra coefficient is either infeasible or impractical, we also present a method to compute subsets of Walsh coefficients. We present experimental results showing that logic functions having more than 60 inputs which cannot be processed by other published methods can be computed within 30 seconds on Sparc 2.>

The Walsh transform has numerous applications in computer-aided design, but the usefulness of these tech-niques in practice has been limited by the size of the boolean functions that can be transformed. Currently available techniques limit the functions to less than 20 variables. In this paper, we show how to compute concise representations of the Walsh transform for functions with several hundred vari-ables. We have applied our techniques to boolean technolqy mapping and, in certain cases, we obtained a speed up of as much as 50 % for the matching phase.