Todays SoCs are driving unprecedented verification complexity. The combination of billions of gates, system-level functionality on a chip, complex design methodologies like asynchronous clock domains and an explosion of untimed paths on a chip, interacting dynamic power domains, aggressive reset schemes etcetera could have been the perfect storm to staunch productivity. Instead it has turned out to be the mother of all necessities that has driven significant innovation in verification and brought about a paradigm shift. Static sign-off has proven to be a pillar in this new paradigm. This talk will discuss the template for what has made static techniques successful in verifying modern SoCs. The recent successes are, in no small part, due to the FMCAD community that has pursued formal methods doggedly for decades despite glacial practical adoption. Complementing the efforts of the research community has been the equally determined pursuit in the EDA community to bring structure and automation into the verification process. Through this partnership, we have been able to bring about an analysis framework within which a combination of semantic analysis and formal methods enables a systematic verification process that leads to sign-off level confidence for important failure modes. It will be gratifying for the FMCAD audience to realize that SAT, model checking, functional abstraction, QBF etcetera have become essential in being able to tape out some of the most complex chips in the world on time and within budget. The adoption of IC3/PDR into the verification process was almost immediate. The recent successes represent a strong debut for static methods. What is the vision to extend the promise into bigger slices of the verification pie? System-level verification continues to be an art-form with very little of the automation, process and problem-framing that have proven successful in other domains. May be the FMCAD community should adopt that as its next major challenge.

Summary form only given. Application-based verification, i.e., partitioning the verification process by verification concerns, has become an important approach for managing verification complexity in the billion-transistor SoC. This new verification paradigm has truly come into focus with the proliferation of layers of complexity in an SoC beyond the baseline complexity of its constituent components. In a sense, the nature of chip complexity has shifted from how much goes into a chip to what goes into a chip. Given a narrow verification concern like clock-domain verification, power, dft, reset analysis etc, the specification, analysis and debug dimensions of the verification problem become meaningfully solvable. This is a new paradigm in a sense because it focuses technologists toward the development of complete solutions and closure for the problem at hand as a whole rather than on just nuts-and-bolts technologies like simulation and ABV. Static formal analysis is able to play a key role in this paradigm for various reasons. With the narrow focus on a specific verification problem, much of the specification becomes precise and implicit. In addition, the limited scope allows the formal analysis to be controlled and nominally tractable. Further, even when the formal analysis remains bounded, it is still possible to return actionable information to the user. Finally, debug becomes much more precise and actionable in the context of the narrow verification concern being addressed. These aspects all come to fore in the verification of clock domain crossings in the modern SoC. Used to be that a chip would have a handful of clock domains and the clock-domain checking could be done manually. With 100s of clocks domains on chip, that luxury is not available any more. No SoC gets taped out today without a dedicated sign-off of clock-domain crossings using verification tools specialized for this problem. Another reason clock-domain verification is good to highlight as an example of the new paradigm is that it is at the intersection of chip functionality and timing. This verification task cannot be completed by just functional simulation or just by static timing analysis. It needs a specialized solution, with static formal analysis at its core, to do justice to it.

This paper presents a lightweight interval analysis technique for determining the lower and upper bounds for program variables and its application in improving software model checking techniques. The experiments demonstrate that it is an effective approach to alleviate the state explosion problem in software model checking.

Model checking of safety properties has taken a significant lead over non-safety properties in recent years. To bridge the gap, we propose dedicated SAT-based model checking algorithms for properties beyond safety. Previous bounded model checking (BMC) approaches have relied on either converting such properties to safety checking, or finding proofs by deriving termination criteria using loop-free path analysis. Instead, our approach uses a customized SAT-based formulation for bounded model checking of non-safety properties, and determines the completeness bounds for liveness using unbounded SAT-based analysis. Our main contributions are: 1) Customized property translations for LTL formulas for BMC, with novel features that utilize partitioning, learning, and incremental formulation. Customized translations not only improve the BMC performance significantly in comparison to standard monolithic LTL translations, but also allow efficient derivation and use of completeness bounds. Though we discuss the translation schemas for liveness, they can be easily extended to handle other LTL properties as well. 2) Customized formulations for determining completeness bounds for liveness using SAT-based unbounded model checking (UMC) rather than using loop-free path analysis. These formulations comprise greatest fixed-point and least fixed-point computations to efficiently handle nested properties using SAT-based quantification approaches. We show the effectiveness of our overall approach for checking liveness on public benchmarks and several industry designs.

We describe verification techniques for embedded memory systems using efficient memory modeling (EMM), without explicitly modeling each memory bit. We extend our previously proposed approach of EMM in bounded model checking (BMC) for a single read/write port single memory system, to more commonly occurring systems with multiple memories, having multiple read and write ports. More importantly, we augment such EMM to providing correctness proofs, in addition to finding real bugs as before. The novelties of our verification approach are in (a) combining EMM with a proof-based abstraction that preserves the correctness of a property up to a certain analysis depth of SAT-based BMC, and (b) modeling arbitrary initial memory state precisely and thereby providing inductive proofs using SAT-based BMC for embedded memory systems. Similar to the previous approach, we construct a verification model by eliminating memory arrays, but retaining the memory interface signals with their control logic and adding constraints on those signals at every analysis depth to preserve the data forwarding semantics. The size of these EMM constraints depends quadratically on the number of memory accesses and the number of read and write ports; and linearly on the address and data widths and the number of memories. We show the effectiveness of our approach on several industry designs and software programs.

We describe an efficient approach for SAT-based quantifier elimination that significantly improves the performance of pre-image and fixed-point computation in SAT-based unbounded symbolic model checking (UMC). The proposed method captures a larger set of new states per SAT-based enumeration step during quantifier elimination, in comparison to previous approaches. The novelty of our approach is in the use of circuit-based cofactoring to capture a large set of states, and in the use of a functional hashing based simplified circuit graph to represent the captured states. We also propose a number of heuristics to further enlarge the state set represented per enumeration, thereby reducing the number of enumeration steps. We have implemented our techniques in a SAT-based UMC framework where we show the effectiveness of SAT-based existential quantification on public benchmarks, and on a number of large industry designs that were hard to model check using purely BDD-based techniques. We show several orders of improvement in time and space using our approach over previous CNF-based approaches. We also present controlled experiments to demonstrate the role of several heuristics proposed in the paper. Importantly, we were able to prove using our method the correctness of a safety property in an industry design that could not be proved using other known approaches.

Bounded Model Checking (BMC) based on Boolean Satisfiability (SAT) procedures has recently gained popularity as an alternative to BDD-based model checking techniques for finding bugs in large designs. In this paper, we explore the use of learning from BDDs, where learned clauses generated by BDD-based analysis are added to the SAT solver, to supplement its other learning mechanisms. We propose several heuristics for guiding this process, aimed at increasing the usefulness of the learned clauses, while reducing the overheads. We demonstrate the effectiveness of our approach on several industrial designs, where BMC performance is improved and the design can be searched up to a greater depth by use of BDD-based learning.

Resolution-based proof analysis techniques have been proposed recently to identify a sufficient set of reasons for unsatisfiability derived by a CNF-based SAT solver. We have adapted these techniques to work with a hybrid SAT solver. We use the proof analysis technique with SAT-based BMC, in order to, generate useful abstract models. Our abstraction procedure is used iteratively in a top-down framework, starting from the concrete design, where we apply BMC on increasingly more abstract models. We apply various SAT-based and BDD-based verification methods on these abstract models, in order to obtain proofs of correctness, or to perform deeper searches for counterexamples. We demonstrate the effectiveness of our prototype implementation on several large industry designs.

We introduce a novel approach to accelerating functional simulation. The key attributes of our approach are high-performance, low-cost, scalability and low turn-around-time (TAT). We achieve speedups between 25 and 2000x over zero delay event-driven simulation and between 75 and 1000x over cycle-based simulation on benchmark and industrial circuits while maintaining the cost, scalability and TAT advantages of simulation. Owing to these attributes, we believe that such an approach has potential for very wide deployment as replacement or enhancement for existing simulators. Our technology relies on a VLIW-like virtual simulation processor (SimPLE) mapped to a single FPGA on an off-the-shelf PCI board. Primarily responsible for the speed are (i) parallelism in the processor architecture (ii) high pin count on the FPGA enabling large instruction bandwidth and (iii) high speed (124 MHz on Xilinx Virtex-II) single-FPGA implementation of the processor with regularity driven efficient place and route. Companion to the processor is the very fast SimPLE compiler which achieves compilation rates of 4 million gates/hour. In order to simulate the netlist, the compiled instructions are streamed through the FPGA, along with the simulation vectors. This architecture plugs in naturally into any existing HDL simulation environment. We have a working prototype based on a commercially available PCI-based FPGA board.

We propose Satisfiability Checking (SAT) techniques that lead to a consistent performance improvement of up to 3x over state-of-the-art SAT solvers like Chaff on important problem domains in VLSI CAD. We observe that in circuit oriented applications like ATPG and verification, different software engineering techniques are required for the portions of the formula corresponding to learnt clauses compared to the original formula. We demonstrate that by employing the same innovations as in advanced CNF-based SAT solvers, but in a hybrid approach where these two portions of the formula are represented differently and processed separately, it is possible to obtain the consistently highest performing SAT solver for circuit oriented problem domains. We also present controlled experiments to highlight where these gains come from. Once it is established that the hybrid approach is faster, it becomes possible to apply low overhead circuit-based heuristics that would be unavailable in the CNF domain for greater speedup.

Design validation and verification is the process of ensuring correctness of a design described at different levels of abstraction during the design process. Design validation is the main bottleneck in improving design turnaround time. Currently, simulation is the primary methodology for validation of the first description of a design. In this paper we integrate directed search methods and observability-based code coverage metric (OCCOM) computation into an algorithm for generating test vectors under OCCOM for sequential HDL models. A prototype system for design validation under OCCOM has been built. The system uses repeated coverage computation to minimize the number of vectors generated. Experimental results using the test vector generation system are presented.

In this paper, we present a new technique for the efficient dynamic detection and removal of inactive clauses, i.e. clauses that do not affect the solutions of interest of a Boolean Satisfiability (SAT) problem. The algorithm is based on the extraction of gate connectivity information during generation of the Boolean formula from the circuit, and its use in the inner loop of a branch-and-bound SAT algorithm. The motivation for this optimization is to exploit the circuit structure information, which can be used to find unobservable gates at circuit outputs under dynamic conditions. It has the potential to speed up all applications of SAT in which the SAT formula is derived from a logic circuit. In particular, we find that it has considerable impact on an image computation algorithm based on SAT. We present practical results for benchmark circuits which show that the use of this optimization consistently improves the performance for reachability analysis, in some cases enabling the prototype tool to reach more states than otherwise possible.

A practical solution to the complexity of design validation is semi-formal verification, where the specification of correctness criteria is done formally, as in model checking, but checking is done using simulation, which is guided by directed vector sequences derived from knowledge of the design and/or the property being checked. Simulation vectors must be effective in targeting the types of bugs designers expect to find rather than some generic coverage metrics. The focus of our work is to generate property-specific testbenches for guided simulation, that are targeted either at proving the correctness of a full CTL property or at finding a bug. This is facilitated by generation of a property-specific model, called a "witness graph", which captures interesting paths in the design. Starting from an initial abstract model of the design, symbolic model checking, pruning, and refinement steps are applied in an iterative manner, until either a conclusive result is obtained or computing resources are exhausted. The witness graph is annotated with, e.g., state or transition priorities before testbench generation. The overall testbench generation flow, and the iterative flow for witness graph generation are shown.

Methods based on Boolean satisfiability (SAT) typically use a conjunctive normal form (CNF) representation of the Boolean formula, and exploit the structure of the given problem through use of various decision heuristics and implication methods. We propose a new decision heuristic based on separator-set induced partitioning of the underlying CNF graph. It targets those variables whose choice generates clause partitions with disjoint variable supports. This can potentially improve performance of SAT applications by decomposing the problem dynamically within the search. In the context of a recently proposed image computation method combining SAT and BDDs, this results in simpler BDD subproblems. We provide algorithms for CNF partitioning - one based on a clause-variable dependency matrix, and another based on standard hypergraph partitioning techniques, and also for the use of partitioning information in decision heuristics for SAT. The effectiveness of the proposed partition-based heuristic is shown with practical results for reachability analysis of benchmark sequential circuits.

This article introduces the notion of a Complete-1-Distinguishability (C-1-D) property for simplifying equivalence checking of finite state machines (FSMs). When a specification machine has the C-1-D property, the traversal of the product machine can be eliminated. Instead, a much simpler check suffices. The check consists of first obtaining a 1-equivalence mapping between the individually reachable states of the specification and the implementation machines, and then checking that it is a bisimulation relation. The C-1-D property can be used directly for specification machines on which it naturally holds---a condition that has not been exploited thus far in FSM verification. We also show how this property can be enforced on an arbitrary FSM by exposing some of its latch outputs as pseudo-primary outputs during synthesis and verification. In this sense, our synthesis/verification methodology provides another point in the trade-off curve between constraints-on-synthesis versus complexity-of-verification. Practical experiences with this methodology have resulted in success with several examples for which it is not possible to complete verification using existing implicit state space traversal techniques.

Validation of RTL circuits remains the primary bottleneck in improving designturnaround time, and simulation remains the primary methodology for validation. Simulation-based validation has suffered from a disconnect between the metrics used to measure the error coverage of a set of simulation vectors, and the vector generation process. This disconnect has resulted in the simulation of virtually endless streams of vectors which achieve enhanced error coverage only infrequently. Another drawback has been that most error coverage metrics proposed have either been too simplistic or too inefficient to compute. Recently, an effective observability-based statement coverage metric was proposed along with a fast companion procedure for evaluating it. The contribution of our work is the development of a vector generation procedure targeting the observability-based statement coverage metric. Our method uses repeated coverage computation to minimize the number of vectors generated. For vector gen...

Design rule checking (DRC) is an important step in VLSI design in which the widths and spacings of design features in a VLSI circuit layout are checked against the design rules of a particular fabrication process. In the past, some efforts to build hardware accelerators for DRC have been proposed, but these efforts were hobbled by the fact that it is often impractical to build a different rule-checking ASIC each time design rules or fabrication processes change. In this paper, we propose a configurable hardware approach to DRC. Because the rule-checking is built in configurable hardware, it can garner impressive speedups over software approaches, while retaining the flexibility needed to easily change the rule checker as rules or processes change. Our work proposes an edge-endpoints-based method for performing Manhattan geometry checking; this approach is particularly well-suited to the constraints of configurable hardware. Although design rules do change over time, their intrinsic similarity allows us to propose a general scalable architecture for DRC. We then demonstrate our approach by applying this architecture to a set of design rules for the MOSIS SCN4N SUB process. The hardware required per rule is quite small; we have implemented several design rule checks within a single Xilinx XC4013 FPGA. Our hardware, implemented on a Pamette board, runs at a clock rate of 33 MHz. We also compare the performance of our approach to software methods and demonstrate overall speedups in excess of 25X.

We propose a novel procedure based on uninterpreted symbolic simulation for checking the scheduling step in high-level synthesis. The primary task in scheduling is the assignment of time steps or, equivalently, states to operations. Various transformations like operation reordering and loop unrolling may be performed in the process to meet the optimization criteria. The contribution of our proposal lied in its ability to efficiently handle loops and a wide range of loop transformations performed during scheduling. Our algorithm is based on loop invariant extraction using a combination of uninterpreted symbolic simulation and induction techniques. In spite of its wide scope, our procedure is relatively complete and practical. This work is a part of our effort to provide a suite of techniques for verifying the various steps involved in the high-level synthesis process. It is being implemented in an in-house verification system for checking equivalence of designs generated from high-level specifications through successive refinements. We present case studies to demonstrate the applicability of our approach. These case studies consist of examples where equivalence cannot be established using conventional FSM-based methods. By providing a viable automated equivalence checking technique for such examples, we improve on the state of the art.

The issues of software compute time and complexity are very important in current computer-aided design (CAD) tools. As field-programmable gate array (FPGA) speeds and densities increase, the opportunity for effective hardware accelerators built from FPGA technology has opened up. This paper describes and evaluates a formula-specific method for implementing Boolean satisfiability solver circuits in configurable hardware. That is, using a template generator, we create circuits specific to the problem instance to be solved. This approach yields impressive runtime speedups of up to several hundred times compared to the software approaches. The high performance comes from realizing fine-grained parallelism inherent in the clause evaluation and implication and from direct mapping of Boolean relations into logic gates. Our implementation uses a commercially available hardware system for proof of concept. This system yields more than 100 times run-time speedup on many problems, even though the clock rate of the hardware is 100 times slower than that of the workstation running the software solver. While the time to compile the solver circuit to configurable hardware can he quite long on current platforms (20-40 min per chip), this paper discusses new approaches to overcome this compilation overhead. More broadly, we view this work as a case study in the burgeoning domain of high performance configurable computing. Our approach realizes large amount of fine-grained parallelism, and has broad applications in the very large scale integration CAD area.

The Boolean satisfiability problem lies at the core of several CAD applications, including automatic test pattern generation and logic synthesis. This paper describes and evaluates an approach for accelerating Boolean satisfiability using configurable hardware. Our approach harnesses the increasing speed and capacity of field-programmable gate arrays by tailoring the SAT-solver circuit to the particular formula being solved. This input-specific technique gets high performance due both to (i) a direct mapping of Boolean operations to logic gates, and (ii) large amounts of fine-grain parallelism in the implication processing. Overall, these strategies yields impressive speedups (>200X in many cases) compared to current software approaches, and they require only modest amounts of hardware. In a broader sense, this paper alerts the hardware design community to the increasing importance of input-specific designs, and documents their promise via a quantitative study of input-specific SAT solving.

This paper describes and evaluates methods for implementing formula-specific Boolean satisfiability (SAT) solver circuits in configurable hardware. Starting from a general template design, our approach automatically generates VHDL for a circuit that is specific to the particular Boolean formula being solved. Such an approach tightly customizes the circuit to a particular problem instance. Thus, it represents an ideal use for dynamically-reconfigurable hardware, since it would be impractical to fabricate an ASIC for each Boolean formula being solved. Our approach also takes advantage of direct gate mappings and large degrees of fine-grained parallelism in the algorithm's Boolean logic evaluations. We compile our designs to two hardware targets: an IKOS logic emulation system, and Digital SRC's Pamette configurable computing board. Performance evaluations on the DIMACS SAT benchmark suite indicate that our approach offers speedups from 17X to more than a thousand times. Overall, this SAT solver demonstrates promising performance speedups on an important and complex problem with extensive applications in the CAD and AI communities.

We propose a complete procedure for verifying register-transfer logic against its scheduled behavior in a high-level synthesis environment Our proposal advances the state of the art because it is the first such verification procedure that is both complete and practical.Hardware verification is known to be a hard problem and the proposed verification technique leverages off the fact that highlevel synthesis -performed manually or by means of high-level synthesis software -proceeds from the algorithmic description of the design to structural RTL through a sequence of very well defined steps, each limited in its scope.The major contribution is the partitioning of the equivalence checking task into two simpler subtasks, verifying the validity of register sharing, and verifying correct synthesis of the RTL interconnect and control.While state space traversal is unavoidable for verifying validity of the register sharing, we automatically abstract out irrelevant portions oftbe design, significantly simpliQing the task that must be performed by a back-end model checker.The second task of verifying the RTL is not only shown to reduce to a combinational equivalence check,we present a novel and fast RTL technique for combinational equivalence check instead of using slower gate level techniques.The verification procedure has been applied to several large circuits, and is illustrated on the implementation of a sort algorithm.

The need to reduce the power consumption of the next generation of digital systems is clearly recognized at all levels of system design. At the system level, power management is a very powerful technique and delivers large and unambiguous savings. The ideas behind power management can be extended to the logic level. This would involve determining which parts of a circuit are computing results that will be used and which are not. The parts that are not needed are then "shut off". This paper describes an approach termed guarded evaluation, which is an implementation of this idea. A theoretical framework and the algorithms that form the basis of the approach are presented. The underlying idea is to automatically determine the parts of the circuit that can be disabled on a per-clock-cycle basis. This saves the power used in all the useless transitions in those parts of the circuit. Initial experiments indicate substantial power savings and the strong potential of this approach for a large number of benchmark circuits. While this paper presents the development of these ideas at the logic level of design, the same ideas have direct application at the register-transfer level of design also.

The biggest obstacle in the formal verification of large designs istheir very large state spaces, which cannot be handled even bytechniques such as implicit state space traversal. The only viablesolution in most cases is validation by functional simulation. Unfortunately, this has the drawbacksof high computationalrequirementsdue to the large number of test vectors needed, and the lack of adequate coverage measures to characterize the quality of a given testset. To overcome these limitations, there has been recent interest inhybrid techniques which combine the strengths of formal verification and simulation. Formal verification-based techniques are usedon a test model (usually much smaller than the design) to derive a setof functional test vectors, which are then used for design validationthrough simulation. The test set generated typically satisfies somecoverage measure on the test model. Recent research has proposedthe use of state or transition coverage. However, no effort has beenmade to relate these measures to the coverage of design errors. Furthermore, the derivation of the test model remains largely ad-hoc,with few formal guidelines.We demonstrate that under a given set of assumptions, transitiontours on test models can be used for complete validation of an implementation against a specification, for a large and important classof designs that includes many programmable/hardwired, general-purpose processors/DSPs. A by-product of this study is specificguidelines for deriving the test model, motivated by the requirement of providing complete coverage of all errors. We illustrate theapplication of our methodology on a pipelined implementation of the DLX processor.

Shut-down" techniques are effective in reducing the power dissipation of logic circuits.Recently, methods have been developed that identify conditions under which the output of a module in a logic circuit is not used for a given clock cycle.When these conditions are met, input latches for that module are disabled, thus eliminating any switching activity and power dissipation.In this paper, we introduce these power management techniques in behavioral synthesis.We present a scheduling algorithm which maximizes the "shut-down" period of execution units in a system.Given a throughput constraint and the number of execution units available, the algorithm first schedules operations that generate controlling signals and activates only those modules whose result is eventually used.We present results which show that this scheduling technique can save up to 40% in power dissipation.

This paper introduces the use of the Complete-1-Distinguishability (C-1-D) property for simplifying FSM verification. This property eliminates the need for a traversal of the product machine for the implementation and the specification. Instead, a much simpler check suffices. This check consists of first obtaining a 1-equivalence mapping between states of the two machines, and then checking that it is a bisimulation relation. The C-1-D property can be used directly on specifications for which it naturally holds a condition that has not been exploited thus far in FSM verification. We also show how this property can be enforced on arbitrary FSMs by exposing some of the latch outputs as pseudo-primary outputs during synthesis and verification. In this sense, our synthesis/verification methodology provides another point in the tradeoff curve between constraints-on-synthesis versus complexity-of-verification. Practical experiences with using this methodology have resulted in success with several examples for which it is not possible to complete verification using existing implicit state space traversal techniques.

This paper addresses the problem of speeding up functional (delay-independent) logic simulation for synchronous digital systems. The problem needs very little new motivation-cycle-based functional simulation is the largest consumer of computing cycles in system design. Most existing simulators for this task can he classified as being either event driven or levelized compiled-code, with the levelized compiled code simulators generally being considered faster for this task. An alternative technique, based on evaluation using branching programs, was suggested about a decade ago in the context of switch level functional simulation. However, this had very limited application since it could not handle the large circuits encountered in practice. This paper resurrects the basic idea present this technique and provides significant modifications that enable its application to contemporary industrial strength circuits. We present experimental results that demonstrate up to a 10X speedup over levelized compiled code simulation for a large suite of benchmark circuits as well as for industrial examples with over 40.000 gates.

This paper addresses the performance optimization problem for sequential logic circuits. It is shown how the notion of false paths, traditionally defined for combinational logic circuits, can be extended to the sequential context by considering the operation of the circuit over multiple clock-cycles. These multicycle false paths can be removed from the circuit using techniques similar to those proposed for combinational logic circuits. This observation offers new techniques to improve the performance of sequential logic circuits. An implementation of an algorithm that uses these ideas shows significant performance improvement on some typical benchmark circuits at a modest area overhead.>

Paths that are never exercised are referred to as false paths and timing analysis that ignores the delay contribution of these paths is referred to as functional timing analysis. Such timing analysis provides a more accurate estimate of circuit delay compared to conventional static timing analysis. We show how unmodified conventional Automatic Test Pattern Generators (ATPG) for stuck-at faults can be used for functional timing analysis without sacrificing computational efficiency in comparison with existing approaches to the same problem. This is a significant result since it enables us to use the entire body of work in ATPG for this problem and relieves us from re-inventing new solutions for this problem. The basic algorithm can be used under an arbitrary delay model. We provide delay computation results for all the ISCAS benchmark examples under the unit-delay and the mapped-delay models.>

Circuits that have an underlying acyclic topology are guaranteed to be combinational since feedback is necessary for sequential behavior. However, the reverse is not true, i,e., feedback is not a sufficient condition since there do exist combinational logic circuits that are cyclic. In fact, such combinational circuits occur often in bus structures in data paths. This class of circuits has largely been ignored by conventional combinational single-stuck-at fault test pattern generators which assume that the circuit topology is acyclic. There has not been a formal study of the test generation problem for these circuits. Also, no algorithms and tools exist for this purpose. In practice, test generation for these circuits is handled in an awkward manner, typically with poor fault coverage. This work provides, for the first time, a formal analysis of the test generation problem for these circuits. This analysis leads to a clear insight into generation of tests, as well as a classification of untestable faults for such circuits. We demonstrate that cyclic combinational circuits may have untestable faults that do not correspond to redundancies. This insight is then translated to a testing algorithm which has been implemented in the program RAM. RAM has been successful in providing complete or near complete coverage on a range of typical examples, which is significantly higher than that provided by conventional techniques.>

The contribution of this paper is an implicit method for computing the minimum cost feedback vertex set for a graph.For an arbitrary graph, we efficiently derive a Boolean function whose satisfying assignments directly correspond to feedback vertex sets of the graph.Importantly, cycles in the graph are never explicitly enumerated, but rather, are captured implicitly in this Boolean function.This function is then used to determine the minimum cost feedback vertex set.Even though computing the minimum cost satisfying assignment for a Boolean function remains an NP-hard problem, we can exploit the advances made in the area of Boolean function representation in logic synthesis to tackle this problem efficiently in practice for even reasonably large sized graphs.The algorithm has obvious application in flip-flop selection for partial scan.Our algorithm was the first to obtain the MFVS solutions for many benchmark circuits.

The last couple of years have seen the addition of a new dimension in the evaluation of circuit quality -its power requirements.Low power circuits are emerging as an important application domain, and synthesis for low power is demanding attention.The research presented in this paper addresses one aspect of low power synthesis.It focuses on the problem of mapping a technology independent circuit to a technology specific one, using gates from a given library, with power as the optimization metric.Several issues in modeling and measuring circuit power, as well as algorithms for technology mapping for low power are presented here.Empirically, it is observed that a significant variation in the power consumption is possible Just by varying the choice of gates.Technology mapping for low power provides circuits with up to 24% lower power requirements than those obtained by technology mapping for area.

It is shown how the notion of false paths, traditionally defined for combinational logic circuits, can be extended to the sequential context by considering the operation of the circuit over multiple clock-cycles. Multicycle false paths can be removed from the circuit using techniques similar to those proposed for combinational logic circuits. This observation offers techniques to improve the performance of sequential logic circuits. A preliminary implementation of an algorithm that uses these ideas shows significant performance improvement on some typical benchmark circuits at a very modest area overhead.>

It is shown how general binary decision diagrams (BDDs), i.e., BDDs where input variables are allowed to appear multiple times along any path in the BDD, can be used to check for Boolean satisfiability. This satisfiability checking strategy is based on an input smoothing operation on general BDDs. Various input smoothing strategies for general BDDs are developed. In order to verify the equivalence of two functions f/sub 1/ and f/sub 2/, f/sub 1/(+)f/sub 2/ is checked for satisfiability. Using general BDDs different implementations of a 16*16 multiplier, a modified Achilles' heel function and a complex add-shift function were verified. It was not possible to construct OBDDs for any of the three functions.>

We investigate the gate-delay-fault testability properties of multilevel, multiplexor-based logic circuits. Based on this investigation, we describe a procedure for synthesizing gate-delay-fault testable multilevel circuits. The procedure involves the construction of a multilevel circuit from a general, unordered Binary Decision Diagram (BDD) by replacing vertices of the BDD with multiplexors. The procedure relies on the following result derived in this article: If the multilevel circuit constructed from the BDD is initially fully single stuck-at fault testable, or made fully single stuck-at fault testable by redundancy removal, then it is completely robustly gate-delay-fault testable. Once the initial gate-delay-fault testable circuit has been obtained, constrained algebraic factorization is used to improve the area and performance characteristics without compromising testability. Unlike previous techniques for synthesizing robustly gate-delay-fault testable circuits, this procedure can be used to synthesize fully testable circuits directly from nonflattenable, logic-level implementations.

Optimum and heuristic algorithms for the general decomposition of finite state machines (FSMs) such that the sum total of the number of product terms in the one-hot-coded and logic-minimized submachines is minimum or minimal are presented. This cost function is much more reflective of the area of an optimally state-assigned and minimized submachine than the number of states/edges in the submachine. The problem of optimum two-way FSM decomposition is formulated as one of symbolic output partitioning, and it is shown that this is an easier problem than optimum state assignment. A procedure of constrained prime implicant generation and covering that represents an optimum FSM decomposition algorithm, under the specified cost function, is described. It is shown that by means of this formulation, arbitrary decomposition topologies can be targeted by suitably modifying the constraints on the ability to encode during the covering. A novel iterative optimization strategy of symbolic implicant expansion and reduction, modified from two-level Boolean minimizers, that represents a heuristic algorithm based on the exact procedure is presented. Reduction and expansion are performed on functions with symbolic rather than binary-valued outputs. Preliminary experimental results that illustrate both the efficacy of the proposed algorithms and the validity of the selected cost function are presented.>

The authors develop optimal synthesis procedures for interacting nonscan sequential circuits composed of interacting finite state machines. For each of the different classes of redundancies, the authors define don't care sets, which if optimally exploited will result in the implicit elimination of any such redundancies in a given circuit. It is shown that notions of sequential don't cares and conditional compatibility are required to eliminate redundancies. Using a complex don't care set in an optimal sequential synthesis procedure of state minimization, state assignment, and combinational logic optimization results in fully testable single or interacting finite-state machines (FSMs). Preliminary experimental results indicate that irredundant sequential circuits can be synthesized with no area overhead and within reasonable CPU times with optimal logic synthesis.>

We present a unified framework and associated algorithms for the optimal decomposition and re-decomposition of sequential machines. This framework allows for a uniform treatment of arbitrary decomposition topologies operating at the State Transition Graph (STG) level, while targeting a cost function that is close to the eventual logic implementation. Previous work has targeted specific decomposition topologies via the formulation of decomposition as implicant covering with associated constraints. It is shown that this formulation can be used to target arbitrary desired topologies merely by customizing the constraints during implicant covering. It is shown how this work relates to preserved partitions and covers traditionally used in parallel and cascade decomposition, and how this formulation establishes the relationship between state assignment and FSM decomposition.In many cases, an initial decomposition is specified as a starting point. Attempting to flatten a set of interacting circuits into a single lumped STG in order to modify the decomposition structure could require astronomical amounts of CPU time and memory. Memory and CPU time efficient re-decomposition algorithms that operate on distributed-style specifications and which are more global than those presented in the past have been developed. These algorithms have been implemented in the sequential logic synthesis system, FLAMES, that is being developed at UCB/MIT.

Implicit state enumeration is used in developing strategies to solve key problems in sequential logic synthesis and test. It is shown that it is possible to extract implicit state transition graphs (ISTGs) from logic-gate and flip-flop descriptions of sequential circuits that allow equivalent states to be represented by cubes, and edges from different states to be coalesced into one, thereby decreasing significantly the CPU time and memory requirements of the extraction process. Coupled with the enumeration technique, synthesis strategies are proposed for FSMs (finite state machines) described at the logic level. As is illustrated, these synthesis strategies allow the authors to optimize large FSMs. The authors apply an ISTG traversal algorithm for verifying equivalence and detecting redundancies in logic-level sequential circuits. This algorithm is more efficient than previously developed sequential test generation algorithms when used to detect equivalent-state redundancies present in some classes of circuits.>

Sequential testability aspects in the decomposition of finite state machines (FSMs) are addressed. It is shown that the sequential testability of an FSM can be enhanced more easily when the machine is recognized to be, or is synthesized as, an interconnection of smaller machines. An exhaustive classification of redundant faults that can occur in a single FSM embedded in an interacting sequential circuit is presented. Associating each class of these redundant faults with a don't care set, a synthesis procedure is described that exploits the don't cares optimally to obtain an irredundant interacting sequential circuit with no area overhead. The synthesis procedure operates on a distributed-style representation of interacting state transition graphs (STGs), carrying out a series of local analyses. Insights into sequential logic synthesis improving on current optimization techniques for interacting sequential circuits are presented.>

The authors formulate the problem of optimum two-way finite-sole-machine (FSM) decomposition as one of symbolic-output partitioning and show that this is an easier problem than optimum state assignment. They describe a procedure of constrained prime-implicant generation and covering that represents an optimum FSM decomposition algorithm under the specified cost function. Exact procedures are not viable for large problem instances. The authors give a novel iterative optimization strategy of symbolic-implicant expansion and reduction, modified from two-level Boolean minimizers, that represents a heuristic algorithm based on their exact procedure. Reduction and expansion are performed on functions with symbolic, rather than binary-valued, outputs. Preliminary experimental results that illustrate both the efficacy of the proposed algorithms and the validity of the selected cost function.>

A control loop which maintains constant the magnitude of a transfer function is proposed. This loop is named the magnitude-locked loop (MLL). It is shown that it can perform most of the functions of the phase-locked loop. Several configurations can be chosen for the transfer function. The best, selected for its minimization of error, is presented.>