The authors propose a scalable abstraction-refinement method for model checking invariant properties on large sequential circuits, which is based on fine-grain abstraction and simultaneous analysis of all abstract counterexamples of the shortest length. Abstraction efficiency is introduced to measure for a given abstraction-refinement algorithm how much of the concrete model is required to make the decision. The fully automatic techniques presented in this paper can efficiently reach or come near to the maximal abstraction efficiency. First, a fine-grain abstraction approach is given to keep the abstraction granularity small by breaking down large combinational logic cones with Boolean network variables (BNVs) and then treating both state variables and BNVs as atoms in abstraction. Second, a refinement algorithm is proposed based on an improved Ariadne's bundle In the legend of Theseus, Ariadne's bundle contained one ball of thread to help Theseus navigate the labyrinth. In this paper, we work with multiple threads-hence, the "improved." of synchronous onion rings on the abstract model, through which the transitions contain all shortest abstract counterexamples. The synchronous onion rings are exploited in two distinct ways to provide global guidance to the abstraction refinement process. The scalability of our algorithm is ensured in the sense that all the analysis and computation required in our refinement algorithm are conducted on the abstract model. Finally, we derive sequential don't cares from the invisible variables and use them to constrain the behavior of the abstract model. We conducted experimental comparisons of our new method with various existing techniques. The results show that our method outperforms other counterexample-guided methods in terms of both run time and abstraction efficiency

Bounded Model Checking (BMC) relies on solving a sequence of highly correlated Boolean satisfiability (SAT) problems, each of which checks for the existence of counter-examples of a bounded length. The performance of SAT search depends heavily on the variable decision ordering. We propose an algorithm to exploit the correlation among different SAT problems in BMC, by predicting and successively refining a partial variable ordering. This ordering is based on the analysis of all previous unsatisfiable instances, and is combined with the SAT solver's existing decision heuristic to determine the final variable decision ordering. Experiments on real designs from industry show that our new method improves the performance of SAT-based BMC significantly.

Abstraction refinement is a key technique for applying model checking to the verification of real-world digital systems. In previous work, the abstraction granularity is often limited at the state variable level, which is too coarse for verifying industrial-scale designs. In this paper, we propose a finer grain abstraction in which intermediate variables are selectively inserted to partition large combinational logic cones into smaller pieces; these intermediate variables, together with the state variables, are then treated as "atoms" in abstraction refinement. With this fine-grain approach, refinement is conducted in two different directions, sequential and Boolean. We propose a SAT-based method for predicting the appropriate refinement direction, and apply greedy minimization in both directions to keep the refinement set small. We also explore the use of approximate reachable states of the remaining submodules to help verifying the abstract model. Experimental studies show that the proposed techniques significantly improve the performance of abstraction refinement, and therefore increase the model checker's ability to handle large designs.

We propose an abstraction refinement method for invariant checking, which is based on the simultaneous analysis of all abstract counter examples of shortest length in the current abstraction. The algorithm is focused on an improved Ariadne's Bundle/sup 1/ of SORs (Synchronous Onion Rings) of the abstract model; the transitions through these SORs contain all shortest ACEs (Abstract Counter Examples) and no other ACEs. The SORs are exploited in two distinct ways to provide global guidance to the abstraction refinement process: (1) Refinement variable selection is based on the entirety of transitions connecting the SORs, and (2) a SAT-based concretization test is formulated to test all ACEs in the SORs at once. We call this test multi-thread concretization. The scalability of our refinement algorithm is ensured in the sense that all the analysis and computation required in our refinement algorithm are conducted on the abstract model. The abstraction efficiency of a given abstraction refinement algorithm measures how much of the concrete model is required to make the decision. We include experimental comparisons of our new method with recently published techniques. The results show that our scalable method, based on global guidance from the entire bundle of shortest ACEs, outperforms these other methods in terms of both run time and abstraction efficiency.

A paradigm for automatic approximation/refinement in conservative CTL model checking is presented. The approximations are used to verify a given formula conservatively by computing upper and lower bounds to the set of satisfying states at each sub-formula. These approximations attempt to perform conservative verification with the least possible number of BDD variables and BDD nodes. We present new forms of operational graphs to avoid limitations associated with previously used operational graphs. Three new techniques for efficient automatic refinement of approximate system are presented. These methods make it easier to find the locality. We also present a new type of don't cares (approximate satisfying don't cares) that can make model checking more efficient in time and space. On average, an order of magnitude speedup was achieved.

An automatic abstraction/refinement algorithm for symbolic CTL model checking is presented. Conservative model checking is thus done for the full CTL language-no restriction is made to the universal or existen tial fragments. The algorithm begins with conserv ativ everification of an initial abstraction. If the conclusion is negativ e,it deriv es a “goal set” of states which require further resolution. It then successiv ely refines, with respect to this goal set, the appro ximations made in the sub-formulas, until the giv en form ula is v erified or computational resources are exhausted. This method applies uniformly to the abstractions based in over-appro ximation as well as under-approximations of the model. Both the refinement and the abstraction procedures are based in BDD-subsetting. Note that refinement procedures which are based on error traces, are limited to over-appro ximation on the universal fragment (or for language con tainment), whereas the goal set method is applicable to all consisten t appro ximations, and for all CTL formulas.

RDCs (Reachability Don’t Cares) can have a dramatic impact on the cost of CTL model checking [18]. Unfortunately, RDCs, being a global property, are often much more difficult to compute than the satisfying set of typical CTL formulas. We address this problem through the use of Approximate Reachability Don’t Cares (ARDCs), computed with the algorithms developed for the VERITAS sequential synthesis package [4, 5]. Approximate Reachable states represent an upper bound on the set of true reachable states, and thus a lower bound on the set of unreachable (Don’t Care) states. ARDCs can be 10X to 100X (or much more for very large circuits) cheaper to compute than RDCs, and in some cases have the same dramatic effect on CTL model checking as the real RDCs. We also discuss the application of ARDCs to the problem of exact computation of the RDCs themselves. Experiments on industrial benchmarks show that order of magnitude speedups are possible, and occur frequently. The experimental results presented strongly support our claim that ARDCs play a safe and important way out of a serious dilemma: RDCs are necessary for tractable model checking of many large circuits, but the computation of the RDCs themselves is often intractable. We include, and theoretically justify, significant extensions of the VERITAS algorithms, and show that they can be up to an order of magnitude faster, while computing a virtually identical upper bound. 1

This paper presents applications of algebraic decision diagrams (ADDs) to timing analysis and resynthesis for low power of combinational CMOS circuits. We first propose a symbolic algorithm to perform true delay calculation of a technology mapped network; the procedure we propose, implemented as an extension of the SIS synthesis system, is able to provide more accurate timing information than any other method presented so far; in particular, it is able to compute and store the arrival times of all the gates of the circuit for all possible input vectors, as opposed to the traditional methods which consider only the worst case primary inputs combination. Furthermore, the approach does not require any explicit false path elimination. We then extend our timing analysis tool to the symbolic calculation of required times and slacks, and we use this information to perform resynthesis for low power of the circuit by gate resizing. Our approach takes into account false paths naturally; in fact, it guarantees that resizing of the gates does not increase the true delay of the circuit, even in the presence of false paths. Our experiments have shown that many circuits, originally free of false paths, exhibit a large number of these false paths when optimized for area; therefore, the ability to deal with circuits containing false paths is of primary importance. We present experimental results for ADD-based and static timing analysis-based resynthesis, which clearly show that our tool is superior in the case of circuits containing false paths, but at the same time, it provides competitive results in the case of circuits which are free of false paths.

This paper presents a novel technique for re-synthesizing circuits for low-power dissipation. Power consumption is reduced through redundancy addition and removal by using learning to identify indirect logic implications within a circuit. Such implications are exploited by adding gates and connections to the circuit without altering its overall behavior and thereby enabling us to eliminate other, high power dissipating, nodes. We propose a new BDD-based method for computing indirect implications in a logic network; furthermore, we present heuristic techniques to perform redundancy addition and removal without destroying the topology of the mapped circuit. Experimental results show the effectiveness of the proposed technique in reducing power while keeping within delay and area constraints.

Exploiting circuit structure is a key issue in the implementation of algorithms for state space decomposition when the target is approximate FSM traversal. Given the gate-level description of a sequential circuit, the information about its structure can be captured by evaluating the affinity between pairs or groups of latches. Two main factors have to be considered in carrying out the structural analysis of a sequential circuit: latch connectivity and latch correlation. The first one takes into account the mutual dependency of each memory element on the others; the second one tells us how related are the functions realized by the logic feeding each latch. In this paper we estimate the affinity of two latches by combining these two factors, and we use this measure to formulate the state space decomposition problem as a graph partitioning problem. We propose an algorithm to automatically determine "good" partitions of the latch set which induce state space decomposition, and we present approximate FSM traversal and logic optimization results for the largest ISCAS'89 sequential benchmarks.

This paper presents algorithms for approximate finite state machine traversal based on state space decomposition. The original finite state machine is partitioned in component submachines, and each of them is traversed separately; the result of the computation is an over-estimation of the set of reachable states of the original machine. Different traversal strategies, which reduce the effects of the degrees of freedom introduced by the decomposition, are discussed. Efficient partitioning is a key point for the performance of the traversal techniques; a method to heuristically find a good decomposition of the overall finite state machine, based on the exploration of its state variable dependency graph, is proposed. Applications of the approximate traversal methods to logic optimization of sequential circuits and behavioral verification of finite state machines are described; experimental results for such applications, together with data concerning pure traversal, are reported.

Regarding finite state machines as Markov chains facilitates the application of probabilistic methods to very large logic synthesis and formal verification problems. In this paper we present symbolic algorithms to compute the steady-state probabilities for very large finite state machines (up to 10/sup 27/ states). These algorithms, based on Algebraic Decision Diagrams (ADD's)-an extension of BDD's that allows arbitrary values to be associated with the terminal nodes of the diagrams-determine the steady-state probabilities by regarding finite state machines as homogeneous, discrete-parameter Markov chains with finite state spaces, and by solving the corresponding Chapman-Kolmogorov equations. We first consider finite state machines with state graphs composed of a single terminal strongly connected component; for this type of system we have implemented two solution techniques: One is based on the Gauss-Jacobi iteration, the other one is based on simple matrix multiplication. Then we extend our treatment to the most general case of systems which can be modelled as finite state machines with arbitrary transition structures; here our approach exploits structural information to decompose and simplify the state graph of the machine. We report experimental results obtained for problems on which traditional methods fail.

This paper studies the problem of estimating worst case power dissipation in a sequential circuit.We approach this problem by nding the maximum average weight cycles in a weighted directed g r aph.In order to handle practical sized examples, we use symbolic methods, based o n A lgebraic Decision Diagrams (ADDs), for computing the maximum average length cycles as well as the number of gate transitions in the circuit, which is necessary to construct the weighted directed g r aph.

Regarding finite state machines as Markov chains facilitates the application of probabilistic methods to very large logic synthesis and formal verification problems. Recently, we have shown how symbolic algorithms based on Algebraic Decision Diagrams may be used to calculate the steadystate probabilities of finite state machines with more than 10 8 states. These algorithms treated machines with state graphs composed of a single terminal strongly connected component. In this paper we consider the most general case of systems which can be modeled as state machines with arbitrary transition structures. The proposed approach exploits structural information to decompose and simplify the state graph of the machine. 1 Introduction Finite state machines (FSMs), or their extensions, are often employed to model real digital systems for formal verification. As the complexity of those systems increases, probabilistic approaches to design and implementation verification become of interest; for...

Symbolic computation techniques play a fundamental role in logic synthesis and formal hardware verification algorithms. Recently, Algebraic Decision Diagrams, i.e., BDDs with a set of constant values different to the set /spl lcub/0,1/spl rcub/, have been used to solve general purpose problems, such as matrix multiplication, shortest path calculation, and solution of linear systems, as well as logic synthesis and formal verification problems, such as timing analysis, probabilistic analysis of finite state machines, and state space decomposition for approximate finite state machine traversal. ADD-based procedures for single-source and all-pairs shortest path weight calculation have appeared to be very effective for the manipulation of large graphs (over 10/sup 27/ vertices and 10/sup 36/ edges). However, for those procedures to be applicable to real problems, for example flow network problems, computing only shortest path weights is not enough; what it is needed is an algorithm that, given the weight of a shortest path between two vertices of a graph, actually determines the sequence of vertices belonging to the shortest path. This paper proposes a symbolic algorithm to execute shortest path back-tracing which exploits the compactness of the ADD data structure to handle large graphs.>

Exploiting circuit structure is a key issue in the implementation of algorithms for state space decomposition when the target is approximate FSM traversal. Given the gate-level description of a sequential circuit, the information about its structure can be captured by evaluating the affinity between pairs or groups of latches. Two main factors have to be considered in carrying out the structural analysis of a sequential circuit: latch connectivity and latch correlation. We estimate the affinity of two latches by combining these two factors, and we use this measure to translate the state space decomposition problem into a graph partitioning problem. Traversal results obtained on the largest ISCAS'89 benchmarks show the effectiveness of the method.>

In order to reliably predict the behavior of a finite state machine (FSM) M or to generate acceptance tests for sequential designs, it is necessary to drive M to a predictable state or set of states. One possible way of accomplishing this is to have a special reset circuit to force all the latches to a specific state. However, if the circuit can be driven to a predictable state by applying an input sequence, the area required for reset circuitry can be saved. A synchronizing sequence for an FSM M is an input sequence which, when applied to any initial state of M, will drive M to a single specific state, called a reset state. An efficient and exact method for computing synchronizing sequences based on the efficient image and pre-image computation methods using binary decision diagrams is presented. The method is exact in the sense that it is a decision procedure: Given enough time and memory, the method can compute a synchronizing sequence if M has one; otherwise, the method says that M is not resettable. The theoretical heart of the proposed method is Universal Alignment, which is an analysis of the product of an FSM with itself. Algorithms and their related theorems are presented to perform the following: decide whether M has a synchronizing sequence (i.e., M is resettable), calculate a synchronizing sequence for M, calculate the set of all reset states, decide whether a specific state is a reset state. New results on the resettability of some benchmark circuits are reported.>

In this paper we present two exact algorithms for state minimization of FSM's. Our results prove that exact state minimization is feasible for a large class of practical examples, certainly including most hand-designed FSM's. We also present heuristic algorithms, that can handle large, machine-generated, FSM's. The possibly many different reduced machines with the same number of states have different implementation costs. We discuss two steps of the minimization procedure, called state mapping and solution shrinking, that have received little prior attention to the literature, though they play a significant role in delivering an optimally implemented reduced machine. We also introduce an algorithm whose main virtue is the ability to cope with very general cost functions, while providing high performance.>

Article Algorithms for approximate FSM traversal Share on Authors: Hyunwoo Cho View Profile , Gary D. Hachtel View Profile , Enrico Macii View Profile , Bernard Plessier View Profile , Fabio Somenzi View Profile Authors Info & Claims DAC '93: Proceedings of the 30th international Design Automation ConferenceJuly 1993 Pages 25–30https://doi.org/10.1145/157485.164555Online:01 July 1993Publication History 72citation370DownloadsMetricsTotal Citations72Total Downloads370Last 12 Months3Last 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

In this paper we present theory and experiments on the algebraic decision diagrams (ADDs). These diagrams extend BDD's by allowing values from an arbitrary finite domain to be associated with the terminal nodes. We present a treatment founded in Boolean algebras and discuss algorithms and results in applications like matrix multiplication and shortest path algorithms. Furthermore, we outline possible applications of ADD's to logic synthesis, formal verification, and testing of digital systems.

We present an algorithm for finding the maximum flow in a 0-1 network. The algorithm is symbolic and avoids explicit enumeration of the nodes and edges of the network. Therefore, it can handle much larger graphs than it was previously possible (more than 10/sup 36/ edges). The main idea is to trace (implicitly) sets of edge-disjoint augmenting paths. Disjointness is enforced by solving an edge matching problem for each layer of the network with the help of newly defined priority functions.

Finite state machine (FSM) verification based on implicit state enumeration can be extended to test generation and redundancy identification. The extended method constructs the product machine of two FSMs to be compared, and reachability analysis is performed by traversing the product machine to find any difference in I/O behavior. When an output difference is detected, the information obtained by reachability analysis is used to generate a test sequence. This method is complete, and it generates one of the shortest possible test sequences for a given fault. However, applying this method indiscriminately for all faults may result in unnecessary waste of computer resources. An efficient method based on reachability analysis of the fault-free machine (three-phase ATPG) in addition to the powerful but more resource-demanding product machine traversal is presented. The application of these algorithms to the problems of generating test sequences, identifying redundancies, and removing redundancies is reported.>

The authors explore the relationship between algebraic transformations for area optimization and the testability of combinational logic circuits. It is shown that for each multifault in an algebraically factored circuit there is an equivalent multifault in the original circuit. Using this result, it is shown how algebraic factorization may be applied to minimized two-level circuits, to synthesize area-optimized, completely multifault testable multilevel circuits. When a circuit is synthesized using algebraic factorization from a minimized two-level circuit, a reasonably small set of tests that give complete multifault coverage of the synthesized circuit can be derived from the single-fault tests for the original two-level circuit. It is shown that single-fault testability is not an invariant maintained by algebraic transformations, and a simple single-fault irredundant circuit on which the application of algebraic transformations activate a latent multifault, making the resulting algebraically transformed circuit single-fault redundant is presented.>

The authors present an extension to binary decision diagrams (BDDs) that exploits the information contained in the structure of the circuit to produce a compact, semicanonical representation. The extended BDDs (XBDDs) retain many of the advantages of BDDs while at the same time allowing one to deal with larger circuits. Using XBDDs, it is possible to verify circuits for which the BDDs could not be built in the same amount of space. Results of the application of XBDDs to combinational multipliers are presented.>

The authors consider the problem of variable ordering in algorithms for verification of finite state machines (FSMs) for which the traversal is based on BDD (binary decision diagram) representation and image computation via implicit enumeration. They treat two separate BDD ordering problems: (1) minimization of the representation of the next state function and the representation of the set of reachable states, and (2) a selection heuristic to reduce the complexity of the image computation problem by dynamic selection of the implicit enumeration splitting variables. In both problems they present theoretical results based on the algebraic structure of the next state functions, heuristic ordering methods, and favorable experimental results for problems with significant algebraic structure.>

The authors consider the nature of incomplete specifications for a finite state machine embedded in a network of sequential machines. They show how limited controllability and observability of component machines are expressed in quite different ways. For the input don't care sequences, a general solution was known. The authors present extensions to it, both in terms of topologies contemplated and in terms of applicability to larger designs. For the output don't care sequences, they provide a general theory based on the concept of information lossyness and present algorithms to address the related optimization problem in practical cases. The implementation of the proposed techniques in a program called SEQUOIA (sequential optimization of interacting automata) shows that the proposed approach is viable and effective.>

The knowledge of the state transition graph (STG) of a sequential circuit helps in generating test sequences and identifying redundancies. The application of algorithms to the identification and removal of redundancies is reported. This strategy is based on traversing the STG of the given circuit and then performing redundancy identification using the reachability information calculated by the traversal. This method considers one candidate redundancy at a time, in an order that tries to minimize the total processing time. Substantial area and delay reductions are achieved. Experiments show that for many circuits 100% of the sequentially redundant faults can be eliminated in very reasonable amounts of time.>

The knowledge of the State Transition Graph (STG) of a sequential circuit helps in generating test sequences. For instance, by determining that a set of states is not reachable from the reset state, it is possible to identify a certain type of sequentially untestable faults. However, until recently, the ability of algorithms to store the STG of a sequential circuit has been limited to small instances. Recent advances in sequential circuit verification, based on the use of binary decision diagrams and new powerful implicit enumeration algorithms, have dramatically improved our ability to deal with large numbers of states. In this paper we report on the application of these algorithms to the problems of generating justification sequences, identifying redundancies, and dealing with hard-to-detect faults. Our experiments show substantial improvements over previously published results.

A novel state assignment algorithm, called MUSE (multilevel symbolic encoding), for the encoding of FSMs (finite state machines) targeted for multilevel implementation is presented. Novel methods are discussed for the computation of state pair costs that are based onmultilevel algebraic structures derived from the one hot encoded state machine by purely algebraic techniques. Both Boolean (distance-1 MERGE and consensus) and algebraic (SUB-EXPRESSION EXTRACTION and CO-KERNEL EXTRACTION) operations are used to calculate the encoding affinity of state pairs, and account for face embedding constraints as well. Both heuristic and simulated annealing encoding techniques are used.>

Algorithms are presented for finite state machine (FSM) verification and image computation which improve on the results of O. Coudert et al (1989), giving 1-4 orders of magnitude speedup. Novel features include primary input splitting-this PODEM feature enlarges the search space but shortens the search due to implications. Another new feature, identical subtree recombination, is shown to be effective for iterative networks (eg, serial multipliers). The free-variable recognition feature prevents unbalanced bipartitioning trees in tautological subspaces. Finally, reached set pruning is significant when the image contains large numbers of previously reached states.>

A survey of logic synthesis techniques for multilevel combinational logic is presented. The goal is to provide more in-depth background and perspective for people interested in pursuing or assessing some of the topics in this emerging field. Introductions, capsule summaries, and, in some cases, detailed analysis of the synthesis methods that have become established as practically significant are provided. Also included are some methods that have theoretical interest and potential for future impact. The discussion covers notation and definitions, representation of the network and nodes, logic decomposition/restructuring, logic optimization/minimization, logic synthesis and testing, and technology mapping.>

The authors describe efficient polynomial algorithms for the extraction of topologically minimal multilevel Boolean equations and don't care conditions from the C-based hardware description language CHDL, which has control constructs switch, if-then-else, and go-to. They show that significant savings in CPU cost, area cost, and robustness may be obtained by applying these algorithms as a preprocessing step before using higher cost minimization tools such as BOLD or misII. The approach is based on a control-flow-graph construct with embedded set-use-graph information. The algorithms parse a CHDL description into a directed, nonseries parallel control flow graph. In cases where the graph is also acyclic, graph search and decomposition algorithms are used to derive a Boolean network representing the implied combinational logic. The derived equations are topologically irredundant in the sense that the topological identities are associated with the fork, and join nodes of the control flow graph are accounted for in the code generation. Without this feature, multilevel logic optimizers would have to flatten the control expressions down to primary inputs to discover these identities.>

The authors present a number of results exploring the relationship between algebraic transformations for area optimization and the testability of combinational logic circuits. They show that for each multifault in an algebraically factored circuit there is an equivalent multifault in the original circuit, and it is well known that two-level single-output circuits that are single-fault testable are also multifault testable. They also show how these results imply that algebraic factorization may be applied to minimized (and therefore completely single-fault testable) two-level circuits, in order to synthesize area optimized, completely multifault testable circuits. Furthermore, when algebraic factorization is applied to a minimized two-level circuit all tests needed for complete multifault coverage of the synthesized circuit can be derived from the single-fault tests for the original two-level circuit.>

Algorithms are presented for RI (redundancy identification) and RR (redundancy removal). With fault simulation and a backtrack limit of 10, the RI program is able to find a test for all testable faults and identify all the redundant faults in each of the ISCAS benchmark examples. The RR program makes the whole benchmark set 100% testable for single stuck-at faults, and generates the test, in less than 1 CPU hour (SUN4/280). The algorithms were developed for equivalence-based logic optimization applications, which accentuate the role of heuristics in the process of automatic test program generation (ATPG), since this diminishes the role of fault simulation. The authors compare a limited set of results obtained by RR to those of existing logic optimization programs. The results show that in most cases, superior results can be obtained with factors of tens to hundreds speedup in CPU time.>

A hierarchical procedure for net routing on l*m*n grid-graphs, where l is the number of layers, m is the number of rows, and n is the number of columns, is presented. The hierarchy reduces the overall problem to a sequence of subproblems, where each subproblem works on an l*m'*n portion of the overall grid. For each subproblem, an initial constructive placement (CP) of as many nets as possible is used; then a generalized dynamic programming (DP) algorithm to solve the Steiner problem of an l*2*n grid-graph is used for any remaining nets. The CP procedure uses simplistic routing assumptions to route quickly as many nets as possible. If all nets are routed, the subproblem solution is (locally) optimal and the corresponding branch of the binary recursion tree generated by the hierarchy is pruned. For any unrouted nets, the generalized DP procedure is called to route each net, one at a time, with a run time complexity of O(K*n) where n is the number of columns and K is a function of the grid cross section and layer/wiring restrictions. There are no a priori layer restrictions or limitations on the number of layers used; three-layer cases and even some four-layer cases are feasible for the PYRAMID 90-X.>

BEATNP (BoolEAn Tools Network Partitioner) was designed to extend the application size capability of the BOLD (Boulder Optimal Logic Design) system. BEATNP partitions a Boolean network into subnetworks which satisfy user specified size constraints. Most of the tools in the BOLD tools suite solve problems which are in NP or Co-NP, so they can be assumed to have exponential complexity. Because the BEATNP algorithms have log-linear worst-case complexity, the CPU time requirements of optimization tools can be reduced greatly in difficult cases. When used with the BOLD minimizer on a set of well known benchmark examples, BEATNP reduced CPU time by 1 to 3 orders of magnitude while retaining a significant majority of the optimization savings available in the unpartitioned case.>

Uses of implied network values or conditions in the context of multilevel logic synthesis are presented. The use of these implications has resulted in performance-enhanced versions, ESPRESSOMLT2 and MLTAUT2, of the two cornerstone tools of the BOLD system, ESPRESSOMLT (multilevel logic minimizer based on tautology checking) and MLTAUT (multilevel logic verifier). The relationship between the implied values and the intermediate don't care set is presented. Then it is shown how this relationship can be exploited to reduce the number of tautology calls and the number of leaves in the binary recursion tree of tautology checking. A parallelized version MLTAUT2P, which runs on a Sun 3/75 LAN, is discussed. ESPRESSOMLT2, is expected to have speedups of up to a factor of 20 and the parallelized version a factor of over 100.>

An approach is described for the minimization of multilevel logic circuits. A multilevel representation of a block of combinational logic is defined, called a Boolean network. A procedure is then proposed, called ESPRESSOMLD, to transform a given Boolean network into a prime, irredundant, and R-minimal form. This procedure rests on the extension of the notions of primality and irredundancy, previously used only for two-level logic minimization, to combinational multilevel logic circuits. The authors introduce the concept of R-minimality, which implies minimality with respect to cube reshaping, and demonstrate the crucial role played by this concept in multilevel minimization. Theorems are given that prove the correctness of the proposed procedure. Finally, it is shown that prime and irredundant multilevel logic circuits are 100% testable for input and output single-stuck faults, and that these tests are provided as a byproduct of the minimization.>

A description is given of a theory for, and the application of, a general algorithm for determining whether a given multilevel Boolean function is a tautology or whether two given multilevel Boolean functions are equivalent. Four specific cases of this general algorithm are examined. These are termed the flattening method, the don't-care method, the simulation method, and the algebraic string comparison method. A single unifying algorithm frame is given for the implementation of any of these four methods, depending on parameterization. Experimental results are given which indicate that, with the exception of the don't-care method, each of these methods has a problem class in which it is clearly superior to the others. The primary application of these algorithms is as a verification tool for silicon compilation systems. However, these algorithms are also being used as the foundation for multilevel logic minimization and automatic test pattern generation programs.>

Article Free Access Share on SOCRATES: a system for automatically synthesizing and optimizing combinational logic Authors: David Gregory GE Calma Company Research Triangle Park, North Carolina GE Calma Company Research Triangle Park, North CarolinaView Profile , Karen Bartlett Department of Electrical Engineering University of Colorado at Boulder Department of Electrical Engineering University of Colorado at BoulderView Profile , Aart de Geus GE Calma Company Research Triangle Park, North Carolina GE Calma Company Research Triangle Park, North CarolinaView Profile , Gary Hachtel Department of Electrical Engineering University of Colorado at Boulder Department of Electrical Engineering University of Colorado at BoulderView Profile Authors Info & Claims DAC '86: Proceedings of the 23rd ACM/IEEE Design Automation ConferenceJuly 1986 Pages 79–85Online:02 July 1986Publication History 32citation279DownloadsMetricsTotal Citations32Total Downloads279Last 12 Months2Last 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 Alerts New Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

The automation of the synthesis and optimization of combinational logic can result in savings in design time, significant improvements of the circuitry, and guarantee functional correctness. Synthesis quality is often measured in terms of the area of the circuit on the chip, which fails to take into account the timing constraints that might be imposed on the logic. This paper describes SOCRATES, a synthesis system capable of generating combinational logic in a given technology under user-defined timing constraints. We believe this system is the first to perform optimized, delay-constrained, multilevel synthesis into standard cell libraries. Applied to a large number of examples, the system has successfully traded off area versus delay and performs optimized, delay-constrained, multilevel synthesis into standard cell libraries.

The optimal PLA folding problem is presented and discussed in its different forms. In particular, new algorithms for row folding in unconstrained architectures and in AND-OR-AND architectures are presented and their complexity examined. The problem of finding an optimal row folding after a column folding has been performed, is described and an algorithm for its solution given. Finally, the organization of an APL package for row and column folding of PLA's is introduced and experimental results reported.

In this paper we introduce the concept of implication for MOS switch level circuits. The implication performed on these circuits is an extension of the classical implication now applied to Boolean logic networks. Given the ability to perform implication on MOS circuits we can then; generate functional macromodels of MOS circuits, use these macromodels to verify the Boolean function realized by the MOS circuit extracted from the mask set, generate, directly from the MOS circuit sets of tests for nodes stuck-at-1 and stuck-at-0 as well as transistors stuck open and stuck short. We present the conceptual frame work and algorithms for performing implication on MOS networks. We present examples of MOS implication and discuss extensions of the algorithm to test generation, and to a first order instead of zero order MOS network.

In this paper we present a graph-theoretic formulation of the optimal PLA folding problem. The class of admissible PLA foldings is defined. Necessary and sufficient conditions for obtaining the optimal folding are given. A subproblem of the optimal problem is shown to be NP-complete, and a heuristic algorithm is given which has proven to be effective on a number of test problems.