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.

Simulation and Boolean satisfiability (SAT) checking are common techniques used in logic verification. This paper shows how simulation and satisfiability (S&S) can be tightly integrated to efficiently compute flexibilities in a multilevel Boolean network, including the following: 1) complete "don't cares" (CDCs); 2) sets of pairs of functions to be distinguished (SPFDs); and 3) sets of candidate nodes for resubstitution. These flexibilities can be used in network optimization to change the network structure while preserving its functionality. In the first two applications, simulation quickly enumerates most of the solutions while SAT detects the remaining solutions. In the last application, simulation efficiently filters out most of the infeasible solutions while SAT checks the remaining candidates. The experimental results confirm that the combination of simulation and SAT offers a computation engine that outperforms binary decision diagrams, which are traditionally used in such applications.

This paper describes linear cofactor relationships (LCRs), which are defined as the exclusive sums of cofactors with respect to a pair of variables in Boolean functions. These relationships subsume classical symmetries and single-variable symmetries. The paper proposes an efficient algorithm to detect LCRs and discusses their potential applications in Boolean matching, minimization of decision diagrams, synthesis of regular layout-friendly logic circuits, and detection of support-reducing bound sets

Detecting support-reducing bound sets is an important step in Boolean decomposition. It affects both the quality and the runtime of several applications in technology mapping and re-synthesis. This paper presents an efficient heuristic method for detecting support-reducing bound sets using two-cofactor symmetries. Experiments on the MCNC and ITC benchmarks show an average 40x speedup over the published exhaustive method for bound set construction.

Embedded systems are electronic devices that function in the context of a real environment, by sensing and reacting to a set of stimuli. Because of their close interaction with the environment, and to simplify their design, different parts of an embedded system are best described using different notations and different techniques. In this case, we say that the system is heterogeneous.We informally refer to the notation and the rules that are used to specify and verify the elements of heterogeneous system and their collective behavior as a model of computation. In this paper, we focus in particular on abstraction and refinement relationships in the form of conservative approximations. We do so by constructing a framework, called Agent Algebra, where the different models reside and share a common algebraic structure. We compare our techniques to the well established notion of abstract interpretation. We show that, unlike abstract interpretations, conservative approximations preserve refinement verification results from an abstract to a concrete model while avoiding false positives. In addition, we use the inverse of a conservative approximation to identify components that can be used indifferently in several models, thus enabling reuse across domains of computation.

In many computer-aided design tools, binary decision diagrams (BDDs) are used to represent Boolean functions. To increase the efficiency and capability of these tools, many algorithms have been developed to reduce the size of the BDDs. This paper presents heuristic algorithms to minimize the size of the BDDs representing incompletely specified functions by intelligently assigning don't cares to binary values. Experimental results show that new algorithms yield significantly smaller BDDs compared with existing algorithms yet still require manageable run-times. These algorithms are particularly useful for synthesis application where the structure of the hardware/software is derived from the BDD representation of the function to implement because the minimization quality is more critical than the minimization speed in these applications.

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

In many computer-aided design tools, binary decision diagrams(BDDs) are used to represent Boolean functions. To increase theefficiency and capability of these tools, many algorithms have beendeveloped to reduce the size of BDDs. This paper presents heuristicalgorithms that minimize the size of BDDs representing incompletelyspecified functions by intelligently assigning don't cares tobinary values. The traditional algorithm, restrict [Verification of Synchronous Sequential Machines Based on Symbolic Execution], is often effectivein BDD minimization, but can increase the BDD size. We proposenew algorithms based on restrict which are guaranteed neverto increase the size of the BDD, thereby significantly reducing peakmemory requirements. Experimental results show that our techniquestypically yield significantly smaller BDDs than restrict.

Burch and Dill [3] described an automatic method for verifying a pipelined processor against its instruction set architecture (ISA).We describe three techniques for improving this method.We show how the combination of these techniques allows for the automatic verification of the control logic of a pipelined, superscalar implementation of a subset of the DLX architecture.

We describe an efficient validity checker for the quantifier-free logic of equality with uninterpreted functions. This logic is well suited for verifying microprocessor control circuitry since it allows the abstraction of datapath values and operations. Our validity checker uses special data structures to speed up case splitting, and powerful heuristics to reduce the number of case splits needed. In addition, we present experimental results and show that this implementation has enabled the automatic verification of an actual high-level microprocessor description.

The temporal logic model checking algorithm of Clarke, Emerson, and Sistla (1986) is modified to represent state graphs using binary decision diagrams (BDD's) and partitioned transition relations. Because this representation captures some of the regularity in the state space of circuits with data path logic, we are able to verify circuits with an extremely large number of states. We demonstrate this new technique on a synchronous pipelined design with approximately 5/spl times/10/sup 120/ states. Our model checking algorithm handles full CTL with fairness constraints. Consequently, we are able to express a number of important liveness and fairness properties, which would otherwise not be expressible in CTL. We give empirical results on the performance of the algorithm applied to both synchronous and asynchronous circuits with data path logic.>

We present sufficient conditions for the correctness of speed-independent circuits with respect to their state graph (SG) specification, which can be tested in linear-time with respect to the size of the SG. Our correctness conditions consist of one safety condition and one progress condition. The progress condition detects deadlock conditions that are not present in the specification. The SG specifications considered are determinate, allowing input choice (conditionals) but not output choice (arbitration). The circuits considered are a network of basic gates; arbiters and mutual-exclusion elements are not allowed. We present an efficient algorithm to test the correctness conditions, in which false positives are not possible, but false negatives are possible. We have implemented the algorithm and present a table of run-time comparisons between our verification tool and the tool AVER by D. Dill on a large benchmark of asynchronous circuits. The results demonstrate run-times of over an order of magnitude faster than AVER and no false negatives were found. Our speedup is achieved by avoiding the state explosion problem caused by explicitly examining the behavior of internal signals.

Hierarchical descriptions of combinational circuits often contain apparent loops. Since it may be difficult to distinguish apparent loops from actual loops, it is useful to construct models of combinational circuits that can handle cyclic dependencies. We show that Boolean relations are inadequate for this purpose, and define a ternary model that solves the problem. We use the model to characterize exact solutions to a broad class of substitution and rectification problems. The theory cleanly handles network transformations that might introduce cyclic dependencies.

Efficient algorithms for performing the matching step in technology mapping are proposed. The main result is an algorithm for matching under input negations that takes time polynomial in the size of the BDDs representing the functions to be matched. This algorithm is the basis for efficient methods for matching under permutations, bridging and constant inputs. A simple mapper based on the algorithms was implemented and tested on a suite of combinational circuits. Using the Actel type 1 mother cell, the mapper required an average of 8.5% fewer cells than mispga. When integrated into a more sophisticated technology mapper, the matching algorithms could provide even better performance.>

It is demonstrated that the binary inertial delay model can lead to false positive results when used in the verification of speed-dependent asynchronous circuits. A delay model called the binary chaos delay model solves this problem in many cases. The two timing models are compared by using them in the verification of a FIFO controller circuit. The models can be viewed as two extremes of a more general, parameterized model.>

Bryant’s Binary Decision Diagrams (BDDs) [6] have been successfully used for verifying combinational circuits [12, 181. However, multiplier circuits are difficult to verify using BDDs since the size of the BDD representing multiplication grows exponentially in the number of input bits [6, 71. This paper presents a method for using BDDs to verify multipliers that avoids this exponential complexity. The method has been used to verify a 16 by 16 bit combinational multiplier, the C6288 circuit from the ISCAS85 benchmarks [5]. This is the only ISCAS85 benchmark circuit that could not be verified using the techniques described by Fujita et al. [12] and Malik et al. [la].

Article Representing circuits more efficiently in symbolic model checking Share on Authors: J. R. Burch School of Computer Science, Carnegie Mellon University School of Computer Science, Carnegie Mellon UniversityView Profile , E. M. Clarke School of Computer Science, Carnegie Mellon University School of Computer Science, Carnegie Mellon UniversityView Profile , D. E. Long School of Computer Science, Carnegie Mellon University School of Computer Science, Carnegie Mellon UniversityView Profile Authors Info & Claims DAC '91: Proceedings of the 28th ACM/IEEE Design Automation ConferenceJune 1991 Pages 403–407https://doi.org/10.1145/127601.127702Online:01 June 1991Publication History 134citation365DownloadsMetricsTotal Citations134Total Downloads365Last 12 Months6Last 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

The temporal logic model checking algorithm developed by Clarke, Emerson, and Sistla [9] is modified to represent a state graph using binary decision diagrams (BDD's) [4]. Because this representation captures some of the regularity in the state space of sequential circuits with data path logic, we are able to verify circuits with an extremely large number of states. We demonstrate this new technique on a synchronous pipelined design with approximately 5 x 1020 states. Our model checking algorithm handles full CTL with fairness constraints. Consequently, we are able to handle a number of important liveness and fairness properties, which would otherwise not be expressible in CTL. We give empirical results on the performance of the algorithm applied to both synchronous and asynchronous circuits with data path logic.

A general method that represents the state space symbolically instead of explicitly is described. The generality of the method comes from using a dialect of the mu-calculus as the primary specification language. A model-checking algorithm for mu-calculus formulas which uses R.E. Bryant's (1986) binary decision diagrams to represent relations and formulas symbolically is described. It is then shown how the novel mu-calculus model checking algorithm can be used to derive efficient decision procedures for CTL model checking, satisfiability of linear-time temporal logic formulas, strong and weak observational equivalence of finite transition systems, and language containment of finite omega -automata. This eliminates the need to describe complicated graph-traversal or nested fixed-point computations for each decision procedure. The authors illustrate the practicality of their approach to symbolic model checking by discussing how it can be used to verify a simple synchronous pipeline.>

An extension of trace theory is described that allows for the verification of asynchronous circuits that are not speed-independent, but instead rely on assumptions about the delays of their components for correct operation. The theory has been implemented in an automatic verifier that checks whether a circuit satisfies a given formal specification in time linear in the number of states of both the specification and the circuit. The ability of the verifier to model timing assumptions greatly expands the class of circuits that can be automatically verified, making the verifier a more useful tool in the design of asynchronous circuits. The verifier is demonstrated on a self-timed queue element.>