We present a method for using a set of temporal properties (SVA, PSL, OVA, RTL monitors) as environment models for industrial-strength hybrid verification that combines formal methods with constrained random simulation. We demonstrate the effectiveness of the method on real-world designs.

We study model checking for a first-order linear-time temporal logic. We present the computation model: abstract description of state machines (ASMs), in which data and data operations are described using abstract sort and uninterpreted function symbols. ASMs are suitable for describing Register Transfer level designs. We define a first-order linear-time temporal logic called LMDG which supports the abstract data representations. Both safety and liveness properties can be expressed in LMDG, however, only universal path quantification is possible. Fairness constraints can also be imposed. The property checking algorithms are based on implicit state enumeration of an ASM and implemented using Multiway Decision Graphs.

As an efficient representation of Extended Finite State Machines, Multiway Decision Graphs (MDG) are suitable for automatic hardware verification of Register Transfer Level (RTL) designs. However, in some cases, MDG-based verification suffers from the state explosion problem. Some of cases are caused by the standard order used by MDG to order cross-terms that have the same top-level function symbol. These terms usually label decision nodes and must be ordered. We call this kind of state explosion the standard term ordering problem. A solution based on function renaming and cross-term rewriting is proposed in this paper. Experimental results show that this solution can solve the problem completely and thus increase the range of circuits that can be verified by MDG.

Given a pseudo-synchronous (sampled input) finite-state machine implementation of a real-time controller (e.g., RTL Verilog code), and a timing diagrams (TDs) specification, the question we wish to answer is whether the controller satisfies this specification. Our method uses constraint logic programming (CLP). The controller FSM is fed with input sequences derived from the assumption constraints on the inputs as stated in the TD, and its outputs are verified against the required timing (commit) constraints in the TD. Our technique considers all input sequences in one consistency check for each commit constraint, carried out on a system of constraints constructed from the TD and the unfolded controller FSM. The number of constraints is linear in the lengths of the intervals of the assumption constraints. The method was implemented in CLP (BNR) Prolog which is based on relational interval arithmetic (RIA). We verified a controller for an asynchronous bus.

We present an algorithm for automatically generating minimal test sets for parametric faults in linear analog circuits. In a previous work we elaborated a multifrequency test generation method (TPG) for such circuit faults. The method was formulated as a series of optimization problems that were solved by sequential quadratic programming (SQP) available in MATLAB. Such a standard optimization method processes local information and, consequently, cannot guarantee that the found solution is global. This may lead to a poor test selection. Furthermore, the method is semiautomatic and depends on various parameters that must be selected by an experienced user. In this paper, we propose a method based on constraint logic programming (CLP) using relational interval arithmetic (RIA) to solve these optimization problems as a series of constraint satisfaction problems (CSPs). The method is fully automatic and provides tight and guaranteed bounds on the true range of a multivariable nonlinear function. The correctness of the bounds stems from the enumeration of subdivisions of the function and its variable domains while discarding those subdivisions containing no solution. The tightness (i.e., the closeness to the true range) of the bounds can be refined to any desired degree by increasing the fineness of subdivisions imposed on the variable domains and the stringency of the termination criterion at the cost of an increased CPU time. The TPG method was implemented in CLP (BNR) prolog. The effectiveness of our approach is illustrated on a number of nonlinear functions known to be difficult, and two realistic electronic circuits in the context of TPG. Our algorithm accelerated the computation of the various parameters related to the test of a biquadratic filter by a factor ranging from 11 to 29 as compared to the Monte Carlo method.

This paper proposes a new testability analysis and test-point insertion method at the register transfer level (RTL), assuming a full scan and a pseudorandom built-in self-test design environment. The method is based on analyzing the RTL synchronous specification in synthesizable very high speed integrated circuit hardware descriptive language (VHDL). A VHDL intermediate form representation is first obtained from the VHDL specification and then converted to a directed acyclic graph (DAG) that represents all data dependencies and flow of control in the VHDL specification. Testability measures (TMs) are computed on this graph. The considered TMs are controllability and observability for each bit of each signal/variable that is declared or may be implied in the VHDL specification. Internal signals of functional modules (FMs) such as adders and comparators are also analyzed to compute their controllability and observability values. The internal signals are obtained by decomposing at the RTL large FMs into smaller ones. The calculation of TMs is carried out at a functional level rather than the gate level, to reduce or eliminate errors introduced by ignoring reconvergent fanouts in the gate network, and to reduce the complexity of the DAG construction. Based on the controllability/observability values, test-point insertion is performed to improve the testability for each bit of each signal/variable. This insertion is carried out in the original VHDL specification and thus becomes a part of it unlike in other existing methods. This allows full application of RTL synthesis optimization on both the functional and the test logic concurrently within the designer constraints such as area and delay. A number of benchmark circuits were used to show the applicability and the effectiveness of our method in terms of the resulting testability, area, and delay.

In this paper, we present several techniques for modeling and formal verification of the Fairisle asynchronous transfer mode (ATM) switch fabric using multiway decision graphs (MDGs). MDGs represent a new class of decision graphs which subsumes Bryant's reduced ordered binary decision diagrams (ROBDDs) while accommodating abstract sorts and uninterpreted function symbols. The ATM device we investigated is in use for real applications in the Cambridge University Fairisle network. We modeled and verified the switch fabric at three levels of abstraction: behavior, and register transfer level (RTL) and gate levels. In a first stage, we validated the high-level specification by checking specific safety properties that reflect the behavior of the fabric in its real operating environment. Using the intermediate abstract RTL model, we hierarchically completed the verification of the original gate-level implementation of the switch fabric against the behavioral specification. Since MDGs avoid model explosion induced by data values, this work demonstrates the effectiveness of MDG based verification as an extension of ROBDD-based approaches. All the verifications were carried out automatically in a reasonable amount of CPU time.

Waveform narrowing is an attractive framework for circuit delay verification as it can handle different delay models and component delay correlation efficiently. The method can give false negative results because it relies on local consistency techniques. We present two methods to reduce this pessimism: (1) global timing implications and necessary assignments, and (2) a case analysis procedure that finds a test vector that violates the timing check or proves that no violation is possible. Under floating-mode, global implications eliminate timing check violation without case analysis in the c1908 benchmark, while for a tighter requirement case analysis finds a test vector after only 5 backtracks.

Multiway Decision Graphs (MDGs) have been recently proposed as an efficient verification tool for RTL designs based on an efficient representation mechanism. In MDG, a data value is represented by a single variable of abstract sort, and a data operation is represented by an uninterpreted function symbol. In this work we investigate the non-termination problem of MDG-based verification. We present a novel approach to dealing with the problem based on retiming and circuit transformations that preserve the behaviour of the circuit. We demonstrate the effectiveness of our method on the example of the Island Tunnel Controller (ITC).

Specifications containing linear timing constraints, such as found in action diagrams (timing diagrams) defining interface behaviors, are often used in practice. Although efficient O(n 3 ) shortest path algorithms exist for computing the minimum and maximum time distances between actions, subject to the timing constraints, there is so far no accurate method that can decide (a) whether a specification of this kind is realizable (i.e., can be simulated by a causal system), and (b) given the action diagrams of the interfaces of two or more communicating systems, whether the systems implementing such independent specifications will correctly interoperate (i.e., satisfy the respective protocols and timing assumptions). First we illustrate the weakness of existing action diagram verification techniques: the causality issue is not addressed, and the proposed methods to answer the compatibility (interoperability) question yield false negative answers in many practical situations. We then define the meaning of causality in an action diagram specification and state a set of sufficient conditions for causality to hold. This development then leads to an exact procedure for the verification of the interface compatibility of communicating action diagrams. the results are illustrated on a practical example.

In our previous work we elaborated a multifrequency test generation method (TPG) for detecting parametric and catastrophic faults in linear analog circuits. The method was formulated as an optimization problem which was solved by Sequential Quadratic Programming (SQP), a non-linear programming method available in MATLAB. Such standard optimization methods are based on and process local information and consequently cannot guarantee a global optimum. In this paper we propose a method based on Constraint Logic Programming (CLP) that solves the optimization problem in TPG as a series of Constraint Satisfaction Problems (CSPs). Our TPG method is fully automatic and provides right and guaranteed bounds on the global optima of a nonlinear function. The TPG method was implemented in CLP(BNR) Prolog. First, we illustrate the effectiveness of our approach on a number of nonlinear functions known to be difficult, and then we apply it to a realistic electronic circuit in the context of TPG. The two methods produce the same results except for one case where SQP falls into a local minimum. This could lead to a wrong test selection. Moreover, while the TPG took over a week of work using SQP, it was solved in a matter of minutes using CLP.

In this paper we present our results on formally verifying the implementation of an asynchronous transfer mode (ATM) network switching fabric using a new class of decision graphs, called Multiway Decision Graphs (MDG). The design we consider is in use for real applications in the Cambridge Fairisle network. We produced the description of the hardware implementation at different levels of abstraction. We then performed the verification of an abstract description model against the description of the gate-level implementation. Using this abstract model, we accomplished the verification of specific properties that reflect the behavior of the Fairisle ATM switch fabric.

We investigate equivalence checking of the RTL hardware implementation of the Cambridge Fairisle Asynchronous Transfer Mode (ATM) 4 by 4 switch fabric against a high-level behavioral specification which has unrestricted frame size, cell length and word width. The verification is based on the reachability analysis of the product machine of the implementation and the specification, both modeled as Abstract State Machines (ASM). Multiway Decision Graphs (MDG) are used to encode both the output and transition relations of the ASMs and of the set of reachable abstract states, allowing implicit abstract state enumeration. Since MDGs avoid model explosion induced by data values, this experiment demonstrates the effectiveness of MDG-based verification as an extension of ROBDD-based approaches.

We propose a new efficient constraint generation technique for 2-D mask compaction based on Branch-and-Bound Optimization (BBO). To assure separation in X and Y between rectangles in a layout, we generate the so called "diagonal" constraints in addition to the usual simple constraints in the X and Y directions. A diagonal constraint consist of two constraints, one in each dimension. Our method determines areas around the rectangles beyond which the diagonal (and the simple) constraints need not be generated, producing thus a nearly irredundant system of constraints. During BBO, the diagonal constraints are treated as dual constraints, in which case, one of the two component constraints of the dual can be deactivated. When a such constraint is deactivated, few additional constraints must be be added to assure a legal layout. The overall performance is still considerably improved, because there are fewer dual constraints. Proofs of sufficiency are based on a novel characterization of the 2-D constraint structure.

We present a fast recursive technique for estimating lower-bound performance of data path schedules. The method relies on the determination of an ASAPUC a(s Soon As Possible Under Constraint) time-step value for each node of the DFG (Data-Flow Graph) that is based on the ASAPUC values of its predecessor nodes. That is, the lower-bound estimation is applied to each subgraph permitting the derivation of a tight lower bound on the performance of the complete DFG. Applying the greedy lower-bound estimator of Rim and Jain [1994] to each subgraph improves the complete lower bound in more than 50% of the experiments reported in Rim and Jain [1994], and the CPU time is only about twice as long. The recursive methodology can be extended to exploit other lower-bound techniques, for example, considering other constraints such as the number of busses or registers.

Multiway Decision Graphs (MDGs) have been recently proposed as an efficient representation of Extended Finite State Machines (EFSMs), suitable for automatic hardware verification of Register Transfer Level (RTL) designs. We report here on the results of our research into automatic partitioning of state transition relations described using MDGs. The objective is to achieve the maximum possible performance during an abstract implicit state enumeration procedure that is at the basis of our automatic verification method.

In this paper we address the behavioral modeling of cell processing hardware (e.g., packet/ATM switching systems). We propose a modeling methodology, Action Diagrams, in which the timing and protocol aspects are specified in a nearly "orthogonal" way to the data manipulation aspects, while maintaining the links between the two. We show the novel aspects of this specification paradigm and we illustrate its use on cell processing applications.>

A new approach to fault analysis is presented. The authors consider multiple stuck-at-0/1 faults at the gate level. First, a fault collapsing phase is applied to the network, so that equivalent faults are eliminated. During the analysis the authors consider frontier faults where there is at least a normal path from each faulty line to a primary output. It is shown that the set of frontier faults is equivalent to the set of multiple faults. Given an input vector, the authors evaluate the fault-free circuit and then propagate fault effects. Assuming that fault-free response is observed, a fault-dropping procedure is then applied to eliminate faulty conditions on lines, that are either absent or may be hidden by other faulty conditions. This method is applied to some benchmark circuits and achieves a high degree of efficiency.>

The early study of fault tolerance in efficient sorting networks only achieved single-fault tolerance. By eliminating critical comparators, L. Rudolph (1985) presented a 1-fault tolerant design of the balanced sorting network (BSN) at the cost of one redundant stage of N/2 comparators and two permuters external to the network. In this paper, we show, however, that 1-fault tolerance of BSN can be achieved without introducing redundancy and external permuters. Furthermore, we provide solutions to the open question of how to achieve multiple-fault tolerance in BSN. We analyze the problem from a higher-level by introducing a new concept of critical stages, and find that all stages in previous designs are critical. A 2-fault tolerant design of BSN is then discovered after eliminating its critical stages. The new design has a similar network architecture (i.e., a multistage network with the output recirculated back to the input) and the same hardware cost as Rudolph's, but it has many distinguished features. The performance analysis shows that the new designs achieve much higher probabilities of correct sorting in the presence of faulty comparators than the previous reported designs.>

Presents a fast recursive technique for estimating a lower-bound performance of data path schedules. The method relies on the determination of an ASAPUC (as soon as possible under constraint) time-step value for the root of the DFG (data flow graph) that is based on the ASAPUC values of its predecessor nodes, etc., until the leaf nodes are reached where this value becomes the regular ASAP value. The method computes a tighter lower-bound than the greedy technique and is only two times slower on the same benchmarks. Synthesis methods that depend on the exploration of the solution space directed by a lower-bound estimation, such a local microcode generation and behavioral synthesis, can benefit from our method. This is because bad solutions can be pruned earlier. We illustrate this dramatic effect on the reduction of the search space during the synthesis of an optimal microcode sequence for the elliptic wave filter benchmark and a fixed data path (containing a multiport RAM and a ROM).>

The author generalizes a transformation of the composition of two relations introduced earlier and then illustrates its use by analyzing the problem of I/O trace set inclusion of two synchronous nondeterministic finite-state machines. It is shown that the expression describing the inclusion of sets of traces can be transformed into a polynomial-time algorithm verifying a simulation relation, if the larger machine is k-step observably nondeterministic, i.e., a machine in which the selection of the next state can be identified by observing distinct I/O sequences of length of up to k.>

The relationship between switch-level circuit models and the linear electric circuits from which they are abstracted is investigated. This is important in determining the accuracy and consistency of switch-level simulation programs. A precise definition of magnitude or strength classes is presented, which leads to exact bounds on the accuracy of resistance and voltage calculations with magnitude classes relative to the corresponding linear calculations. The results indicate that the potential of switch-level simulators to provide accurate results is far less than was previously thought.>

The authors present a tool that captures timing specifications from hierarchical timing diagrams and models them using hierarchical constraint graphs. The main contribution of the present work is a novel algorithm that traverses the graph during simulation to generate stimuli and to validate circuit responses. The system, implemented in VHDL (VHSIC hardware description language), interacts with the circuit during simulation, thus allowing the generation of stimuli that depend on circuit responses. Experimental results are presented, and areas of future work are identified, such as the extension of the model to include inter-TD constraints, conditional execution semantics, and early firing events.>

The conditions under which a conjunction of two relations aR/sub 1/b and bR/sub 2/c with existential abstraction of b can be transformed into an implication aR/sub 1/b to bR/sub 2/c with universal abstraction of b are determined. In algorithmic design verification based on tautology checking and automata equivalence this transformation allows one to derive new verification algorithms, and to show under which conditions the breadth-first symbolic reachability algorithm used in proving automata equivalence can be applied when the automata are nondeterministic. Boolean characteristic functions of relations that have efficient representation using binary decision diagrams are used in the derivations.>

An efficient recursive technique for computing the Elmore delay in series-parallel resistance-capacitance (RC) networks is presented. The time complexity of the algorithm is on the order of the number of resistors times the number of nodes to which the delay has to be computed. In this respect it is superior to other known methods, particularly to that of P.K. Chan Karplus. Although that algorithm is more general, the present method should be attractive given the fact that many VLSI MOS circuits are based on design styles which are restricted to series-parallel transistor networks, which, in particular, exclude bridges. A special type of series-parallel RC circuit occurs in interconnection networks driven by multiple sources. A variation on the first algorithm, which is especially useful in a hierarchical simulator, is presented for computing the Elmore delay in such networks.>

A novel method is described for verifying the equivalence between a combinational circuit and its specification, when both are given in a modular (e.g., factored) form. It is based on the notion of cross-controllability and cross-observability relations that exist between the internal logic values across a cut of the joint composition of the circuit and the specification. It is proven that even after abstracting input and other internal variables the relations are sufficient to verify the equivalence. The abstraction allows reduction of the size of the relation, thus permitting the verification of much larger circuits. A report is presented on the verification of an 8*8 parallel multiplier using at most 527 BDD (binary decision diagram) cells of 21 variables. Extensions to sequential circuits are also discussed.>

The relationship between switch-level circuit models and the linear electric circuits from which they are abstracted were investigated. This is important in determining the accuracy and consistency of switch-level simulation programs. A precise new definition of magnitude or strength classes is presented, which leads to exact bounds on the accuracy of resistance and voltage calculations with magnitude classes relative to the corresponding linear calculations. The applicability to switch-level networks of standard solution methods for linear networks, including Gaussian elimination and Jacobi iteration, is also examined. The results indicate that the potential of switch-level simulators to provide accurate results is far less than previously thought.>

A scheme for fault-tolerant triangular cellular interconnection networks is proposed. A fault model is defined which unifies the concept of usable and unusable faulty components. An algorithm for testing these networks with a minimal number of tests (8) is presented. This result is extended to other cellular networks. A constant number of tests independent of the network size (at most 8) is added, in order to locate the faulty cell in the triangular cellular interconnection networks. Then, by considering networks of n+2 instead of n inputs/outputs, any single faulty cell can be tolerated. Neither the complexity of the cell nor that of the links is increased. The programming of the fault tolerant network is of the same complexity as that of the fault-free network and the relative silicon area overhead decreases with n and is proportional to 4/n.>

An algebraic methodology for comparing switch-level circuits with higher-level specifications is presented. Switch-level networks, 'user' behavior, and input constraints are modeled as asynchronous machines. The model is based on the algebraic theory of characteristic functions (CF). An asynchronous automation is represented by a pair of CFs, called a dynamic CF (DCF): the first CF describes the potential stable states, and the second CF describes the possible transitions. The set of DCFs is a Boolean algebra. Machine composition and internal variables abstraction correspond, respectively, to the product and sum operations of the algebra. Internal variables can be abstracted under the presence of a domain constraint. The constraint is validated by comparison to the outside behavior. The model is well suited for speed-independent circuits for which the specification is given as a collection of properties. Verification reduces to the validation of Boolean inequalities.>

The switch-level abstraction of digital MOS circuits has been used primarily in simulators. In formal verification, a functional description must be first extracted from the switch network. It is shown here how the theory of characteristic functions can be applied to analyze such networks and to extract their functional description.>

We present an approach to the integration of VLSI CAD tools through the uniformization of interactions with design cells at both the user and the program levels. The integration model is based on the concept of objects applied to circuit cells. User interactions are achieved through a desk-top-like graphics interface. Regrouping of related or equivalent cell-objects into tissues represented by a generic cell helps with their management. Late binding of specific version cells then encourages exploration of the design space. To test the integration concept, a data base and tools for symbolic layout were developed.

Magnitude networks [1l, [2] have been used as a theoretical base for switch-level simulation of MOS VLSI circuits. We address in this paper the particular problem of evaluating the influence of switches in unknown state on the steady-state response of the network. A two-pass procedure based on local controllers attached to such switches is described and a hardware implementation is proposed which models magnitude networks as self-adjusting combinational circuits.

Communication protocol testing can be done with a test architecture consisting of remote Lower Tester and local Upper Tester processes. For real protocols, tests can be designed based on the formal specification of the protocol which uses an extended finite state machine model. The specification is transformed into a simpler form consisting of normal form transitions. It can then be modeled by a control and a data flow graph. The graphs are decomposed into subtours and data flow functions, respectively. Tests are designed by considering parameter variations of the input primitives of each data flow function and determining the expected outputs. The methodology gives complete test coverage of all data flow functions and control paths in the specification. Functional fault models are proposed for functions that are not formally specified.

The simulator described functions within an object-cell oriented design environment. Leaf and composite cells are treated as abstract data types (objects) and their definition within a design is recursive. The leaf cells are simulated at the switch level using a functional description of transistor groups in terms of decision diagrams. These diagrams are extracted during a preprocessing step.

This paper describes a novel approach to switch-level simulation of MOS circuits. The circuit is first partitioned into connector-switch networks CSN [4]. Then each CSN is represented in terms of a decision diagram DD, which is particularly suitable for use in simulators. The advantages of DD's are that they are based on a solid theory and they permit fast evaluation of the network's response to any input vector. The CSN's are coupled through a 3-state automaton representing charge wells associated with transistor gates.

It has been shown in the literature that C-testable iterative arrays have very simple test structures, independent of the length of the arrays. We show in this work that all C-testable arrays are also pI-testable, which is a property yielding, in many cases, rather simple built-in-testing structures, both for the test generator and for the response verifier.

Currently proposed and used schemes for built-in testing (B-I-T) use as test generators either binary counters (exhaustive testing), linear feedback shift registers (semiexhaustive testing), or ROM's containing the test vectors (prestored testing). The disadvantages of these methods have been discussed in [4], and a store-and-generate B-I-T arrangement was proposed as a compromise between the exhaustive and the prestored form of test generation. Unfortunately, no systematic method was given for producing tests.

Experience with the use of formal descriptions of communication services and protocols is described. The paper focuses on the experience of the authors with the extended state transition model which is proposed as a standard formal description technique (FDT) for the services and protocols in the OSI environment. The first part of the paper refers to various example specifications, including transport protocol and service specifications, and discusses the suitability of the specification method and possible extensions. In the remaining part, the use of such formal specifications during the phases of system design, implementation, and testing is described. Various approaches to protocol design validation, implementation, and assessment of implementations are discussed, with emphasis on the last point. The experience with several of these approaches is described in the paper, and further details may be found in the references.

The concept of binary decision trees is extended to include multiple output Boolean functions. A systematic and programmable method is then developed for the minimization of trees realizing multiple output incompletely specified functions. Further simplification of minimal trees can be achieved through state reduction methods to obtain subminimal decision algorithms. Possible physical realizations of decision trees and algorithms as well as their applications are discussed.

An extension of a methodology based on Boolean equations to fault detection in modular combinational networks is described. The resulting method allows for the use of cataloged module tests, and it is applicable under the single-faulty-module constraint. The conceptual and computational framework is rather simple, and it is independent of any particular data structure for representing Boolean functions.

A methodology based on the theory of Boolean equations has been developed which permits a unified approach to the analysis and synthesis of combinational logic circuits. The type of circuits covered by the approach includes both the classical loopless combinational networks as well as those that contain closed feedback loops and thus have internally a sequential character. To that end, a general multiple-output circuit represented by a Mealy-type machine is studied using characteristic equations (functions) that describe its internal structure. It is shown how behavioral properties of the circuit are reflected through the sosutions of these equations. Moreover, it is demonstrated that a multiple-output incompletely specified switching function is reaeized if a ≤ relation is satisfied between the corresponding charchteristic functions. This leads to a new unified outlook on functional decomposition as used in modular synthesis procedures. Although the building modules are allowed to be sequential circuits, it is shown under which conditions the feedback loops are redundant with respect to the realization of a given output characteristic function, and thus the existence conditions of nondegenerate combinational circuits with loops are stated.

This note presents an alternate approach to solving the inverse problem of logic by applying a decomposition technique based on Boolean equations.

A method has been investigated for the synthesis of memoryless logical networks using a restricted repertoire of functional modules. The method is based on the reduced general solution to a generalized system of Boolean equations (BE) as applied to the decomposition of Boolean functions. The aim of the synthesis is to obtain the most constrained circuit having at most two levels of gating. The constraints take the form of single input variables or constant logic levels applied to the inputs of the first level gate. This is achieved by assembling a set of constraint equations which are then a part of the generalized system of BE. The method is then tested on some synthesis examples of single and multiple output functions in terms of the NAND and (WOS) modules.