Ashenhurst-Curtis decomposition (ACD) is a decomposition technique used, in particular, to map combinational logic into lookup tables (LUTs) structures when synthesizing hardware designs. However, available implementations of ACD suffer from excessive complexity, search-space restrictions, and slow run time, which limit their applicability and scalability. This article presents a novel fast and versatile technique of ACD suitable for delay optimization. We use this new formulation to compute two-level decompositions into a variable number of LUTs and enhance delay-driven LUT mapping by performing ACD on the fly. Compared to state-of-the-art technology mapping, experiments on heavily optimized benchmarks demonstrate an average delay improvement of 12.39% and area reduction of 2.20% with affordable run time. Additionally, our method improves 4 of the best delay results in the EPFL synthesis competition without employing design-space exploration techniques. Moreover, we use the new formulation to compute exact decompositions into fixed LUT cascade structures of two LUTs, which have efficient implementations in the architecture of AMD field-programmable gate arrays. Compared to the state-of-the-art method, this new formulation leads to an average reduction of 6.22% in delay, 3.82% in area, and 3.09% in the edge count for better run time.

This article proposes a new logic synthesis and verification paradigm based on circuit simulation. In this paradigm, high quality, expressive simulation patterns are pregenerated to be reused in multiple runs of optimization and verification algorithms, resulting in reduced time-consuming Boolean computations such as satisfiability (SAT) solving. Methods to generate expressive simulation patterns are presented and compared, and a bit-packing technique to compress them is integrated into the implementation. The generated patterns are shown to be reusable across different algorithms and after network function modifications. A logic synthesis algorithm, Boolean resubstitution, and a verification algorithm, combinational equivalence checking, are two examples of using this paradigm. In simulation-guided Boolean resubstitution, simulation patterns are used for efficient filtering of optimization choices, leading to a lower cost in expanding the search space. By adopting the proposed paradigm, we achieve a 5.9% reduction in the number of AIG nodes, compared to 3.7% by a state-of-the-art resubstitution algorithm, within comparable runtime. In simulation-guided equivalence checking, the number of SAT solver calls is reduced by 9.5% with the use of the expressive simulation patterns accumulated in earlier logic synthesis stages.

The paper addresses a key aspect of efficient computation in logic synthesis and formal verification, namely, the integration of a circuit simulator and a Boolean satisfiability solver. A novel way of interfacing these is proposed along with a fast preprocessing step to detect easy SAT instances and a new hybrid SAT solver, which is more robust for hardware designs than are state-of-the-art CNF-based solvers. The proposed integration enables a 10x speedup in essential computation engines widely used in industrial EDA tools, including SAT sweeping, combinational and sequential equivalence checking, and computing structural choices for technology mapping. The speedup does not lead to a loss in quality because the computed equivalences are canonical.

To reduce dynamic power dissipation in digital circuits, a dependency graph (DG) is derived for a sequential circuit to accomplish verification and synthesis of clock-gated circuits. This is used recursively to derive sufficient conditions for a given bank of flops (flip-flops) to be legally clock gated (disabled.) These conditions are expressed with linear temporal logic (LTL)/past LTL (PLTL) properties, which can be used to create hardware monitors and justified by hardware model checkers. For sequential equivalence checking (SEC), LTL/PLTL properties are formulated to be proved on a clock-gated circuit (R) derived from a “golden” circuit (G). If these sufficient conditions can be proved on R, then the clock gating structures are proved redundant and can be removed. This creates a simplified circuit (R') and makes the SEC task easier. Experiments were performed on a set of benchmarks. It was observed that since the properties are expressed in terms of the control signals which only appear in the DG, they are quite easy to prove on R because the DG abstracts away complicated arithmetic logic. Similarly, the miter between G and R' is usually proved easily by model-checking methods because of the increased similarity between G and R' in sequential behaviors, compared to the changes between G and R. The proposed formulation is extended to provide a systematic and automatic method for sequential clock-gating synthesis. Experiments showed that the DG-based framework for synthesis gave encouraging results.

This paper proposes a fast SAT-based algorithm for recovering area applicable to an already technology mapped circuit. The algorithm considers a sequence of relatively small overlapping regions, called windows, in a mapped network and tries to improve the current mapping of each window using a SAT solver. Delay constraints are considered by interfacing the SAT solver with a timer. Experimental results are given for benchmarks that have been mapped already into 6-LUTs by a high-effort area-only synthesis/mapping flow. The new mapper starting from these results, many of which represented the best known area results at the time, achieved an additional average area reduction of 3-4%, while for some benchmarks the area reduction exceeded 10%. Runtime for any example was only a few seconds.

Engineering Change Orders (ECO) modify a synthesized netlist after its specification has changed. ECO is divided into two major tasks: finding target signals whose functions should be updated and synthesizing the patch that produces the desired change. This paper proposes an efficient SAT-based solution for the second task: resource-aware computation of multi-output patch functions. The solution is based on several new algorithms and outperforms the top three winners of the 2017 ICCAD CAD Contest (Problem A).

A representation of a Boolean function is canonical if, given a variable order, only one instance of the representation is possible for the function. A computation is canonical if the result depends only on the Boolean function and a variable order, and does not depend on how the function is represented and how the computation is implemented.

In electronic design automation Boolean resynthesis techniques are increasingly used to improve the quality of results where algebraic methods hit local minima. Boolean methods rely on complete functional properties of a logic circuit, preferably including don't care information. Computationally expensive engines such as truth tables, SAT and binary decision diagrams are required to gather such properties. The choice of the engine determines the scalability of Boolean resynthesis. In this paper, we present improvements to Boolean resynthesis, enabling more optimization opportunities to be found at the same or smaller runtime cost as compared to state-of-the-art methods. Our contributions include (i) a theory of Boolean filtering to drastically reduce the number of gates processed and still retain all possible optimization opportunities, (ii) a weaker notion of maximum set of permissible functions, which can be computed efficiently via truth tables, (iii) a generalized refactoring engine that supports multiple representation forms, and (iv) a practical Boolean resynthesis flow, which combines the techniques proposed so far. Using our Boolean resynthesis on the EPFL benchmarks, we improve 10 of the best known area results in the synthesis competition. Embedded in a commercial EDA flow for ASICs, the Boolean resynthesis flow reduces the area by -2.67% and total negative slack by -5.48%, after physical implementation, at negligible runtime cost.

The fast-extract algorithm is a well-known algebraic method for factoring and decomposing Boolean expressions. Since it uses pairwise comparisons between cubes to find factors, the runtime is degraded for networks whose primary outputs are expressed in terms of primary inputs and have Boolean functions with thousands of cubes. This paper describes a new implementation of the fast-extract algorithm, fxch, having complexity linear in the number of cubes. The reduction in complexity is achieved by hashing sub-cubes and using the hash table to find good factors to extract. Experimental results on industrial benchmarks show superior runtime and scalability of the proposed algorithm, compared to the available solutions.

SAT-based Property Directed Reachability (PDR) has become the key algorithmic development for unbounded model checking of gate-level sequential circuits, but it can be inefficient when applied to word-level problems with heavy arithmetic logic. To address this issue, word-level abstraction is often performed by replacing a whole set of signals with unconstrained new primary inputs. This paper introduces PDR-WLA, a word-level abstraction-refinement algorithm integrated into a modified PDR implementation. The algorithm uses efficient refinement and re-uses reachability information across iterations of refinement. PDR-WLA was implemented in ABC and evaluated on a large set of industrial Verilog designs. Experimental results show significant speedups on hard problems compared to the original PDR and to a naive word-level abstraction-refinement method.

Given (i) a Boolean function, (ii) a set of arrival times at the inputs, and (iii) a gate library with associated delay values, the exact delay synthesis problem asks for a circuit implementation which minimizes the arrival time at the output(s). The exact delay synthesis problem, with given input arrival times, relates to computing the communication complexity of a Boolean function, which is an intractable problem. Input arrival times are variable and can take any value, thereby making the exact delay synthesis search space infinite. This paper presents theory and algorithms for exact delay synthesis. We introduce the theory of equioptimizable arrival times, which allows us to partition all arrival time patterns into a finite set of equivalence classes. Thanks to this new theory, we create for the first time exact delay circuit databases covering all Boolean functions up to 5 variables and all possible arrival time patterns. We describe further arrival time compression techniques which enable the creation of larger databases. We propose an enhanced delay synthesis flow capable of dealing with large circuits, combining exact delay logic rewriting and Boolean optimization techniques, attaining unprecedented results. We improve 9/10 of the best known results in the EPFL arithmetic delay synthesis competition, outperforming previous best results up to 3x. Embedded in a commercial EDA flow for ASICs, our exact delay synthesis techniques reduce the total negative slack by 12.17%, after physical implementation, at negligible area and runtime costs.

Methods for word-level model checking based on purely bit-level techniques have difficulties with heavy arithmetic logic. Word-level and SMT approaches often are limited by relying on (incomplete) bounded model checking. UFAR, a hybrid word- and bit-level approach, addresses these issues, taking advantage of modern bit-level sequential techniques while heavy arithmetic logic is addressed by word-level abstraction and the use of uninterpreted function (UF) constraints. The methods and efficiency improvements developed for UFAR enabled it to prove 2422 of a set of 2492 industrial sequential model checking problems within a 1-hour limit, while a bit-level model checker super prove completed only 2115 of these within the same limit.

Lexicographic Boolean satisfiability (LEXSAT) is a variation of the Boolean satisfiability problem (SAT). Given a variable order, LEXSAT finds a satisfying assignment whose integer value under the given variable order is minimum (maximum) among all satisfiable assignments. If the formula has no satisfying assignments, LEXSAT proves it unsatisfiable, as does the traditional SAT. The paper proposes an efficient algorithm for LEXSAT by combining incremental SAT solving with binary search. It also proposes methods that use the lexicographic properties of the assignments to further improve the runtime when generating consecutive satisfying assignments in lexicographic order. The proposed algorithm outperforms the state-of-the-art LEXSAT algorithm—on average, it is 2.4 times faster when generating a single LEXSAT assignment, and it is 6.3 times faster when generating multiple consecutive assignments.

This paper introduces m-inductiveness over a set of nodes S in sequential circuits. The m-inductive property can be used for equivalence-checking or improved sequential optimization. It allows the behavior of many next state functions (not in S) to be changed while maintaining correctness at the primary outputs of a circuit. As such, it creates flexibility that can be used for sequential optimization. It is shown that the number of nodes in S is reduced as m, the parameter for the inductiveness, increases. We provide an algorithm for finding a minimal set S, as well as one for using m-inductiveness in optimization. We give examples of such optimized circuits and show that m-inductive-based optimization can result in significant area reduction when applied to industrial designs.

Sequential clock-gating can lead to easier equivalence checking problems, compared to the general sequential equivalence checking (SEC) problem. Modern sequential clock-gating techniques introduce control structures to disable unnecessary clocking. This violates combinational equivalence but maintains sequential equivalence between the original and revised circuits. We propose the use of characteristic graphs (CGs) to extract essential LTL clock-gating properties, which when proved imply certain sequential redundancies. The extraction, proof and subsequent removal of the implied redundancies lead to an efficient SEC procedure for clock-gated circuits. Experiments show that the proposed SEC procedure substantially outperforms existing methods in terms of speed and scalability when applied to several difficult cases.

We study three-level implementations where the first two levels represent a standard PLA form with an AND-plane and an OR-plane. This implements a 2m-output SOP. The final stage consists of m two-input programmable LUTs. The PLA outputs are paired so that the LUT outputs implement a set of m given incompletely specified functions (ISFs). Three-level structures have been studied previously, e.g. resulting in ANDOR-AND or AND-OR-XOR implementations. By using the LUT effectively, the composition of the AND-plane can be controlled to implement a PLA which has the optimum phase assignment for maximum cube sharing. For each output, we characterize the problem of all legal implementations of such a model, by defining Boolean relations that capture all the flexibility induced by the final LUT logic. The extra LUT level provides a dimension beyond simple phase assignment. We performed experiments using a Boolean relation minimizer to compare such realizations vs. SOP forms and published three-level forms, comparing areas and delays. To approximate the possible sharing in the PLA, we mapped the 2m PLA logic using SIS. We focused on experiments with two-input Boolean functions not captured by AND-OR-AND or AND-OR-XOR approaches and found good gains in many cases with affordable increases in synthesis runtimes.

Reverse engineering is the extraction of word level information from a gate-level netlist. It has applications in formal verification, hardware trust, information recovery, and general technology mapping. A preprocessing step finds blocks in a circuit in which word level components are expected. A second step searches for word level components in these blocks. For this second step, we propose two variants of equivalence checking that consider subfunction containment. We propose algorithms to solve these variants by using subgraph isomorphism. A simulation graph (SG) is constructed for the block and for each library component, using a set of permutation-invariant simulation vectors for that component. If a library component SG is a subgraph of the block SG, we have a candidate match, which is then checked by standard equivalence checking. We extend a state-of-the-art subgraph isomorphism algorithm, LAD, to handle simulation graphs efficiently and also propose a SAT-based formulation. Experimental evaluations show that our algorithms can efficiently find 32-bit arithmetic components in blocks with over 300 primary inputs.

Field-Programmable Gate Arrays (FPGA) implement logic functions using programmable cells, such as K-input lookup-tables (K-LUTs). A K-LUT can implement any Boolean function with K inputs and one output. Methods for mapping into K-LUTs are extensively researched and widely used. Recently, cells other than K LUTs have been explored, for example, those composed of several LUTs and those combining LUTs with several gates. Known methods for mapping into these cells are specialized and complicated, requiring a substantial effort to evaluate custom cell architectures. This paper presents a general approach to efficiently map into single-output K-input cells containing LUTs, MUXes, and other elementary gates. Cells with to 16 inputs can be handled. The mapper is fully automated and takes a logic network and a symbolic description of a programmable cell, and produces an optimized network composed of instances of the given cell. Past work on delay/area optimization during mapping is applicable and leads to good quality of results.

The articles in this special issue provides an overview of and a perspective on the evolution of electronic design automation (EDA), and offers a perspective on some of the principal avenues of future development.

An important step in the design of a complex system is its decomposition into a number of interacting components, of which some are given (known) and some need to be synthesized (unknown). Then a basic task in the design flow is to synthesize an unknown component that when combined with the known part of the system (the context) satisfies a given specification. This problem arises in several applications ranging from sequential synthesis to the design of discrete controllers. There are different formulations of the problem, depending on the formal models to specify the system and its components, the composition operators, and the conformance relations of the composed system versus the specification. Various behavioral models have been studied in the literature, e.g., finite state machines and automata, omega-automata, process algebras; various forms of synchronous and asynchronous (interleaving/parallel) composition have been considered; the conformance relations include language containment and equality, and notions of simulation. In this paper we give an overview of the problem (a.k.a., the unkown component problem, or submodule construction, etc.), and we focus on its reduction to solving equations over languages, as a key technology for supporting synthesis of compositional systems. We survey the state-of-art and highlight open problems requiring further investigation.

We present ABCD-NL, a technique that approximates non-linear analog circuits using purely Boolean models, to high accuracy. Given an analog/mixed-signal (AMS) system (e.g., a SPICE netlist), ABCD-NL produces a Boolean circuit representation (e.g., an And Inverter Graph, Finite State Machine, or Binary Decision Diagram) that captures the I/O behaviour of the given system, to near SPICE-level accuracy, without making any apriori simplifications. The Boolean models produced by ABCD-NL can be used for high-speed simulation and formal verification of AMS designs, by leveraging existing tools developed for Boolean/hybrid systems analysis (e.g., ABC [1]). We apply ABCD-NL to a number of SPICE-level AMS circuits, including data converters, charge pumps, comparators, non-linear signaling/communications sub-systems, etc. Also, we formally verify the throughput of an AMS signaling system - modelled in SPICE using 22nm BSIM4 transistors, Booleanized with high accuracy using ABCD-NL, and property-checked using ABC.

Sequential logic synthesis often leads to substantially easier equivalence checking problems, compared to general-case sequential equivalence checking (SEC). This paper theoretically investigates when SEC can be reduced to a combinational equivalence checking (CEC) problem. It shows how the theory can be applied when sequential transforms are used, such as sequential clock gating, retiming, and redundancy removal. The legitimacy of such transforms is typically justified intuitively, by the designer or software developer believing that the two circuits reach the same state after a finite number of cycles, and no difference is observed at the outputs due to fanin non-controllability and fanout non-observability effects.

Verification benefits from removing logic that is not relevant for a proof. Techniques for doing this are known as localization abstraction. Abstraction is often performed by selecting a subset of gates to be included in the abstracted model; the signals feeding into this subset become unconstrained cut-points. In this paper, we propose several improvements to substantially increase the scalability of automated abstraction. In particular, we show how a better integration between the BMC engine and the SAT solver is achieved, resulting in a new hybrid abstraction engine, that is faster and uses less memory. This engine speeds up computation by constant propagation and circuit-based structural hashing while collecting UNSAT cores for the intermediate proofs in terms of a subset of the original variables. Experimental results show improvements in the abstraction depth and size.

In numerous EDA flows, time-consuming computations are repeatedly applied to sequential circuits. This motivates developing methods to determine what circuits have been processed already by a tool. This paper proposes an algorithm for semi-canonical labeling of nodes in a sequential AIG, allowing problems or sub-problems solved by an EDA tool to be cached with their computed results. This can speed up the tool when applied to designs with isomorphic components or design suites exhibiting substantial structural similarity.

Formal verification of liveness properties of practical communication fabrics are generally intractable with present day verification tools. We focus on a particular type of liveness called `progress' which is a form of deadlock freedom. An end-to-end progress property is broken down into localized safety assertions, which are more easily provable, and lead to a formal proof of progress. Our target systems are credit-based flow-control networks. We present case studies of this type and experimental results of progress verification of large networks using a bit-level formal verifier.

Mapping into K-input lookup tables (K-LUTs) is an important step in synthesis for Field-Programmable Gate Arrays (FPGAs). The traditional FPGA architecture assumes all interconnects between individual LUTs are “routable”. This paper proposes a modified FPGA architecture which allows for direct (non-routable) connections between adjacent LUTs. As a result, delay can be reduced but area may increase. This paper investigates two types of LUT structures and the associated tradeoffs. A new mapping algorithm is developed to handle such structures. Experimental results indicate that even when regular LUT structures are used, area and delay can be improved 7.4% and 11.3%, respectively, compared to the high-effort technology mapping with structural choices. When the dedicated architecture is used, the delay can be improved up to 40% at the cost of some area increase.

Reducing delay of a digital circuit is an important topic in logic synthesis for standard cells and LUT-based FPGAs. This paper presents a simple, fast, and very efficient synthesis algorithm to improve the delay after technology mapping. The algorithm scales to large designs and is implemented in a publicly-available technology mapper. The code is available online. Experimental results on industrial designs show that the method can improve delay after standard cell mapping by 30% with the increase in area 2.4%, or by 41% with the increase in area by 3.9%, on top of a high-effort synthesis and mapping flow. In a separate experiment, the algorithm was used as part of a complete industrial standard cell design flow, leading to improvements in area and delay after place-and-route. In yet another experiment, the algorithm was applied before FPGA mapping into 4-LUTs, resulting in 16% logic level reduction at the cost of 9% area increase on top of a high-effort mapping.

During the very large scale integration design process, a synthesized design is often required to be modified in order to accommodate different goals. To preserve the engineering effort already invested, designers seek small logic structural transformations to achieve these logic restructuring goals. This paper proposes a systematic methodology to devise such transformations automatically. It first presents a simulation-based formulation to approximate sets of pairs of functions to be distinguished and avoid the memory/time explosion issue inherent with the original representation. Then, it uses this new data structure to devise the required transformations dynamically without the need of a static dictionary model. The methodology is applied to both combinational and sequential designs with transformations at a single or multiple locations. An extensive suite of experiments documents the benefits of the proposed methodology when compared to existing practices.

We describe an optimization method for combinational and sequential logic networks, with emphasis on scalability. The proposed resynthesis (a) is capable of substantial logic restructuring, (b) is customizable to solve a variety of optimization tasks, and (c) has reasonable runtime on industrial designs. The approach uses don't-cares computed for a window surrounding a node and can take into account external don't-cares (e.g., unreachable states). It uses a SAT solver for all aspects of Boolean manipulation: computing don't-cares for a node in the window, and deriving a new Boolean function of the node after resubstitution. Experimental results on 6-input LUT networks after a high effort synthesis show substantial reductions in area and delay. When applied to 20 large academic benchmarks, the LUT counts and logic levels are reduced by 45.0% and 12.2%, respectively. The longest runtime for synthesis and mapping is about two minutes. When applied to a set of 14 industrial benchmarks ranging up to 83K 6-LUTs, the LUT counts and logic levels are reduced by 11.8% and 16.5%, respectively. The longest runtime is about 30 minutes.

ABC is a public-domain system for logic synthesis and formal verification of binary logic circuits appearing in synchronous hardware designs. ABC combines scalable logic transformations based on And-Inverter Graphs (AIGs), with a variety of innovative algorithms. A focus on the synergy of sequential synthesis and sequential verification leads to improvements in both domains. This paper introduces ABC, motivates its development, and illustrates its use in formal verification.

This paper presents a fast global method for delay optimization after technology mapping. Timing analysis is used to identify timing-critical areas in the mapped network where new structures are synthesized to favor late-arriving signals. Unlike previous methods that make incremental local changes to the mapped network, the proposed method records many alternative structures and defers the final decision to the technology mapper. Experimental results for networks mapped into 6-input look-up tables (6-LUTs) show that the delay is, on average, improved 14% using a realistic delay library for LUTs with variable-pin delays and wire-delay estimation. The area penalty after the delay optimization is about 2% and can be eliminated by area-oriented resynthesis. When the algorithm is compared with DAOmap, the experimental results show 27% logic level reduction while the area is increased by only 1%. The algorithm is also fast and applicable to very large networks. The runtime of the proposed algorithm is 16x and 3x faster than DAOmap for large industrial and academic designs, respectively.

The process of sequential redundancy identification is the cornerstone of sequential synthesis and equivalence checking frameworks. The scalability of the proof obligations inherent in redundancy identification hinges not only upon the ability to cross-assume those redundancies, but also upon the way in which these assumptions are leveraged. In this paper, we study the technique of speculative reduction for efficiently modeling redundancy assumptions. We provide theoretical and experimental evidence to demonstrate that speculative reduction is fundamental to the scalability of the redundancy identification process under various proof techniques. We also propose several techniques to speed up induction-based redundancy identification. Experiments demonstrate the effectiveness of our techniques in enabling substantially faster redundancy identification, up to six orders of magnitude on large designs.

In the digital VLSI cycle, logic transformations are often required to modify the design to meet different synthesis and optimization goals. Logic transformations on sequential circuits are hard to perform due to the vast underlying solution space. This paper proposes an SPFD-based sequential logic transformation methodology to tackle the problem with no sacrifice on performance. It first presents an efficient approach to construct approximate SPFDs (aSPFDs) for sequential circuits. Then, it demonstrates an algorithm using aSPFDs to perform the desirable sequential logic transformations using both combinational and sequential don't cares. Experimental results show the effectiveness and robustness of the approach.

In recent years, the maximum logic capacity of each successive FPGA family has been increasing by more than 50%, which motivates scalable solutions. Meanwhile, academic research in logic synthesis has been fruitful, but these advances have been demonstrated on academic architectures and benchmark designs which are not representative of modern industrial FPGAs. This paper presents a framework (SmartOpt) for mapping complex FPGA architectures to a simple netlist model, which can be supported by academic tools. SmartOpt was applied to leverage the algorithms implemented in the ABC package and to study their relative contributions. This work is integrated into the Xilinx ISE 11.1 software flow for FPGAs and shows significant improvements in both the LUT count and performance of large industrial circuits described in HDL. Xilinx Synthesis Technology (XST) reference flow was compared experimentally against the same flow augmented by SmartOpt. When applied to a set of 20 large industrial Virtex-5 benchmarks ranging from 17K to 69K 6-LUTs, the augmented flow produced 8.3% fewer LUTs and led to 2.1% higher operating frequency while keeping runtimes reasonable. With dual-LUT-merging, the LUT count is reduced by 22.7%, while increasing the operating frequency only by 0.7%.

We describe an optimization method for combinational and sequential logic networks, with emphasis on scalability and the scope of optimization. The proposed resynthesis (a) is capable of substantial logic restructuring, (b) is customizable to solve a variety of optimization tasks, and (c) has reasonable runtime on industrial designs. The approach uses don't cares computed for a window surrounding a node and can take into account external don't cares (e.g. unreachable states). It uses a SAT solver and interpolation to find a new representation for a node. This representation can be in terms of inputs from other nodes in the window thus effecting Boolean re-substitution. Experimental results on 6-input LUT networks after high effort synthesis show substantial reductions in area and delay. When applied to 20 large academic benchmarks, the LUT count and logic level is reduced by 45.0% and 12.2%, respectively. The longest runtime for synthesis and mapping is about two minutes. When applied to a set of 14 industrial benchmarks ranging up to 83K 6-LUTs, the LUT count and logic level is reduced by 11.8% and 16.5%, respectively. Experimental results on 6-input LUT networks after high-effort synthesis show substantial reductions in area and delay. The longest runtime is about 30 minutes.

This paper presents a new type of sequential technology independent synthesis. Building on the previous notions of combinational observability and sequential equivalence, sequential observability is introduced and discussed. By considering both the sequential nature of the design and observability simultaneously, better results can be obtained than with either algorithm alone. The experimental results show that this method can reduce the technology-independent gate count up to 10% more than the previously best known synthesis techniques.

We demonstrate that a maximum-flow-based approach to register-minimization is a useful platform for incorporating varied design constraints. In this work, we extend the flowbased formulation to include timing constraints and to guarantee the existence of an equivalent initial state. Reducing the register count is motivated by positive consequences for physical design, verification, and power consumption, but it is critically necessary for synthesis that these timing and functionality requirements are also met. Our solution is optimum in the number of registers under either or both constraints and also possesses several other distinct advantages: the runtime is significantly faster than comparable techniques, the algorithm is capable of early termination with a timing-feasible solution, and both maximum and minimum path constraints can be specified.

This work presents a technology-independent synthesis optimization that is effective in reducing the total number of state elements of a design. It works by identifying and eliminating dependent state elements which may be expressed as functions of other registers. For scalability, we rely exclusively on SAT- based analysis in this process. To enable optimal identification of all dependent state elements, we integrate an inductive invariant generation framework. We introduce numerous techniques to heuristically enhance the reduction potential of our method, and experiments confirm that our approach is scalable and is able to reduce state element count by 12% on average in large industrial designs, even after other aggressive optimizations such as min- register retiming have been applied. The method is effective in simplifying later verification efforts.

Performing synthesis and verification in isolation has two undesirable consequences: (1) verification runs the risk of becoming intractable, and (2) strong sequential optimizations are not applied because they are hard to verify. This paper proposes a format for recording synthesis information and a methodology for sequential equivalence checking using this feedback from synthesis. An implementation is described and experimentally compared against an efficient general-purpose sequential equivalence checker that does not use synthesis information. Experimental results confirm expected substantial savings in runtime and reliability of equivalence checking for large designs.

This paper presents new methods for restructuring logic networks based on fast Boolean techniques. The basis for these are 1) a cut-based view of a logic network, 2) exploiting the uniqueness and speed of disjoint-support decompositions, 3) a new heuristic for speeding these up, 4) extending these to general decompositions, and 5) limiting local transformations to functions with 16 or less inputs so that fast truth table manipulations can be used in all operations. Boolean methods lessen the structural bias of algebraic methods, while still allowing for high speed and multiple iterations. Experimental results on K-LUT networks show an average additional reduction of 5.4% in LUT count, while preserving delay, compared to heavily optimized versions of the same networks.

This paper describes an efficient implementation of sequential synthesis that uses induction to detect and merge sequentially-equivalent nodes. State-encoding, scan chains, and test vectors are essentially preserved. Moreover, the sequential synthesis results are sequentially verifiable using an independent inductive prover similar to that used for synthesis, with guaranteed completeness. Experiments with this sequential synthesis show effectiveness. When applied to a set of 20 industrial benchmarks ranging up to 26 K registers and up to 53 K 6 -LUTs, average reductions in register and area are 12.9% and 13.1% respectively while delay is reduced by 1.4%. When applied to the largest academic benchmarks, an average reduction in both registers and area is more than 30%. The associated sequential verification is also scalable and runs about 2times slower than synthesis. The implementation is available in the synthesis and verification system ABC.

We present an algorithm for improving the performance of carry-save-adder (CSA) style multipliers. Based on placement information, the algorithm exploits the arithmetic equivalence in the CSA multipliers and rewires to improve the slack of the multiplier.

In the digital VLSI cycle, a netlist is often modified to correct design errors, perform small specification changes or implement incremental rewiring-based optimization operations. Most existing automated logic rectification tools use a small set of predefined logic transformations when they perform such modifications. This paper first shows that a small set of predefined transformations may not allow rectification to exploit the full potential of the design. Then, it proposes an automated simulation-based methodology to "approximate" sets of pairs of functions to be distinguished (SPFDs) and avoid the memory/time explosion problem. This representation is used by a SAT-based algorithm that devises appropriate logic transformations to fix a design. The SAT method is later complemented by a greedy one that improves on runtime performance. An extensive suite of experiments documents the added potential of the proposed rectification methodology.

Modern combinational equivalence checking (CEC) engines are complicated programs which are difficult to verify. In this paper we show how a modern CEC engine can be modified to produce a proof of equivalence when it proves a miter unsatisfiable. If the CEC engine formulates the problem as a single SAT instance (call this naive), one can use the resolution proof of unsatisfiability as a proof of equivalence. However, a modern CEC engine does not directly invoke a SAT solver for the whole miter, but instead uses a variety of techniques such as structural hashing, detection of intermediate functional equivalences, and circuit re-writing to first simplify the problem. We show that in spite of using these simplification techniques, a CEC engine can be modified to generate a single (extended) resolution proof for the whole miter just as in the naive case. The benefit of having a single proof is that the proof verification program remains extremely simple, and its correctness is much easier to establish than that of the CEC engine.

Model checking can be aided by inductive invariants, small local properties that can be proved by simple induction. We present a way to automatically extract inductive invariants from a design and then prove them. The set of candidate invariants is broad, expensive to prove, and many invariants can be shown to not be helpful to model checking. In this work, we develop a new method for systematically exploring the space of candidate inductive invariants, which allows us to find and prove invariants that are few in number and immediately help the problem at hand. This method is applied to interpolation where invariants are used to refute an error trace and help discard spurious counterexamples.

We present a formulation of retiming to minimize the number of registers in a design by iterating a maximum network flow problem. The retiming returned will be the optimum one, which involves the minimum amount of register movement. Existing methods solve this problem as an instance of minimum-cost network flow, an asymptotically and practically more difficult problem than maximum flow. Furthermore, because all flows are unitary, the problem can be simplified to binary marking. Our algorithm has a worst-case bound of O(R^2 E), where R is the number of registers and E the number of pair-wise connections. We demonstrate on a set of circuits that our formulation is 5x faster than minimum-cost-based methods.

The paper addresses the problem of designing a component that combined with a known part of a system, called the context FSM, is a reduction of a given specification FSM. We study compositionally progressive solutions of synchronous FSM equations. Such solutions, when combined with the context, do not block any input that may occur in the specification, so they are of practical use. We show that if a synchronous FSM equation has a compositionally progressive solution, then the equation has the largest compositionally progressive solution. We provide an algorithm to compute the largest compositionally progressive solution that splits states of the largest solution and then removes those inducing a non-progressive composition.

An algorithm for technology mapping of combinational and sequential logic networks is proposed and applied to mapping into K-input lookup-tables (K-LUTs). The new algorithm avoids the hurdle of computing all K-input cuts while preserving the quality of the results, in terms of area and depth. The memory and runtime of the proposed algorithm are linear in circuit size and quite affordable even for large industrial designs. For example, computing a good quality 6-LUT mapping of an AIG with 1M nodes takes 150Mb of RAM and 1 minute on a typical laptop. An extension of the algorithm allows for sequential mapping, which searches the combined space of all possible mappings and retimings. This leads to an 18–22% improvement in depth with a 3–5% LUT count penalty, compared to combinational mapping followed by retiming.

The orientation of a bus is defined as the direction from the Least Significant Bit (LSB) to the Most Significant Bit (MSB). Bused pin flipping is a property that allows several bused pins to flip without changing the system functionality. In this paper a simultaneous bus orientation and bused pin flipping algorithm is presented. The algorithm can be integrated into a bus-centric floorplanner targeting bus-rich designs such as microprocessors. Experimental results show that a floorplanner enhanced by the algorithm produces high quality floorplans in terms of bus routing

A bus routing algorithm is presented which not only minimizes wire length but also selects the bits in the bus to avoid twisting and conflicts. The resulting bus routes are regular, thus having strong immunity to variations. Minimization for wire length/delay differences between different bits is also implemented.

This paper presents several orthogonal improvements to the state-of-the-art lookup table (LUT)-based field-programmable gate array (FPGA) technology mapping. The improvements target the delay and area of technology mapping as well as the runtime and memory requirements. 1) Improved cut enumeration computes all K-feasible cuts, without pruning, for up to seven inputs for the largest Microelectronics Center of North Carolina benchmarks. A new technique for on-the-fly cut dropping reduces, by orders of magnitude, the memory needed to represent cuts for large designs. 2) The notion of cut factorization is introduced, in which one computes a subset of cuts for a node and generates other cuts from that subset as needed. Two cut factorization schemes are presented, and a new algorithm that uses cut factorization for delay-oriented mapping for FPGAs with large LUTs is proposed. 3) Improved area recovery leads to mappings with the area, on average, 6% smaller than the previous best work while preserving the delay optimality when starting from the same optimized netlists. 4) Lossless synthesis accumulates alternative circuit structures seen during logic optimization. Extending the mapper to use structural choices reduces the delay, on average, by 6% and the area by 12%, compared with the previous work, while increasing the runtime 1.6 times. Performing five iterations of mapping with choices reduces the delay by 10% and the area by 19% while increasing the runtime eight times. These improvements, on top of the state-of-the-art methods for LUT mapping, are available in the package ABC

This paper presents a technique for preprocessing combinational logic before technology mapping. The technique is based on the representation of combinational logic using And-Inverter Graphs (AIGs), a networks of two-input ANDs and inverters. The optimization works by alternating DAG-aware AIG rewriting, which reduces area by sharing common logic without increasing delay, and algebraic AIG balancing, which minimizes delay without increasing area. The new technology-independent flow is implemented in a public-domain tool ABC. Experiments on large industrial benchmarks show that the proposed methodology scales to very large designs and is several orders of magnitude faster than SIS and MVSIS while offering comparable or better quality when measured by the quality of the network after mapping.

Classical two-variable symmetries play an important role in many EDA applications, ranging from logic synthesis to formal verification. This paper proposes a complete circuit-based method that makes uses of structural analysis, integrated simulation and Boolean satisfiability for fast and scalable detection of classical symmetries of completely-specified Boolean functions. This is in contrast to previous incomplete circuit-based methods and complete BDD-based methods. Experimental results demonstrate that the proposed method works for large Boolean functions, for which BDDs cannot be constructed.

The paper presents several improvements to state-of-the-art in FPGA technology mapping exemplified by a recent advanced technology mapper DAOmap [Chen and Cong, ICCAD '04]. Improved cut enumeration computes all K-feasible cuts without pruning for up to 7 inputs for the largest MCNC benchmarks. A new technique for on-the-fly cut dropping reduces by orders of magnitude memory needed to represent cuts for large designs. Improved area recovery leads to mappings with area on average 7% smaller than DAOmap, while preserving delay optimality when starting from the same optimized netlists. Applying mapping with structural choices derived by a synthesis flow on average reduces delay by 7% and area by 14%, compared to DAOmap.

Enumeration of bounded size cuts is an important step in several logic synthesis algorithms such as technology mapping and re-writing. The standard algorithm does not scale beyond 6 or 7 inputs because it enumerates all cuts and there are too many of them. We address the enumeration problem by introducing the notion of cut factorization. In cut factorization, one enumerates global and local cuts (collectively called the factor cuts) of the network, and uses these to generate other cuts. Depending on how global and local cuts are defined, one obtains different factorization schemes. In the first scheme, complete factorization, it is possible to generate any cut from factor cuts. However, complete factorization is expensive though less expensive than exhaustive enumeration. In the second scheme, partial factorization, there is no guarantee of generating all cuts from factor cuts. However, it is much faster, and produces good results. In this paper we also present two applications of factor cuts: LUT mapping and macrocell mapping. In LUT mapping, we find that considering only factor cuts guarantees depth optimality for most nodes in the network. For the remaining nodes, other cuts need to be generated from factor cuts and examined. In macrocell mapping, we focus on a particular 9-input macrocell, and use factor cuts as a heuristic method to improve depth by reducing structural bias. Factor cuts are used to map the macrocell as a whole whenever possible instead of mapping its parts separately. In this context factor cuts enable a new quality-run-time tradeoff between mapping parts of the macrocell separately (poor quality), and mapping using all 9-input cuts (long run-time).

The paper explores several ways to improve the speed and capacity of combinational equivalence checking based on Boolean satisfiability (SAT). State-of-the-art methods use simulation and BDD/SAT sweeping on the input side (i.e. proving equivalence of some internal nodes in a topological order), interleaved with attempts to run SAT on the output (i.e. proving equivalence of the output to constant 0). This paper improves on this method by (a) using more intelligent simulation, (b) using CNF-based SAT with circuit-based decision heuristics, and (c) interleaving SAT with low-effort logic synthesis. Experimental results on public and industrial benchmarks demonstrate substantial reductions in runtime, compared to the current methods. In several cases, the new solver succeeded in solving previously unsolved problems.

Technology mapping, based on directed acyclic graph covering, suffers from the problem of structural bias: The structure of the mapped netlist depends strongly on the subject graph. In this paper, the authors present a new mapper aimed at mitigating structural bias. It is based on a simplified cut-based Boolean-matching algorithm, and using the speed afforded by this simplification, they explore two ideas to reduce structural bias. The first, called lossless synthesis, leverages recent advances in structure-based combinational-equivalence checking to combine the different networks seen during technology-independent synthesis into a single network with choices in a scalable manner. They show how cut-based mapping extends naturally to handle such networks with choices. The second idea is to combine several library gates into a single gate (called a supergate) in order to make the matching process less local. They show how supergates help address the structural-bias problem and how they fit naturally into the cut-based Boolean-matching scheme. An implementation based on these ideas significantly outperforms state-of-the-art mappers in terms of delay, area, and run-time on academic and industrial benchmarks

Transformations using retiming and resynthesis operations are the most important and practical (if not the only) techniques used in optimizing synchronous hardware systems. Although these transformations have been studied extensively for over a decade, questions about their optimization capability and verification complexity are not answered fully. Resolving these questions may be crucial in developing more effective synthesis and verification algorithms. This paper settles the above two open problems. The optimization potential is resolved through a constructive algorithm which determines if two given finite state machines (FSMs) are transformable to each other via retiming and resynthesis operations. Verifying the equivalence of two FSMs under such transformations, when the history of iterative transformation is unknown, is proved to be polynomial-space-complete and hence just as hard as general equivalence checking, contrary to a common belief. As a result, we advocate a conservative design methodology for the optimization of synchronous hardware systems to ameliorate verifiability. Our analysis reveals some properties about initializing FSMs transformed under retiming and resynthesis. On the positive side, a lag-independent bound is established on the length increase of initialization sequences for FSMs under retiming. It allows a simpler incremental construction of initialization sequences compared to prior approaches. On the negative side, we show that there is no analogous transformation-independent bound when resynthesis and retiming are iterated. Nonetheless, an algorithm computing the exact length increase is presented

Both nondeterminism and multilevel networks can be used to compactly characterize logic structures as well as all the flexibilities allowed for optimizing them. Synthesis results can be improved by allowing the manipulation of a larger class of networks called nondeterministic (ND) networks. These are multilevel logic networks that embody both nondeterminism and multivalued (MV) signals and, thus, enhance compactness and expressiveness. In this paper, a complete theory for representing and manipulating ND networks is developed. It is shown that an ND network's behavior can be classified into at least three types, all of which coalesce when the network becomes deterministic. The theory addresses the classical transformations commonly applied to optimize deterministic binary networks, such as node minimization, elimination, and decomposition. These are analyzed with respect to their effects on each type of network behavior, leading to modifications of some operations to make them safe, i.e., guaranteeing that the new behavior remains within the network's specification. Finally, it is proved that all three types of behaviors can be used in a hierarchical-synthesis paradigm

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

The paper describes an improved approach to Boolean network optimization using internal don't-cares. The improvements concern the type of don't-cares computed, their scope, and the computation method. Instead of the traditionally used compatible observability don't-cares (CODCs), we introduce and justify the use of complete don't-cares (CDC). To ensure the robustness of the don't-care computation for very large industrial networks, an optional windowing scheme is implemented that computes substantial subsets of the CDCs in reasonable time. Finally, we give a SAT-based don't-care computation algorithm that is more efficient than BDD-based algorithms. Experimental results confirm that these improvements work well in practice. Complete don't-cares allow for a reduction in the number of literals compared to the CODCs. Windowing guarantees robustness, even for very large benchmarks on which previous methods could not be applied. SAT reduces the runtime and enhances robustness, making don't-cares affordable for a variety of other Boolean methods applied to the network.

A class of discrete event synthesis problems can be reduced to solving language equations, F /spl middot/ X /spl sube/ S, where F is the fixed component and S the specification. Sequential synthesis deals with FSMs when the automata for F and S are prefix closed. and are naturally represented by multi-level networks with latches. For this special case, we present an efficient computation, using partitioned representations, of the most general prefix-closed solution of the above class of language equations. The transition and the output relations of the FSMs for F and S in their partitioned form are represented by the sets of output and next state functions of the corresponding networks. Experimentally, we show that using partitioned representations is much faster than using monolithic representations, as well as applicable to larger problem instances.

Technology mapping based on DAG-covering suffers from the problem of structural bias: the structure of the mapped netlist depends strongly on the subject graph. In this paper we present a new mapper aimed at mitigating structural bias. It is based on a simplified cut-based Boolean matching algorithm, and using the speed afforded by this simplification we explore two ideas to reduce structural bias. The first, called lossless synthesis, leverages recent advances in structure-based combinational equivalence checking to combine the different networks seen during technology independent synthesis into a single network with choices in a scalable manner. We show how cut based mapping extends naturally to handle such networks with choices. The second idea is to combine several library gates into a single gate (called a supergate) in order to make the matching process less local. We show how supergates help address the structural bias problem, and how they fit naturally into the cut-based Boolean matching scheme. An implementation based on these ideas significantly outperforms state-of-the-art mappers in terms of delay, area and run-time on academic and industrial benchmarks.

We discuss a new synthesis flow, which offers the ability to do easy delay testing almost free in terms of its impact on speed and area compared to corresponding implementations with standard cells. The methodology uses matched delays in pre-charged PLAs and bundled routing to produce a completion signal, which is guaranteed to lie on all critical paths. We give a nondelay testing method for ensuring matched delays are correct, i.e. that all completion signals arrive after their corresponding data signals. The design margins of the matched delays can be small since they are internal to the PLAs, which are regular structures and therefore more predictable.

A Module-Based design flow for digital ICs with hard and soft modules is presented. Versions of the soft modules are implemented with different area/delay characteristics. The versions represent flexibility that can be used in the physical design to meet timing requirements. The flow aims at minimizing the clock cycle of the chip while providing quicker turn-around time. Unreliable wiring estimation is eliminated and costly iterations are reduced resulting in substantial reductions in run time as well as a significant decrease in the clock periods.

This work presents two contributions. The first is an incremental placement algorithm for placement-aware logic synthesis along with a proof of optimality. The algorithm can efficiently compute the optimum location for a newly introduced node in a network that minimizes the incremental increase in the total half-perimeter wire-length of the network. The algorithm can be applied in a variety of placement-aware optimization contexts. The second contribution is a specific application of this algorithm to placement-aware common divisor extraction. We evaluate the effectiveness of the proposed extraction procedure by using it in an otherwise non-placement-aware flow with two different final placers. The first flow uses an industrial congestion-driven placer and results in an average reduction of 21% in congestion as measured by the global router. The second flow uses an academic wire-length-driven placer and results in an average reduction of 11% for a tool-specific measure of congestion estimated from the placement. Our experiments also reveal a rather surprising phenomenon: in many cases the attempt to minimize the wire-length results in fewer literals after extraction than with a conventional literal-driven approach.

In the course of hardware system design or real-time process control, high-level specifications may contain simultaneous definitions of concurrent modules whose information flow forms cyclic dependencies without the separation of state-holding elements. The temporal behavior of these cyclic definitions may be meant to be combinational rather than sequential. Most prior approaches to analyzing cyclic combinational circuits were built upon the formulation of ternary-valued simulation at the circuit level. This work shows the limitation of this formulation and investigates, at the functional level, the most general condition where cyclic definitions are semantically combinational. It turns out that the prior formulation is a special case of our treatment. Our result admits strictly more flexible high-level specifications. Furthermore, it allows a higher-level analysis of combinationality, and, thus, no costly synthesis of a high-level description into a circuit netlist before combinationality analysis can be performed. With our formulation, when the target is software implementations, combinational cycles need not be broken as long as the execution of the underlying system obeys a sequencing execution rule. For hardware implementations, combinational cycles are broken and replaced with acyclic equivalents at the functional level to avoid malfunctioning in the final physical realization.

Wire removal is a technique by which the total number of wires between individual circuit nodes is reduced, either by removing wires or replacing them with other new wires. The wire removal techniques we describe in this paper are based on both binary and multivalued sets of pairs of functions to be distinguished (SPFDs). Recently, it was shown that a design style based on a multilevel network of approximately equal-sized programmable logic arrays (PLAs) results in a dense, fast, and crosstalk-resistant layout. This paper describes the application of SPFD-based wire removal techniques for circuit implementations utilizing networks of PLAs as well as standard-cells. In our first set of wire removal experiments (which utilize binary SPFD-based wire removal), we demonstrate that the benefit of SPFD-based wire removal is insignificant when the circuit is mapped using standard cells. We demonstrate that this technique is very effective in the context of a network of PLAs. In the next set of wire removal experiments, we focus only on circuits implemented using a network of PLAs. Three separate wire removal experiments are performed. Wire removal is invoked before clustering the original netlist into a network of PLAs, or after clustering, or both before and after clustering. For wire removal before clustering, binary SPFD-based wire removal is used. For wire removal after clustering, multivalued SPFD-based wire removal is used since the multioutput PLAs can be viewed as multivalued single output nodes. We demonstrate that these techniques are effective. The most effective approach is to perform wire removal both before and after clustering. Using these techniques, we obtain a reduction in placed and routed circuit area of about 11%. This reduction is significantly higher (about 20%) for the larger circuits we used in our experiments.

Extended Finite State Machines (EFSMs) have been proposed to model control oriented systems. A version of this, with the data portion modeled by Presburger arithmetic, has been used in formal verification and test pattern generation. This paper proposes a general logic minimization scheme using don't care derived from both control and data path. It consists of methods to transfer don't cares through the data path and to generate logic don't cares from the data path using quantifier-free Presburger inequalities. Potential applications are discussed and preliminary results validate the scheme on reasonable examples.

Logic evaluation of a Boolean function or relation is traditionally done by simulating its gate-level implementation, or creating a branching program using its Binary Decision Diagram (BDD) representation, or using a set of look-up tables. We propose a new approach called generalized cofactoring diagrams, which are a generalization of the above methods. Algorithms are given for finding the optimal cofactoring structure for free-ordered BDD's and generalized cube cofactoring under an average path length (APL) cost criterion. Experiments on multi-valued functions show superior results to previously known methods by an average of 30%. The framework has direct applications in logic simulation, software synthesis for embedded control applications, and functional decomposition in logic synthesis.

Both non-determinism and multi-level networks compactly characterize the flexibility allowed in implementing a circuit. A theory for representing and manipulating non-deterministic (ND) multi-level networks is developed. The theory supports all the network manipulations commonly applied to deterministic binary networks, such as node minimization, elimination, and decomposition. It is shown that an ND network's behavior can be interpreted in three ways, all of which coincide when the network is deterministic. Operations performed on an ND network are analyzed under each interpretation for changes in a network's behavior. Modifications of a few operations are given which must be used to guarantee that a network's behavior does not violate its external specification. These modifications depend on which behavior is being used and the location of related non-determinism. This theory has been implemented in a system, MVSIS. We provide comparisons among the uses of the various behaviors.

A block-level placement and routing scheme called Fishbone is presented. The routing uses a two-layer spine topology. The pin locations are configurable and restricted to certain routing grids in order to ensure full routability and precise predictability. With this scheme, exact net topologies are determined by pin positions only; hence during block placement, net parameters such as wire length (and delay) can be derived directly. The construction of Fishbone nets is much faster than for Steiner trees; this enables the integration of block placement and routing; there is no separate routing stage.

The state-explosion problem limits formal verification on large sequential circuits partly because the sizes of binary decision diagrams (BDDs) sizes heavily depend on the number of variables dealt with. In the worst case, a BDD size grows exponentially with the number of variables. Thus, reducing this number can possibly increase the verification capacity. In particular, this paper shows how sequential equivalence checking can be done in the sum state space. Given two finite state machines M/sub 1/ and M/sub 2/ with numbers of state variables m/sub 1/ and m/sub 2/, respectively, conventional formal methods verify equivalence by traversing the state space of the product machine with m/sub 1/+m/sub 2/ registers. In contrast, this paper introduces a different possibility, based on partitioning the state space defined by a multiplexed machine, which can have merely max{m/sub 1/,m/sub 2/}+1 registers. This substantial reduction in state variables potentially enables the verification of larger instances. Experimental results show the approach can verify benchmarks with up to 312 registers, including all of the control outputs of microprocessor 8085.

Two regular circuit structures based on the programmable logic array (PLA) are proposed. They provide alternatives to the widely used standard-cell structure and have better predictability and simpler design methodologies. A whirlpool PLA is a cyclic four-level structure, which has a compact layout. Doppio-ESPRESSO, a four-level logic minimization algorithm, is developed for the synthesis of Whirlpool PLAs. A river PLA is a stack of multiple output PLAs, which uses river routing for the interconnections of the adjacent PLAs. A synthesis algorithm for river PLAs uses multilevel logic synthesis, simulated-annealing, and ESPRESSO targeting a combination of minimal area and delay.

We study the problem of optimizing synchronous sequential circuits. There have been previous efforts to optimize such circuits. However, all previous attempts make implicit or explicit assumptions about the design or the environment of the design. For example, it is widespread practice to assume the existence of a hardware reset line and consequently a fixed power-up state; in the absence of the same, a common premise is that the design's environment will apply an initializing sequence. We review the concept of safe replaceability which does away with these assumptions and the delay-safe replaceability notion, which is applicable when the design's output is not used for a certain number of cycles after power-up. We then develop procedures for optimizing the combinational next-state and output logic, as well as routines for reencoding the state space and removing state bits under these replaceability criteria. Experimental results demonstrate the effectiveness of our algorithms.

This paper addresses the problem of automatic generation of implementation software from high-level functional specifications in the context of embedded system on chip designs. Software design complexity for embedded systems has increased so much that a high-level functional programming paradigm need to be adopted for formal verifiability, maintainability and short time-to-market. We propose a framework for efficiently generating implementation software from a synchronous state machine specification for embedded control systems. The framework is generic enough to allow hardware/software partition for a given architecture platform. It is demonstrated that the logic optimization and simulation techniques can be combined to produce fast execution code for such embedded systems. Specifically, we propose a framework for software synthesis from multi-valued logic, including fast evaluation of logic functions, and scheduling techniques for node execution. Experiments are performed to show the initial results of our algorithms in this framework.

A regular circuit structure called a River PLA and its re-configurable version, Glacier PLA, are presented. River PLAs provide greater regularity than circuits implemented with standard-cells. Conventional optimization stages such as technology mapping, placement and routing are eliminated. These two features make the River PLA a highly predictable structure. Glacier PLAs can be an alternative to FPGAs, but with a simpler and more efficient design methodology.

We introduce the notion of problem symmetry in search-based SAT algorithms. We develop a theory of essential points to formally characterize the potential search-space pruning that can be realized by exploiting problem symmetry. We unify several search-pruning techniques used in modern SAT solvers under a single framework, by showing them to be special cases of the general theory of essential points. We also propose a new pruning rule exploiting problem symmetry. Preliminary experimental results validate the efficacy of this rule in providing additional search-space pruning beyond the pruning realized by techniques implemented in leading-edge SAT solvers.

We discuss the simplification of non-deterministic MV networks and their internal nodes using internal flexibilities. Given the network structure and its external specification, the flexibility at a node is derived as a non-deterministic MV relation. This flexibility is used to simplify the node representation and enhance the effect of Boolean resubstitution. We show that the flexibility derived is maximum. The proposed approach has been implemented and tested in MVSIS [16]. Experimental results show that it performs well on a variety of MV and binary benchmarks.

A regular circuit structure called a Whirlpool PLA (WPLA) is proposed. It is suitable for the implementation of finite state machines as well as combinational logic. A WPLA is logically a four-level Boolean NOR network. By arranging the four logic arrays in a cycle, a compact layout is achieved. Doppio-ESPRESSO, a four-level logic minimization algorithm is developed for WPLA synthesis. No technology mapping, placement or routing is necessary for the WPLA. Area and delay trade-off is absent, because these two goals are usually compatible in WPLA synthesis.

SPFDs, a mechanism for expressing flexibility during logic synthesis, were first introduced for FPGA synthesis. They were then extended to general, combinational Boolean networks and later the concept of sequential SPFDs was introduced. In this paper, we explore the idea of using SPFDs for functional decomposition. A new type of functional decomposition called topologically constrained decomposition is introduced. An algorithm is provided for solving this problem using SPFDs. Preliminary experimental results are encouraging and indicate the feasibility of the approach. A scheme is also presented for generating instances of the topologically constrained decomposition problem.

This paper addresses the problem of combinational equivalence checking (CEC) which forms one of the key components of the current verification methodology for digital systems. A number of recently proposed BDD based approaches have met with considerable success in this area. However, the growing gap between the capability of current solvers and the complexity of verification instances necessitates the exploration of alternative, better solutions. This paper revisits the application of Satisfiability (SAT) algorithms to the combinational equivalence checking (CEC) problem. We argue that SAT is a more robust and flexible engine of Boolean reasoning for the CEC application than BDDs, which have traditionally been the method of choice. Preliminary results on a simple framework for SAT based CEC show a speedup of up to two orders of magnitude compared to state-of-the-art SAT based methods for CEC and also demonstrate that even with this simple algorithm and untuned prototype implementation it is only moderately slower and sometimes faster than a state-of-the-art BDD based mixed engine commercial CEC tool. While SAT based CEC methods need further research and tuning before they can surpass almost a decade of research in BDD based CEC, the recent progress is very promising and merits continued research.

CODCs stands for compatible observability don't cares. We first examine the definition of compatibility and when a set of CODCs is compatible. We then discuss Savoj's CODC computation for propagating CODCs from a node's output to its fanins, and show by example, that the results can depend on the current implementation of the node. Then we generalize the computation so that the result is independent of the implementation at the node. The CODCs propagated by this computation are proved to be maximal in some sense. Local don't cares (LDCs) are CODCs of a node, pre-imaged to the primary inputs and then imaged and projected to the local fanins of the node. LDCs combine CODCs with SDCs (satisfiability don't cares), but only the CODC part is propagated to the fanin network. Another form of local don't cares, propagates both the CODC and SDC parts to the fanin network. Both are shown to be compatible in some sense, but conservative. We give a method for updating both kinds of local don't cares incrementally when other nodes in the network are changed.

A new routing algorithm is presented. It is based on a multiple star net model, force-directed placement and maze searching techniques. The algorithm inherits the power of maze routing in that it is able to route complex layouts with various obstructions. The large memory requirement of the conventional maze algorithm is alleviated through successive net refinement, which constrains the maze searching to small regions. The algorithm shows advantages in routing designs with complicated layout obstructions.

SPFDs are a mechanism to express flexibility in Boolean networks. Introduced by Yamashita et al. in the context of FPGA synthesis [1996], they were extended later to general combinational networks. We introduce the concept of sequential SPFDs and provide an algorithm to compute them based on a partition of the state bits. The SPFDs, of each component in the partition are used to generate equivalence classes of states. We provide a formal relation between the resulting state classification and the equivalence classes produced by classical state minimization of completely specified machines. The SPFDs, associated with the state bits can be applied for re-encoding the state space. For this, we give an algorithm to re-synthesize the sequential circuit using sequential SPFDs and the new state re-encoding.

The problem of designing a component that, combined with a known part of a system, conforms to a given overall specification arises in several applications ranging from logic synthesis to the design of discrete controllers. We cast the problem as solving abstract equations over languages. Language equations can be defined with respect to several language composition operators such as synchronous composition, /spl middot/, and parallel composition, /spl square/; conformity can be checked by language containment. In this paper, we address parallel language equations. Parallel composition arises in the context of modeling delay-insensitive processes and their environments. The parallel composition operator models an exchange protocol by which an input is followed by an output after a finite exchange of internal signals. It abstracts a system with two components with a single message in transit, such that at each instance either the components exchange messages or one of them communicates with its environment, which submits the next external input to the system only after the system has produced an external output in response to the previous input. We study the most general solutions of the language equation A/spl square/X/spl sube/C, and define the language operators needed to express them. Then we specialize such equations to languages associated with important classes of automata used for modeling systems, e.g., regular languages and FSM languages. In particular, for A/spl square/X/spl sube/C, we give algorithms for computing: the largest FSM language solution, the largest complete solution, and the largest solution whose composition with A yields a complete FSM language. We solve also FSM equations under bounded parallel composition. In this paper, we give concrete algorithms for computing such solutions, and state and prove their correctness.

The timing-driven macro-cell placement algorithm described is based on the force-directed technique. The proposed star net model enables more accurate timing analysis, hence path delay constraints can be handled. In addition, the placer provides functions such as determination of cell orientation, routing estimation and pad placement. The algorithm is iterative and incremental, allowing flexibility in the physical design flow. The placer competes with commercial physical design tools and gives better results in terms of path delay.

We address the problem of developing suitable criteria for design replacement in the context of sequential logic synthesis. There have been previous efforts to characterize replacements for such designs. However, all previous attempts either make implicit or explicit assumptions about the design or the environment of the design. For example, it is widespread practice to assume the existence of a hardware reset line and, consequently, a fixed power-up state; in the absence of the same, a common premise is that the design's environment will apply an initializing sequence. We present the notion of safe replaceability, which does away with these assumptions, and prove a number of properties that hold of it. Most importantly, we show that the notion is sound, i.e., if design D/sub 1/ is a safe replacement for design D/sub 0/, then no environment can determine if D/sub 1/ is used in place of D/sub 0/ and that the notion is complete, i.e., if D/sub 1/ is not a safe replacement for D/sub 0/ then there exists an environment that can detect if D/sub 1/ is used in place of D/sub 0/. Completeness is important for logic synthesis and verification because it specifies the maximum allowable flexibility for replacement. When the design's output is not used for a certain number of cycles after power up, then safe replaceability can be relaxed to obtain what we refer to as delay safe replaceability; we analyze properties of this notion too. Since our work, many papers have used this notion effectively for sequential optimization.

We present a technology mapping procedure in which an area-delay trade-off curve is constructed at each node using matches found for different decompositions of the node. This information is used effectively to find implementations that meet delay constraints while reducing area. The procedure combines state-of-the-art mapping procedures, in which a graph covering is applied to a special graph structure which succinctly encodes many representations. Major challenges were avoiding memory explosion and finding good cost estimations. The combined procedure outperforms the best result among any of the procedures used separately.

We address optimizing multi-valued (MV) logic functions in a multi-level combinational logic network. Each node in the network, called an MV-node, has multi-valued inputs and single multi-valued output. The notion of don't cares used in binary logic is generalized to multi-valued logic. It contains two types of flexibility: incomplete specification and non-determinism. We generalize the computation of observability don't cares for a multi-valued function node. Methods are given to compute (a) the maximum set of observability don't cares, and (b) the compatible set of observability don't cares for each MV-node. We give a recursive image computation to transform the don't cares into the space of local inputs of the node to be minimized. The methods are applied to some experimental multi-valued networks, and demonstrate reduction in the size of the tables that represent multi-valued logic functions.

We present a VLSI design methodology to address the cross-talk problem, which is becoming increasingly important in Deep Sub-Micron (DSM) IC design. In our approach, we implement the logic netlist in the form of a network of medium sized PLAs. We utilize two regular layout "fabrics" in our methodology, one for areas where PLA logic is implemented, and another for routing regions between such logic blocks. We show that a single PLA implemented in the first fabric style is not only cross-talk immune, but also about 2/spl times/ smaller and faster than a traditional standard cell based implementation of the same logic. The second fabric, utilized in the routing region between individual PLAs, is also highly cross-talk immune. Additionally, in this fabric, power and ground signals are essentially "pre-routed" all over the die. Our synthesis flow involves decomposing the design into a network of PLAs, each of which has a bounded width and height. The number of inputs and outputs of each PLA are flexible as long as the resulting PLA width is bounded. We perform folding of PLAs to achieve better logic density. Routing is performed using 2,3,4,5 and 6 routing layers. State-of-the-art commercial routing tools are utilized for the experiments involving the use of 3,4,5 and 6 routing layers. We have implemented the entire design flow using these ideas. Our scheme results in a reduction in the cross-talk between signal wires of between one and two orders of magnitude. As a result, for a 0.1 /spl mu/m process, the delay variation due to cross-talk dramatically drops from 2.47:1 to 1.02:1. Additionally, our methodology results in circuits that are extremely fast and dense, with a timing improvement of about 15% and an overall area penalty of about 3% compared to standard cells. The regular arrangement of metal conductors in our scheme results in low and highly predictable inductive and capacitive parasitics, resulting in highly predictable designs. The crosstalk immunity, high speed, low area overhead and high predictability of our methodology indicate that it is a strong candidate as the preferred design methodology in the DSM era.

In this paper we present a novel force-directed placement algorithm, which is used to solve macro-cell placement problems. A new wire model replaces the traditional clique model and makes possible early awareness of routing congestion. Issues such as cell orientation, overlap elimination, and pad positioning are also considered. Experiments show satisfactory performance and fast run time.

This paper describes the application of binary and multivalued SPFD-based wire removal techniques for circuit implementations utilizing networks of PLAs. It has been shown that a design style based on a multi-level network of approximately equal-sized PLAs results in a dense, fast, and crosstalk-resistant layout. Wire removal is a technique where the total number of wires between individual circuit nodes is reduced, either by removing wires, or replacing them with other existing wires. Three separate wire removal experiments are performed. Either wire removal is invoked before clustering the original netlist into a network of PLAs, or after clustering, or both before and after clustering. For wire removal before clustering, binary SPFD-based wire removal is used. For wire removal after clustering, multi-valued SPFD-based wire removal is used since the multi-output PLAs can be viewed as multi-valued single output nodes. We demonstrate that these techniques are effective. The most effective approach is to perform wire removal both before and after clustering. Using these techniques, we obtain a reduction in placed and routed circuit area of about 11%. This reduction is significantly higher (about 20%) for the larger circuits we used in our experiments.

We propose the use of the logic S1S as a mathematical framework for studying the synthesis of sequential designs. We will show that this leads to simple and mathematically elegant solutions to problems arising in the synthesis and optimization of synchronous digital hardware. Specifically, we derive a logical expression which yields a single finite state automaton characterizing the set of implementations that can replace a component of a larger design. The power of our approach is demonstrated by the fact that it generalizes immediately to arbitrary interconnection topologies, and to designs containing nondeterminism and fairness. We also describe control aspects of sequential synthesis and relate controller realizability to classical work on program synthesis and tree automata.

We introduce a new technique for solving some discrete optimization problems exactly. The motivation is that when searching the space of solutions by a standard branch-and-bound (B&B) technique, often a good solution is reached quickly and then improved only a few times before the optimum is found: hence, most of the solution space is explored to certify optimality, with no improvement in the cost function. This suggests that more powerful lower bounding would speed up the search dramatically. More radically, it would be desirable to modify the search strategy with the goal of proving that the given subproblem cannot yield a solution better than the current best one (negative thinking), instead of branching further in search for a better solution (positive thinking). For illustration we applied our approach to the unate covering problem. The algorithm starts in the positive-thinking mode by a standard B&B procedure that generates recursively smaller subproblems. If the current subproblem is "deep" enough, the algorithm switches to the negative thinking mode where it tries to prove that solving the subproblem does not improve the solution. The latter is achieved by a new search procedure invoked when the difference between the upper and lower bound is "small". Such a procedure is complete: either it yields a lower bound that matches the current upper bound, or it yields a new solution better than the current one. We implemented our new search procedure on top of ESPRESSO and SCHERZO, two state-of-art covering solvers used for computer-aided design applications, showing that in both cases we obtain new search engines (respectively, AURA and AURA II) much more efficient than the original ones.

We present a logical formalism for expressing properties of continuous-time Markov chains. The semantics for such properties arise as a natural extension of previous work on discrete-time Markov chains to continuous time. The major result is that the verification problem is decidable; this is shown using results in algebraic and transcendental number theory.

We propose a new VLSI layout methodology which addresses the main problems faced in Deep Sub-Micron (DSM) integrated circuit design. Our layout “fabric ” scheme eliminates the conventional no-tion of power and ground routing on the integrated circuit die. In-stead, power and ground are essentially “pre-routed ” all over the die. By a clever arrangement of power/ground and signal pins, we almost completely eliminate the capacitive effects between signal wires. Ad-ditionally, we get a power and ground distribution network with a very low resistance at any point on the die. Another advantage of our scheme is that the arrangement of conductors ensures that on-chip inductances are uniformly negligible. Finally, characterization of the circuit delays, capacitances and resistances becomes extremely simple in our scheme, and needs to be done only once for a design. We show how the uniform parasitics of our fabric give rise to a reliable and predictable design. We have implemented our scheme using public domain layout software. Preliminary results show that it holds much promise as the layout methodology of choice in DSM integrated circuit design. 1

The concept of improving the timing behavior of a circuit by relocating registers is called retiming and was first presented by Leiserson and Saxe.They showed that the problem of determining an equivalent minimum area (total number of registers) circuit is polynomial-time solvable.In this work we show how this approach can be reapplied in the DSM domain when area-delay trade-offs and delay constraints are considered.The main result is that the concavity of the tradeoff function allows for a casting of this DSM problem into a classical minimum area retiming problem whose solution is polynomial time solvable.

Retiming combined with combinational optimization is a powerful sequential synthesis method. However, this methodology has not found wide application because formal sequential verification is not practical and current simulation methodology requires the correspondence of latches disallowing any movement of latches. We present a practical verification technique which permits such sequential synthesis for a class of circuits. In particular, we require certain constraints to be met on the feedback paths of the latches involved in the retiming process. For a general circuit, we can satisfy these constraints by fixing the location of some latches, e.g., by making them observable. We show that equivalence checking after performing repeated retiming and synthesis on this class of circuit reduces to a combinational verification problem. We also demonstrate that our methodology covers a large class of circuits by applying it to a set of benchmarks and industrial designs.

This paper describes a probabilistic approach to state space search. The presented method applies a ranking of the design states according to their probability of reaching a given target state based on a random walk model. This ranking can be used to prioritize an explicit or partial symbolic state exploration to find a trajectory from a set of initial states to a set of target states. A symbolic technique for estimating the reachability probability is described which implements a smooth trade-off between accuracy and computing effort. The presented probabilistic state space search complements incomplete verification methods which are specialized in finding errors in large designs.

A combinational module is a combinational circuit that can be used under any arrival time condition at the primary inputs. An intellectual property (IP) module, if combinational, is one such example. The false-path-aware delay characterization of a combinational module without disclosing its internal structural detail is crucial for accurate timing analysis of IP-based designs. We address three related issues on delay characterization of combinational modules. We first introduce a new notion called timing-safe replaceability as a way of comparing the timing characteristics of two combinational modules formally. This notion allows us to determine whether a new module is a safe replacement of an original module under any surrounding environment with respect to timing. Second, we consider false path detection of combinational modules. Although false path detection is essential in accurate delay modeling, we argue that the conventional definition of false paths such as floating mode analysis is not appropriate for defining the falsity of a path for a combinational module since the falsity is relative to an arrival time condition. A new definition of false paths, termed strongly false paths, is introduced to resolve this issue. Strongly false paths are those paths that are guaranteed to be false under any arrival time condition, and thus uniquely defined independent of arrival time conditions. Finally, we propose a new algorithm that removes strongly false paths from a combinational module by a circuit transformation. We prove that the resulting circuit is a timing-safe replacement of the original.

In many designs a large portion of path delay faults is non-robustly untestable. This paper presents a new low-cost method for identifying non-robustly untestable path delay faults. Using an implication-based procedure, our method starts with a small number of path segments, called maximum fanout-free segments, to quickly locate lines which cannot construct non-robustly testable paths with them. After a large portion of faults is marked as untestable, only a small subset of faults remains for the ATPG procedure, which can effectively alleviate the problem of handling a huge number of path delay faults and reduce test generation time. Experimental results for ISCAS'85 benchmark circuits demonstrate that a significant portion of non-robustly untestable path delay faults was identified efficiently using our method. For most of these circuits, 90%-95% of non-robustly untestable path delay faults can be identified within a small amount of CPU time.

We propose a hierarchical timing analysis technique for combinational circuits under the tightest known sensitization criterion, the XBDO delay model. Given a hierarchical combinational circuit, a generalized delay model of each left module is characterized first. Since this timing characterization step takes into account false paths in each module, the delay model is more accurate than the one obtained by topological analysis. Then topological delay analysis is performed on the circuit composed of generalized gates replacing the leaf modules, where the “gate” delay model is the derived one. As far as the authors know, this is the first result that shows that hierarchical analysis is possible under state-of-the-art tight sensitization criteria. We demonstrate by experimental results that loss of accuracy in using the hierarchical approach is very minimal in practice. The theory developed in this paper also provides a foundation for incremental timing analysis under accurate sensitization criteria.

We propose an algorithm for minimal-delay technology mapping for library-based designs. We show that subject graphs need not be decomposed into trees for delay minimization; they can be mapped directly as DAGs. Experimental results demonstrate that significant delay improvement is possible by this new approach.

A shift is proposed in the design of VLSI circuits. In conventional design, higher levels of synthesis produce a netlist, from which layout synthesis builds a mask specification for manufacturing. Timing analysis is built into a feedback loop to detect timing violations which are then used to update specifications to synthesis. Such iteration is undesirable, and for very high performance designs, infeasible. The problem is likely to become much worse with future generations of technology. To achieve a non-iterative design flow, we propose that early synthesis stages should use “wireplanning” to distribute delays over the functional elements and interconnect, and layout synthesis should use its degrees of freedom to realize those delays. In this paper we attempt to quantify this problem for future technologies and propose some solutions for a “constant delay” methodology.

We present a new combinational verification technique where the functional specification of a circuit under verification is utilized to simplify the verification task. The main idea is to assign to each primary input a general function, called a coordinate function, instead of a single variable function as in most BDD-based techniques. BDDs of intermediate nodes are then constructed based on these coordinate functions in a topological order from primary inputs to primary outputs. Coordinate functions depend on primary input variables and extra variables. Therefore combinational verification is performed not over the set of primary input variables but over the extended set of variables. Coordinate functions are chosen in such a way that in the process of computing intermediate functions the dependency on the primary input variables is gradually replaced with that on the extra variables, thereby making Boolean functions associated with primary outputs simple functions only in terms of the extra variables. We show that such a smart choice of coordinate functions is possible with the help of the high-level functional specification of the circuit.

h this paper, we proWse a new logic synthesis methodology to deal with the increasing imprtance of the interconnect delay in deepsubmicron technologies.We first show that conventional logic synthesis techniques can produce circuits which wi~have long paths even if placed optimally.Then, we charactetie the conditions under which this cm happen and propose logic synthesis techniques which pmduw circuits which are "bettefl for placement.Our proposed approach still separates logic synthesis from physical design.

Retiming and resynthesis transformations can be used for optimizing the area, power, and delay of sequential circuits. Even though this technique has been known for more than a decade, its exact optimization capability has not been formally established. We show that retiming and resynthesis can exactly implement 1-step equivalent state transition graph transformations. This result is the strongest to date. We also show how the notions of retiming and resynthesis can be moderately extended to achieve more powerful state transition graph transformations. Our work will provide theoretical foundation for practical retiming and resynthesis based optimization and verification. 1 Introduction In combinational synthesis [1, 8], the positions of the latches are fixed and the logic is optimized for area, delay, or power. In retiming [5], the latches are moved across combinational gates. Retiming can change the number of latches (and hence the area) and the minimum cycle time (i.e., the clock r...

Yamashita et. al.[1] introduced a new category for ex-pressing the flexibility that a node can have in a multi-level network. Originally presented in the context of FPGA syn-thesis, the paper has wider implications which were discussed in [2]. SPFDs are essentially a set of incompletely specified functions. The increased flexibility that they offer is obtained by allowing both a node to change as well as its immediate fanins. The challenge with SPFDs is (1) to compute them in an efficient way, and (2) to use their increased flexibility in a controlled way to optimize a circuit. In this paper, we provide a complete implementation of SPFDs using BDDs and apply it to the optimization of Boolean networks. Two scenarios are presented, one which trades literals for wires and the other rewires the network by replacing one fanin at a node by a new fanin. Results on benchmark circuits are very favorable. 1

We present a new matrix formulation of the face hypercube embedding problem that motivates the design of an efficient search strategy to find an encoding that satisfies all faces of minimum length. Increasing dimensions of the Boolean space are explored; for a given dimension constraints are satisfied one at a time. The following features help to reduce the nodes of the solution space that must be explored: candidate cubes instead of candidate codes are generated, cubes yielding symmetric solutions are not generated, a smaller sufficient set of solutions (producing basic sections) is explored, necessary conditions help discard unsuitable candidate cubes, early detection that a partial solution cannot be extended to be a global solution prunes infeasible portions of the search tree. We have implemented a prototype package minimum input satisfaction kernel (MINSK) based on the previous ideas and run experiments to evaluate it. The experiments show that MINSK is faster and solves more problems than any available algorithm. Moreover, MINSK is a robust algorithm, while most of the proposed alternatives are not. Besides most problems of the complete Microelectronics Center of North Carolina (MCNC) benchmark suite, other solved examples include an important set of decoder programmable logic arrays (PLA's) coming from the design of microprocessor instruction sets.

This paper addresses how to compute required times at intermediatenodes in a combinational network given required times atprimary outputs. The simplest approach is to compute them basedon topological delay analysis without any consideration of falsepaths. In this paper, however, we take into account false pathsbetween the intermediate nodes and the primary outputs explicitlyto characterize the timing constraints at the nodes more accurately.We show that this approach leads to a technique for computing amore refined and relaxed timing constraint than that obtained bytopological analysis. We generalize the notion of required timesfrom a single constant to a relation where a signal is required atdifferent times depending on the values of the other signals.

We introduce a new technique to solve exactly a discrete optimization problem, based on the paradigm of "negative" thinking. The motivation is that when searching the space of solutions, often a good solution is reached quickly and then improved only a few times before the optimum is found: hence most of the solution space is explored to certify optimality, but it does not yield any improvement of the cost function. So it is quite natural for an algorithm to be "skeptical" about the chance to improve the current best solution. For illustration we have applied our approach to the unate covering problem. We designed a procedure, raiser, implementing a negative thinking search, which is incorporated into a common branch-and-bound procedure. Experiments show that our program, AURA, outperforms both ESPRESSO and our enhancement of ESPRESSO using Coudert's limit lower bound. It is always faster and in the most difficult examples either has a running time better by up to two orders of magnitude, or the other programs fail to finish due to timeout or spaceout. The package SCHERZO is faster on some examples and loses on others, due to a less powerful pruning strategy of the search space, partially mitigated by a more effective computation of the maximal independent set.

We present a new matrix formulation of the face hypercube embedding problem that motivates the design of an efficient search strategy to find an encoding that satisfies all faces of minimum length. Increasing dimensions of the Boolean space are explored; for a given dimension constraints are satisfied one at a time. The following features help to reduce the nodes of the solution space that must be explored: candidate cubes instead of candidate codes are generated, cubes yielding symmetric solutions are not generated, a smaller sufficient set of solutions (producing basic sections) is explored, necessary conditions help discard unsuitable candidate cubes, early detection that a partial solution cannot be extended to be a global solution prunes infeasible portions of the search tree. We have implemented a prototype package MINSK based on the previous ideas and run experiments to evaluate it. The experiments show that MINSK is faster and solves more problems than any available algorithm. Moreover, MINSK is a robust algorithm, while most of the proposed alternatives are not. Besides most problems of the complete MCNC benchmark suite, other solved examples include an important set of decoder PLAs coming from the design of microprocessor instruction sets.

This paper is concerned with approximate delay computation algorithms for combinational circuits. As a result of intensive research in the early 90's efficient tools exist which can analyze circuits of thousands of gates in a few minutes or even in seconds for many cases. However, the computation time of these tools is not so predictable since the internal engine of the analysis is either a SAT solver or a modified ATPG algorithm, both of which are just heuristic algorithms for an NP-complete problem. Although they are highly tuned for CAD applications, there exists a class of problem instances which exhibits the worst-case exponential CPU time behavior. In the context of timing analysis, circuits with a high amount of reconvergence, e.g. C6288 of the ISCAS benchmark suite, are known to be difficult to analyze under sophisticated delay models even with state-of-the-art techniques. To make timing analysis of such corner case circuits feasible we propose an approximate computation scheme to the timing analysis problem as an extension to the exact analysis method proposed previously. Sensitization conditions are conservatively approximated in a selective fashion so that the size of SAT problems solved during analysis is controlled. Experimental results show that the approximation technique is effective in reducing the total analysis time without losing accuracy for the case where the exact approach takes much time or cannot complete.

We propose an algorithm for area optimisation of sequential circuits through redundancy removal. The algorithm finds compatible redundancies by implying values over nets in the circuit. The potentially exponential cost of state space traversal is avoided and the redundancies found can all be removed at once. The optimised circuit is a safe delayed replacement of the original circuit. The algorithm computes a set of compatible sequential redundancies and simplifies the circuit by propagating them through the circuit. We demonstrate the efficacy of the algorithm even for large circuits through experimental results on benchmark circuits.

We address the problem of finite state machine (FSM) traversal, a key step in most sequential verification and synthesis algorithms. We propose the use of partitioned ROBDDs to reduce the memory explosion problem associated with symbolic state space exploration techniques. In our technique, the reachable state set is represented as a partitioned ROBDD (A. Narayan et al., 1996). Different partitions of the Boolean space are allowed to have different variable orderings and only one partition needs to be in memory at any given time. We show the effectiveness of our approach on a set of ISCAS89 benchmark circuits. Our techniques result in a significant reduction in total memory utilization. For a given memory limit, partitioned ROBDD based method can complete traversal for many circuits for which monolithic ROBDDs fail. For circuits where both partitioned ROBDDs as well as monolithic ROBDDs cannot complete traversal, partitioned ROBDDs can reach a significantly larger set of states.

The paper presents an extension to OBDDs with timing information, called timed binary decision diagrams (TBDDs). TBDDs are also canonical and allow the symbolic manipulation of Boolean functions with timing information. A TBDD software package is implemented based on the existing CMU BDD package. Experimental results demonstrate the efficiency of the TBDDs in representing circuits with both functional and timing information.

The breadth-first manipulation technique has proven effective in dealing with very large sized BDDs. However, until now the lack of dynamic variable reordering has remained an obstacle in its acceptance. The goal of the work is to provide efficient techniques to address this issue. After identifying the problems with implementing variable swapping (the core operation in dynamic reordering) in breadth-first based packages, the authors propose techniques to handle the computational and memory overheads. They feel that combining dynamic reordering with the powerful manipulation algorithms of a breadth-first based scheme can significantly enhance the performance of BDD based algorithms. The efficiency of the proposed techniques is demonstrated on a range of examples.

This paper presents an efficient implication-based approach for identifying non-robustly untestable path delay faults. It starts from possible conflicts to find untestable faults by performing static implication. It is neither path-oriented nor space-search based. Experimental results for ISCAS'85 benchmark circuits demonstrate that a significant portion of non-robustly non-robustly untestable path delay faults is identified efficiently. The method can be combined easily with ATPG-based approaches for path delay testing to yield cost effective methods for path delay faults in large circuits.

The computation of sets of compatibles of incompletely specified finite-state machines (ISFSMs) is a key step in sequential synthesis. This paper presents implicit computations to obtain sets of maximal compatibles, compatibles, prime compatibles, implied sets, and class sets. The computations are implemented by means of BDDs that realize the characteristic functions of these sets. We have demonstrated with experiments from a variety of benchmarks that implicit techniques allow us to handle examples exhibiting a number of compatibles up to 2/sup 1500/, an achievement outside the scope of programs based on explicit enumeration. We have shown, in practice, that ISFMSs with a very large number of compatibles may be produced as intermediate steps of logic synthesis algorithms, for instance, in the case of asynchronous synthesis. This shows that the proposed approach not only has a theoretical interest, but also practical relevance for current logic synthesis applications, as shown by its application to ISFSM state minimization.

This paper addresses state minimization problems of different classes of nondeterministic finite-state machines (NDFSMs). We describe a fully implicit algorithm for state minimization of pseudo nondeterministic FSM's (PNDFSMs). The results of our implementation are reported and shown to be superior to a previous explicit formulation. We could solve exactly all but one problem of a published benchmark, while an explicit program could complete approximately one half of the examples, and in those cases, with longer run times. Then we present a theoretical solution to the problem of exact state minimization of general NDFSMs, based on the proposal of generalized compatibles. This gives an algorithmic framework to explore behaviors contained in a general NDFSM.

We survey techniques for solving binate covering problems, an optimization step often occurring in logic synthesis applications. Standard exact solutions are found with a branch-and-bound exhaustive search, made more efficient by bounding away regions of the search space. Standard approaches are said to be explicit because they work on a direct representation of the binate table, usually as a matrix. Recently, covering problems involving large tables have been attacked with implicit techniques. They are based on the representation by reduced-ordered binary decision diagrams of an encoding of the binate table. We show how table reductions, computation of a lower bound, and of a branching column can be performed on the table so represented. We report experiments for two different applications that demonstrate that implicit techniques handle instances beyond the reach of explicit techniques. Various aspects of our original research are presented for the first time, together with a selection of the most important old and new results scattered in many sources.

In this paper, we present a symbolic minimization procedure to obtain optimal two-level implementations of finite-state machines. Encoding based on symbolic minimization consists of optimizing the symbolic representation, and then transforming the optimized symbolic description into a compatible two-valued representation by satisfying encoding constraints (bitwise logic relations) imposed on the binary codes that replace the symbols. Our symbolic minimization procedure captures the sharing of product terms due to ORing effects in the output part of a two-level implementation of the symbolic cover. Face, dominance, and disjunctive constraints are generated. Product terms are accepted in a symbolic minimized cover only when they induce compatible encoding constraints. At the end, a set of codes that satisfy all constraints is computed. The quality of this synthesis procedure is shown by the fact that the cardinality of the cover obtained by symbolic minimization and of the cover obtained by replacing the codes in the initial cover and then minimizing it with ESPRESSO are very close. Experiments show that in some cases, our procedure improves on the best results of state-of-art tools.

personal or class-room use is granted without fee provided that copies are not made or distributed for profit or commercial advantage, the copyright notice, the title of the publication and its date appear, and notice is given that copying is

The success of binary decision diagram (BDD) based algorithms for verification depend on the availability of a high performance package to manipulate very large BDDs. State-of-the-art BDD packages, based on the conventional depth-first technique, limit the size of the BDDs due to a disorderlymemory accesspatterns that results in unacceptably high elapsed time when the BDD size exceeds the main memory capacity. We present a high performance BDD package that enables manipulation of very large BDDs by using an iterative breadth-first technique directed towards localizing the memory accesses to exploit the memory system hierarchy. The new memory-oriented performance features of this package are 1) an architecture independent customized memory management scheme, 2) the ability to issue multiple independent BDD operations (superscalarity) , and 3) the ability to perform multiple BDD operations even when the operands of some BDD operations are the result of some other operations yet to be com...

Retiming is often used to optimize synchronous sequential circuits for area or delay or both. If the latches that are retimed have a hardware reset value, the initial state of the circuit must also be retimed, i.e. an initial state must be derived for the retimed circuit. Previously, it has been suggested that this can be avoided if the hardware reset signals are represented explicitly. However, it was thought that this adds unnecessary area and restricts the space of possible retimings. We demonstrate that this is not the case. In addition, we show that this methodology does not require the restriction that all reset signals be asserted at the beginning of circuit operation-a restriction that was imposed by existing algorithms for determining the retimed initial state. Finally we show how our explicit reset (ER) framework enables us to retime when some latches may be driven by different hardware resets, and some others may not have any hardware resets. We also consider the case where the resets are asynchronous. We expect these solutions to the "retimed initial state" problem to help increase the practical applicability of retiming.

Hardware systems are generally specified as a set of interacting finite state machines (FSMs). An important problem in formal verification using Binary Decision Diagrams (BDDs) is forming the transition relation of the product machine. This problem reduces to conjuncting (or multiplying) the BDDs representing the transition relations of the individual machines, and then existentially quantifying out the set of input and output variables. The resulting graph is called the product graph. Computing the set of reachable states of the product graph is the central verification problem. In this paper, we discuss two related problems. The early quantification problem is the problem of interleaving multiplication of a set of BDDs with the quantification of a set of variables so that the size of the largest BDD encountered is minimized. We show that an abstraction of this problem is NP-complete, and provide heuristic solutions for it. In some cases, the size of the BDD representing the transition relation of the product graph is too large. The partitioned transition relations problem deals with partially combining the BDD's and quantifying as many variables as possible, so that the time for computing the set of reachable states of the product graph is minimized. We offer heuristic solutions to this problem based on our algorithms for early quantification. The algorithms have been implemented and good experimental results have been achieved.

For circuits where there may be latches with no reset line, we show how to replace some of them with combinational logic. All previous work in sequential optimization by latch removal assumes a designated initial state. Without this assumption, the design can power up in any state and earlier techniques are not applicable. We present an algorithm for identifying and replacing redundant latches by combinational logic such that no environment of the design can detect the change. The new design preserves the steady state behavior as well as all initializing sequences of the old design. We report experimental results on benchmark circuits and demonstrate savings in area without adverse impact on delay.

The success of all binary decision diagram (BDD) based synthesis and verification algorithms depend on the ability to efficiently manipulate very large BDDs. We present algorithms for manipulation of very large Binary Decision Diagrams (BDDs) on a network of workstations (NOW). A NOW provides a collection of main memories and disks which can be used effectively to create and manipulate very large BDDs. To make efficient use of memory resources of a Now, while completing execution in a reasonable amount of wall clock time, extension of breadth-first technique is used to manipulate BDDs. BDDs are partitioned such that nodes for a set of consecutive variables are assigned to the same workstation. We present experimental results to demonstrate the capability of such an approach and point towards the potential impact for manipulating very large BDDs.

It is known that wavepipelined circuits offer high performance, because their maximum clock frequencies are limited only by the path delay differences of the circuits, as opposed to the longest path delays. For proper operation, precision in clock frequency is essential. Using a new representation, Timed Boolean Functions, we derive analytical expressions for valid clocking intervals in terms of topological, 2-vector, and single vector delays, both the longest and the shortest. These intervals take into account both circuit functionality and timing characteristics, thus eliminating the pessimism caused by long and short false paths, and include effects of circuit parameters such as delay variations, clock skews, and setup and hold times of flip flops. In addition, we show that these intervals subsume Cotten's lower bound on valid clock period. Further, we study the problem of computing all enact valid clocking intervals and its computational complexity by demonstrating discontinuity and nonmonotonicity of the harmonic number H(/spl tau/) (the number of valid simultaneous data waves allowed) as a function of the clock period /spl tau/. Finally, we propose algorithms to compute the exact valid intervals for a given set of harmonic numbers and demonstrate performance enhancement of balanced circuits from ISCAS benchmarks with gate delay variations.

We present a robust, efficient algorithm for combinational test generation using a reduction to satisfiability (SAT). The algorithm, Test Generation Using Satisfiability (TEGUS), solves a simplified test set characteristic equation using straightforward but powerful greedy heuristics, ordering the variables using depth-first search and selecting a variable from the next unsatisfied clause at each branching point. For difficult faults, the computation of global implications is iterated, which finds more implications than previous approaches and subsumes structural heuristics such as unique sensitization. Without random tests or fault simulation, TEGUS completes on every fault in the ISCAS networks, demonstrating its robustness, and is ten times faster for those networks which have been completed by previous algorithms. Our implementation of TEGUS can be used as a base line for comparing test generation algorithms; we present comparisons with 45 recently published algorithms. TEGUS combines the advantages of the elegant organization of SAT-based algorithms with the efficiency of structural algorithms.

This paper is concerned with logic optimization of multilevel combinational logic circuits. In the light of theoretical work of the past years, where a circuit is modeled by a Boolean network in which each node implements a single-output Boolean function, we address how a concurrent optimization over multiple nodes or components can lead to further optimization compared to conventional minimization techniques. In particular, we provide a procedure for computing maximally compatible sets of permissible relations for multiple nodes. This is a generalization of the classical notion of a compatible set of permissible functions for a single node, where no method is known for correctly computing such a maximal set. We provide a method for computing the set correctly for the general case. Based on this, we develop and implement a procedure for optimizing multiple nodes concurrently. The proposed procedure has been implemented, and we present experimental results.

Retiming has been proposed as an optimization step for sequential circuits represented at the net-list level.Retiming moves the latches across the logic gates and in doing so changes the number of latches and the longest path delay between the latches.In this paper we show by example that retiming a design may lead to differing simulation results when the retimed design replaces the original design.We also show, by example, that retiming may not preserve the testability of a sequential test sequence for a given stuck-at fault as measured by a simulator.We identify the cause of the problem as forward retiming moves across multiple-fanout points in the circuit.The primary contribution of this paper is to show that, while an accurate logic simulation may distinguish the retimed circuit from the original circuit, a conservative three-valued simulator cannot do so.Hence, retiming is a safe operation when used in a design methodology based on conservative three-valued simulation starting each latch with the unknown value.

We present a mathematical framework for analyzing the synthesis of interacting, finite state systems. The logic S1S is used to derive simple, rigorous, and constructive solutions to problems in sequential synthesis. We obtain exact and approximate sets of permissible FSM network behavior, and address the issue of FSM realizability. This approach is also applied to synthesizing systems with fairness and timed systems.

Current approaches to compute and exploit the flexibility of a component in an FSM network are all at the symbolic level. Conventionally, exploitation of this flexibility relies on state minimizers for incompletely specified FSMs (ISFSMs) or pseudo non-deterministic FSMs (PNDFSM's). However, state-of-the art state minimizers cannot handle large ISFSMs or PNDFSMs. In addition, these exploitation techniques are at the symbolic level, not directly at the net-list logic level. We present a general approach to exploit exact or approximate flexibility directly at the net-list logic level, and we demonstrate that many sequential logic optimization techniques can be applied in exploitation. Moreover, we propose a new procedure for input don't care sequences. As a result, both computation and exploitation of input don't care sequences in larger FSM networks can be made efficient and effective. Finally, we give preliminary results on some artificially constructed FSM networks. Preliminary results indicate that our approach can be effective in reducing the size of a component of an FSM network.

This paper addresses state minimization problems of different classes of non-deterministic finite state machines (NDFSMs). We present a theoretical solution to the problem of exact state minimization of general NDFSMs, based on the proposal of generalized compatibles. This gives an algorithmic frame to explore behaviors contained in a general NDFSM. Then we describe a fully implicit algorithm for state minimization of pseudo non-deterministic FSMs (PNDFSMs). The results of our implementation are reported and shown to be superior to a previous explicit formulation. We could solve exactly all but one problem of a published benchmark, while an explicit program could complete approximately one half of the examples, and in those cases with longer run times.

Computing the set of reachable states of a finite state machine, is an important component of many problems in the synthesis and formal verification of digital systems. The process of design is usually iterative, and the designer may modify and recompute information many times, and reachability is called each time the designer modifies the system because current methods for reachability analysis are not incremental. Unfortunately, the representation of the reachable states that is currently used in synthesis and verification, is inherently non updatable (O. Coudert and J.C. Madre, 1990). We solve this problem by presenting alternate ways to represent the reachable set, and incremental algorithms that can update the new representation each time the designer changes the system. The incremental algorithms use the reachable set computed at a previous iteration, and information about the changes to the system to update it, rather than compute the reachable set from the beginning. This results in computational savings, as demonstrated by the results.

Retiming is sometimes used to optimize gate-level sequential designs. This technique allows memory elements to be moved across combinational elements. Unfortunately, retiming may cause the environment of a design to wait for a few additional clock cycles after power-up to guarantee the same behavior as the original design. Leiserson and Saxe [1] presented a bound on this number of clock cycles; in this paper, we tighten this bound. A smaller bound allows the environment of a design to wait for fewer clock cycles. 1 Introduction Retiming, first formulated by Leiserson and Saxe [1] in the context of systolic systems, is a method for moving memory elements or registers (implemented by edge-triggered latches or flip-flops) across combinational logic to achieve a minimum clock period, a minimum area, or a combination of these cost functions. It has earlier been shown [2] that retiming can change the sequential behavior of a design. Given a sequential circuit with some registers, each regi...

The main disadvantage of the path delay fault model is that to achieve 100% testability every path must be tested. Since the number of paths is usually exponential in circuit size, this implies very large test sets for most circuits. Not surprisingly, all known analysis and synthesis techniques for 100% path delay fault testability are computationally infeasible on large circuits. We prove that 100% delay fault testability is not necessary to guarantee the speed of a combinational circuit. There exist path delay faults which can never impact the circuit delay (computed using any correct timing analysis method) unless some other path delay faults also affect it. These are termed robust dependent delay faults and need not be considered in delay fault testing. Necessary and sufficient conditions under which a set of path delay faults is robust dependent are proved; this yields more accurate and increased delay fault coverage estimates than previously used. Next, assuming only the existence of robust delay fault tests for a very small set of paths, we show how the circuit speed (clock period) can be selected such that 100% robust delay fault coverage is achieved. This leads to a quantitative tradeoff between the testing effort (measured by the size of the test set) for a circuit and the verifiability of its performance. Finally, under a bounded delay model, we show that the test set size can be reduced while maintaining the delay fault coverage for the specified circuit speed. Examples and experimental results are given to show the effect of these three techniques on the amount of delay fault testing necessary to guarantee correct operation.>

We propose a novel framework to solve the state assignment problem arising from the signal transition graph (STG) representation of an asynchronous circuit. We first establish a relation between STG's and finite state machines (FSM's). Then we solve the STG state assignment problem by minimizing the number of states in the corresponding FSM and by using a critical race-free state assignment technique. State signal transitions may be added to the original STG. A lower bound on the number of signals necessary to implement the STG is given. Our technique significantly increases the STG applicability as a specification for asynchronous circuits.>

Article Free Access Share on HSIS: a BDD-based environment for formal verification Authors: A. Aziz Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , F. Balarin Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , S.-T. Cheng Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , R. Hojati Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , T. Kam Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , S. C. Krishnan Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , R. K. Ranjan Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , T. R. Shiple Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , V. Singhal Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , S. Tasiran Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , H.-Y. Wang Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , R. K. Brayton Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , A. L. Sangiovanni-Vincentelli Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile Authors Info & Claims DAC '94: Proceedings of the 31st annual Design Automation ConferenceJune 1994 Pages 454–459https://doi.org/10.1145/196244.196467Published:06 June 1994Publication History 39citation325DownloadsMetricsTotal Citations39Total Downloads325Last 12 Months36Last 6 weeks17 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

We address the problem of obtaining good variable orderings for the BDD representation of a system of interacting finite state machines (FSMs).Orderings are derived from the communication structure of the system.Communication complexity arguments are used to prove upper bounds on the size of the BDD for the transition relation of the product machine in terms of the communication graph, and optimal orderings are exhibited for a variety of regular systems.Based on the bounds we formulate algorithms for variable ordering.We perform reached state analysis on a number of standard verification benchmarks to test the effectiveness of our ordering strategy; experimental results demonstrate the efficacy of our approach.The algorithms described in this paper have been implemented in HSIS, a hierarchical synthesis and verification tool currently under development at Berkeley.

Implicit computations of the solution set of optimization problems arising in logic synthesis hold the promise of enlarging the size of instances that can be solved exactly. The state minimization problem for incompletely specified machines is an important step for sequential circuit optimization. The problem is NP-hard. An exact algorithm consists of two steps: generation of sets of compatibles, and solution of a binate covering problem. This paper presents an implicit algorithm for exact state minimization of FSM's. There are various applications of logic synthesis that generate FSM's beyond the reach of state-of-art state minimization tools. Therefore it is of practical importance to revisit exact state minimization of ISFSM's and address the issue of representing implicitly the solution space. In this paper we show how to compute sets of maximal compatibles, compatibles and prime compatibles with implicit techniques and demonstrate that in this way it is possible to handle examples exhibiting a number of compatibles up to 21200, a number outside the scope of programs based on explicit enumeration [13]. We indicate also where such examples arise in practice. Then we address the final step of an implicit exact state minimization procedure, i.e. solving a binate table covering problem [24]. We present the first published algorithm for fully implicit exact binate covering. We report preliminary results of a prototype implementation capable of reducing huge binate tables (up to 106 rows and column)s and of carrying on the branch-and-bound procedure on an implicit representation of the table. Exact solutions to problems beyond the reach of traditional tools are so found

In current research, the minimum cycle times of finite state machines are estimated by computing the delays of the combinational logic in the finite state machines. Even though these methods deal with false paths, they ignore the sequential and periodic nature of minimum cycle times, and hence may give pessimistic results. In this paper, we first prove conditions under which combinational delays are correct upper bounds on minimum cycle times. Then, we present a sequential approach to compute the minimum cycle times of finite state machines, taking into account the effects of gate delay variations, reachable state space, initial states, unrealizable transitions, multiple cycle false paths, and periodicity of the present state vector sequences. We formulate and solve the problem exactly using Timed Boolean Functions, and give an efficient algorithm to solve for upper bounds of minimum cycle times. The exact formulation with Timed Boolean Functions provides a framework for further improvements on existing algorithms to compute the minimum cycle times. We implemented the algorithm and obtained the tightest bounds known on ISCAS benchmarks. From the experiments, we found that for about 20 % of the circuits (not all shown in section 8), combinational delays, e.g. floating, viability, and transition delays, give pessimistic upper bounds for cycle times by as much as 25%. 1

In this paper, we revisit the classical problem of functional decomposition [1, 2] that arises so often in logic synthesis.One basic problem that has remained largely unaddressed to the best of our knowledge is that of decomposing a function such that the resulting sub-functions are simple, i.e., have small numberof cubes or literals.In this paper, we show h o w to solve this problem optimally.W e show that the problem is intimately related to the encoding problem, which is also of fundamental importance in sequential synthesis, especially state-machine synthesis.We formulate the optimum decomposition problem using encoding.In general, an input-output encoding formulation has to be employed.However, for eld-programmable gate array architectures that use look-up tables, the input encoding formulation suces, provided we use minimum-length codes.The last condition is really not a constraint, since each extra code bit means that an extra table has to be used (and that could be expensive).The unused codes are used as don't cares for simplifying the sub-functions.We compare the original implementation of functional decomposition, which ignores the encoding problem, with the new version that uses encoding while doing decomposition.We obtain an average improvement o f o v er 20% on a set of standard benchmarks for look-up table architectures.

A common approach to performance optimization of circuits focuses on re-synthesis to reduce the length of all paths greater than the desired delay .We describe a new delay optimization procedure that optimizes only sensitizable paths greater than .Unlike previous methods that use topological analysis only, this method accounts for both functional and topological interactions in the circuit.Comprehensive experimental results comparing the proposed technique to a state-of-the-art performance optimization procedure are presented for combinational and sequential logic circuits.

We present heuristic algorithms for finding a minimum BDD size cover of an incompletely specified function, assuming the variable ordering is fixed.In some algorithms based on BDDs, incompletely specified functions arise for which any cover of the function will suffice.Choosing a cover that has a small BDD representation may yield significant performance gains.We present a systematic study of this problem, establishing a unified framework for heuristic algorithms, proving optimality in some cases,and presenting experimental results.

Previous attempts to capture the phenomenon of output don't care sequences for a component in an FSM network have been incomplete.We demonstrate that output don't care sequences for a component can be expressed using a set of observability relations given that its state transition function is kept unchanged.Each observability relation is permissible in the sense that any implementation compatible with one of them is feasible.The representation for a set of permissible observability relations is not unique.We provide a method to find a set with the minimum number of permissible relations.We briefly discuss the exploitation of permissible observability relations in state minimization, circuit implementation and signal encoding.We have implemented these methods and present some preliminary results on a few small artificially constructed examples.

We address the problem of compositional minimization of collections of interacting finite state machines that arise in the context of formal verification of hardware designs by language containment. Typically much of the behavior of the system is redundant with respect to a given property being verified, and so the system can be replaced by substantially simpler representations. We show that these redundancies can be captured by computing states that are input-output equivalent in the presence of fairness. Since computing complete equivalences is computationally expensive, we propose a spectrum of approximations which are efficiently computable. Directly minimizing the entire system requires forming the complete product machine, which can be very large, and hence we describe procedures that hierarchically minimize the system with respect to explicit and BDD representations. We present experimental results on some standard verification examples to show that our algorithms allow the product machine to be represented by very small implicit or explicit representations. We conclude with some further directions.>

Several algorithms for gate-level sequential circuit optimization have been reported in the literature. They perform operations similar to those in the more mature multilevel combinational domain while taking relationships across several time periods into account. These techniques are heuristic and their application ad hoc: there is no guarantee of optimality. We present a technique for producing an optimum two-level acyclic sequential circuit. While the circuit restrictions and cost function are limiting, the guarantee of optimality is novel and illuminating. The technique presented herein is useful for optimizing sub-circuits of a multilevel sequential circuit just as two-level combinatorial techniques have been in the combinational domain. Furthermore, the algorithm can be used to detect precisely circuits in which logic sharing across latch boundaries is actually possible- a hitherto unsolved problem.>

The existence of redundant stuck-faults in a logic circuit is potentially detrimental to high-speed operation, especially when there are false paths that are longer than the circuit delay. Keutzer, Malik, and Saldanha (KMS) in IEEE transactions of Computer Aided Design, vol. 10, no. 4, p. 427, April 1991 have proved that redundancy is not necessary to reduce delay by presenting an algorithm that derives an equivalent irredundant circuit from a given redundant circuit, with no increase in delay. The KMS algorithm consists of an iterative loop of timing analysis, gate duplications, and redundancy removal to successively eliminate long false paths. In this paper we resolve the main bottlenecks of the KMS algorithm by providing an efficient single-pass algorithm to simultaneously remove all long false paths from a given circuit. We achieve this by relating a circuit structure property based on path lengths to the testability (redundancy) and delay. The application of this algorithm to a variety of related logic synthesis problems is described.>

Three encoding problems relevant to the synthesis of digital circuits are input, output, and state encoding. Several encoding strategies have been proposed in the past that decompose the encoding problem into a two step process of constraint generation and constraint satisfaction. The latter requires the assignment of binary codes to symbols subject to the satisfaction of constraints on the codes. This paper focuses on the constraint satisfaction problem. We prove that constraint satisfaction is NP-complete. We develop a framework for the satisfaction of both input and output encoding constraints, and describe a polynomial time (in the number of symbols to be encoded) algorithm to check for the existence of a solution for a set of input and output constraints. An exact algorithm to determine the minimum number of encoding bits required to satisfy all the given constraints is provided, and a heuristic algorithm is also described. The application of this framework to a variety of encoding problems with different cost functions is illustrated. Experimental results on standard benchmarks are given for the exact and heuristic algorithms.>

Article A unified approach to language containment and fair CTL model checking Share on Authors: Ramin Hojati View Profile , Thomas R. Shiple View Profile , Robert K. Brayton View Profile , Robert P. Kurshan View Profile Authors Info & Claims DAC '93: Proceedings of the 30th international Design Automation ConferenceJuly 1993 Pages 475–481https://doi.org/10.1145/157485.164985Online:01 July 1993Publication History 7citation260DownloadsMetricsTotal Citations7Total Downloads260Last 12 Months1Last 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 introduce a new circuit delay model, delay by sequences of vectors, which captures the essence of viability and floating delays. Then, we classify delays of circuits according to both the delay models of the gates making up the circuits and the family of inputs to the circuits. In this classification, we give sufficient conditions under which floating delay is the same as delay by sequences of vectors; these sufficient conditions are true for most practical circuits. This implies that the assumption of arbitrary node values used in the floating delay model is not too conservative. Thus, delay by sequences of vectors (hence, viability and floating delays), transition delay, and cycle time delay have coherent definitions under the same framework. Next, we study the problem of computing the exact circuit delays under both bounded and unbounded gate delay models, for some of which only upper bounds are known. By using a new formulation technique, called Timed Boolean Function, we formulate the problem of computing the exact delays as a mixed Boolean linear programming problem for which we give efficient algorithms to compute the exact delays of combinational circuit for transition delay and delay by sequences of vectors. The algorithms consider a subset of paths at one time and only the paths potentially responsible for the delay of a circuit are considered. Moreover, the core computation of the algorithms are composed of two computationally efficient algorithms: linear programming and BDD manipulations. We next compute floating (or viability) delays with the bounded gate delay model and show that delays by sequences of vectors and floating (or viability) delays are invariant under both bounded and unbounded gate delay models. Finally, we address the effect of gate delay lower bounds on delays of circuits. We demonstrate the effectiveness of the method by giving exact delay results for all ISCAS benchmark circuits (except C6188)

The main disadvantage of the path delay fault model is that to achieve 100% testability every path must be tested.Since the number of paths is usually exponential in circuit size, atl known analysis and synthesis techniques for 100% path delay fault testability are infeasible on most circuits.In this paper, we show that 100'%odelay fault testability is not necessary to guarantee the speed of a combinational circuit.There exist path delay faults which can never impact the circuit delay (computed using arty correct timing analysis method) unless some other path delay faults also affect i~hence these delay faults need not be considered in delay fault testing.Next, assuming only the existence of robust delay fault tests for a very small set of paths, we show how the circuit speed can be selected such that 100% robust delay fault coverage is achieved.

Article On computing the transitive closure of a state transition relation Share on Authors: Yusuke Matsunaga View Profile , Patrick C. McGeer View Profile , Robert K. Brayton View Profile Authors Info & Claims DAC '93: Proceedings of the 30th international Design Automation ConferenceJuly 1993 Pages 260–265https://doi.org/10.1145/157485.164884Online:01 July 1993Publication History 26citation439DownloadsMetricsTotal Citations26Total Downloads439Last 12 Months28Last 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

Article Free Access Share on Espresso-signature: a new exact minimizer for logic functions Authors: Patrick McGeer View Profile , Jagesh Sanghavi View Profile , Robert Brayton View Profile , Alberto Sangiovanni Vincentelli View Profile Authors Info & Claims DAC '93: Proceedings of the 30th international Design Automation ConferenceJuly 1993 Pages 618–624https://doi.org/10.1145/157485.165069Online:01 July 1993Publication History 51citation464DownloadsMetricsTotal Citations51Total Downloads464Last 12 Months23Last 6 weeks5 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

We propose a novel method to eliminate dynamic hazards in asynchronous circuits synthesized from the signal transition graph (STG) specifications.We first review a relationship between syntactic constraints such as liveness and complete state coding at the STG level and the hazard properties at the gate level.Using this relationship, we identify the cause of dynamic hazards and rem,ove them by an iterative factoring method.Each factoring entails augmenting the given STG with an internal signal.This method is applicable to botb combinational and sequential circuits, and results in hazard-free multi-level implementations from STG specifications.

Article Sequential synthesis for table look up programmable gate arrays Share on Authors: Rajeev Murgai View Profile , Robert K. Brayton View Profile , Albert Sangiovanni-Vincentelli View Profile Authors Info & Claims DAC '93: Proceedings of the 30th international Design Automation ConferenceJuly 1993 Pages 224–229https://doi.org/10.1145/157485.164681Online:01 July 1993Publication History 13citation184DownloadsMetricsTotal Citations13Total Downloads184Last 12 Months1Last 6 weeks1 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

This paper describes an algorithm for deriving necessa~andsufticient constraints for a multi-phase sequential pipeline to operate at a target clock cycle.Constraints on delays of the pipeline stages are used to drive a combinational logic delay optimizer to resynthesize the pipeline stagesfor improved performance.A main advantage of such an approach is that a global picture of the d~tribution of delays in the circuit is obtained.It also permits safe cycle stealing through level-sensitive latches acrosspipeline stages.

Almost all mapping tools for programmable gate arrays (PGAs) start from a network optimized for the number of literals in the factored form. However, PGA architectures imposed different kinds of constraints on the synthesis process. For example, table look up (TLU) architectures restrict each function to at most m inputs (for a fixed m). This is unlike any type of constraint in PLA or standard-cell synthesis. Thus, standard cost functions like the number of cubes or factored form literals are not necessarily good complexity measures for TLU architectures. Decomposition and block count minimization are two steps in PGA mapping that are applied to an optimized design. In decomposition, a feasible representation of the network is obtained, which can be mapped directly onto the target architecture. Block count minimization then tries to maximally group the functions of the decomposed network into basic blocks such that the total number of blocks used are minimized. We address the problem of modeling the decompositon step, in optimization; in particular, we look at cube-packing, which has proved quite effective for the TLU architectures. We propose a technique for deriving a two-level representation of a logic function which yields better results after cube-packing. The technique rests on the idea of using the support of a set of primes as the basic object is two-level minimization, as opposed to a prime. Experiments indicate an average improvement of 12.5% over standard two-level methods.

Combinational circuits are often embedded in synchronous designs with memory elements at the input and output ports. A performance metric for a circuit is the cycle time of the clock signal. Correct circuit operation requires that all paths have a delay that lies between an upper bound and a lower bound. Traditional approaches in delay optimization for combinational circuits have dealt with methods to decrease the delay of the longest path. We address the issue of satisfying the lower bound constraints. Such a problem also arises in wave pipelining of circuits. We propose to handle short path constraints as a post processing step after traditional delay optimization techniques. There are two issues presented in this paper. We first discuss necessary and sufficient conditions for successful delay insertion without increasing delays of any long paths. In the second part, we present a naive approach to padding delays (greedy heuristic) and an algorithm based on linear programming. We describe an application of the theory to wave pipelining of circuits. Results are presented on a set of benchmark circuits, using two delay models.

We present an approach to compute all input don't care sequences for a component in an FSM network with an arbitrary topology. In a cascade FSM network, Kim and Newborn's (K-N) procedure exactly computes all input don't care sequences for the driven machine. However, for a component in a general FSM network the problem of computing and exploiting input don't care sequences is unsolved. We demonstrate that this problem can be reduced to one for a cascade circuit. This reduction uses the notion of an abstract driving machine. In some cases, the exact computation and exploitation of these sequences may be too expensive. We propose methods to compute subsets of input don't care sequences. We discuss the implementation of these algorithms using implicit methods. We also present approximate methods for managing the complexity of large FSM networks. Finally, we give some preliminary results on small networks.

This paper is concerned with the problem of optimizing systems of interacting sequential circuit components. Specifically, we consider how one can find the set of sequential behaviors that can be implemented at a component while preserving the behavior of the total system. This paper proposes a method for computing and representing the complete set of permissible behaviors. We show that the complete set can be computed and represented by a single non-deterministic finite state machine, called the E-machine. The transition relation of the E-machine is obtained by a fixed point computation. The procedure has been implemented and initial experimental results are given.

We address the problem of determining the "complexity" of Boolean functions where complexity is measured as the minimum number of table look up blocks (TLUs) needed to implement a function. We present three new results. The first shows the exact value of the complexity of the class of (m+1)-input functions in terms of the TLUs with m inputs (m/spl ges/2). The next two derive upper bounds on the complexity, given some information about the representation of the function. One bound needs the number of literals and the number of cubes in a sum-of-products representation, and the other, the number of literals in a factored form. We compare these bounds with the results obtained by a TLU synthesis tool. On average, the factored form bounds are about 20% higher than the synthesized results, and hence are reasonable predictors of the number of TLUs needed. This prediction capability can be employed to quickly estimate, without performing any technology mapping, if a circuit can fit on one chip.>

Synchronous Boolean relations can represent sequential don't-care information in synchronous systems. These relations allow greater flexibility in expressing don't-care information than ordinary Boolean relations. Synchronous relations can be used to specify sequential designs at the finite state machine level as well as at the level of combinational elements and latches. The main objective of this paper is to present a heuristic approach to find a minimal implementation for a given synchronous relation. We also show that the synchronous relation formulation can also be used to find a minimal sum-of-products form which implements a function that is compatible with an arbitrary set of Boolean relations.>

Proposes an objective criterion for determining if, given a specific circuit technology, a gate model is suitable for synthesis and verification. This is based on relating the analog circuit behavior to the digital model behavior using a formal definition of implementation. We illustrate the type of design errors which occur when the criterion is not satisfied, and introduce a gate model designed to satisfy the criterion.>

This paper is concerned with logic optimization of multi-output gates in multi-level combinational logic circuits. We address how a concurrent minimization over multiple gates can lead to further optimization as compared to conventional single-gate minimization techniques. In particular, we provide a procedure for computing a maximally-compatible set of permissible relations for multiple-output gates. We also propose a heuristic for clustering single-output gates into multi-output gates, so that increased concurrent optimization can be obtained.>

Extends the theory of reduced offsets to logic functions with multivalued inputs. The authors show that the use of multivalued reduced offsets provides the same flexibility that is available with the use of the offset. Offset-based minimization of multivalued functions with large offsets often takes long computation time and requires very large memory and sometimes is not possible within reasonable time and memory. Such functions can be minimized effectively using reduced offsets.>

The problem of minimizing the cycle time of a given pipelined circuit is considered. The idea of simultaneous retiming and resynthesis is used to optimize a pipelined circuit to meet a given cycle time. An instance of the pipelined cycle optimization problem is specified by the circuit, a set of input arrival times relative to the clock, a set of required output times relative to the clock, and a given cycle time that it must meet. Given the instance of the pipelined performance optimization problem, the authors construct an instance of a combinational speedup problem. This is specified by a combinational logic circuit, a set of arrival times on the inputs, and a set of required times for the outputs which must be met. A constructive proof that the pipelined problem has a solution if and only if the combinational problem has a solution is given. This result shows that it is enough to consider only the combinational speedup problem, and all known techniques for that can be directly applied to generate a solution for the pipelined problem.>

Retiming is an optimization technique for sequential circuits which consists in modifying the position of latches relative to blocks of combinational logic in order to minimize the maximum propagation delay between latches or to meet a given delay requirement while minimizing the number of latches. If the initial state of the circuit is meaningful, one must compute an equivalent initial state for the retimed circuit after retiming. The authors present a simple linear time algorithm to compute a correct initial state for a retimed circuit that can be used whenever the initial state of the original circuit satisfies a simple condition. If this condition is not originally satisfied, it is shown how it can be automatically enforced by a logic synthesis tool with no need for user intervention.>

An approach to minimization that is based on a state-of-the-art paradigm for the two-level minimization of functions is presented. Some special properties of relations, in contrast to functions, which must be carefully considered in realizing a high-quality procedure for solving the minimization problem are clarified. An efficient heuristic method to find an optimal sum-of-products representation for a multiple-valued relation is proposed and implemented in the program GYOCRO. It uses multiple-valued decision diagrams (MDDs) to represent the characteristic functions for the relations. Experimental results are presented and compared with previous exact and heuristic Boolean relation minimizers to demonstrate the effectiveness of the proposed method.>

We present a new algortthrn for exact two-ievei logzc opttmwatton which radtcally tmproves the Qutne -McCluskey (QM) procedure.The new aigorithm derzves the coverzng problem directly and amplicttly without generat~ng the set of all prtme zmplzcants.It then generates only those prime tmpltcants tnvolved in the covertng problem.We represent a set of primes by the

A method for reducing the complexity of CTL model checking on a system of interacting finite state machines is described. The method consists essentially of reducing each component machine with respect to the property to be verified, and then verifying the property on the composition of the reduced components. The procedure is fully automatic and produces an exact result. The potential of the approach is assessed on real-world examples, and the method is demonstrated on a circuit.>

An analysis of valid clock rates in wavepipelined circuits using a technique called timed Boolean functions is presented. It is shown that the valid intervals for the clock period can be disconnected. Thus, it is insufficient to known only the minimum valid clock period in guaranteeing proper operation of pipelined circuits. Analytic expressions for the valid clock intervals in terms of both topological delay and two-vector longest and shortest delays are provided. Also uncertainties arising from manufacturing are taken into account. Some potential difficulties in computing the exact valid clock intervals are illustrated by demonstrating discontinuity and nonmonotonicity of the harmonic number H( tau ) (the number of valid simultaneous data waves allowed) as a function of the clock period tau .>

For performance-driven synthesis of sequential circuits, the optimal clocking problem is considered, and it is shown that it is reducible to a parametric shortest path problem. Constraints are used that take into account both the short and long paths. The main contributions are efficient graph algorithms to solve the set of constraints necessary for correct clocking.>

A technology-independent delay model is introduced. This model assumes that the technology mapper will attempt modest local restructuring of the network. It models the restructuring by producing a staggered network for each gate based on the arrival times of the fan-in signals. The delay of the network is calculated using the staggered network, and when compared to the delay reported by technology mapping, is found to be accurate and efficiently obtained.>

Properties of the if-then-else directed-acyclic graph (ITE) and its relation to the binary decision diagram (BDD) are investigated. It is shown that, for any given variable ordering, there are fewer exponential ITEs than BDDs, and that, for any function f, the size of its canonical ITE is bounded by 4* the size of its corresponding canonical BDD, i.e. //ITE(f)//>

A description is given of SIS, an interactive tool for synthesis and optimization of sequential circuits. Given a state transition table or a logic-level description of a sequential circuit, SIS produces an optimized net-list in the target technology while preserving the sequential input-output behavior. Many different programs and algorithms have been integrated into SIS, allowing the user to choose among a variety of techniques at each stage of the process. It is built on top of MISII and includes all (combinational) optimization techniques therein as well as many enhancements. SIS serves as both a framework within which various algorithms can be tested and compared and as a tool for automatic synthesis and optimization of sequential circuits.>

Techniques for the optimization of multilevel logic with multiple-valued input variable is presented. The motivation for this is to tackle the input encoding problem in logic synthesis, where binary codes must be found for the different values that a symbolic input variable can take. It is shown how the other multilevel optimization techniques are easily extended with multiple-valued variables. These ideas have been implemented as algorithms in the program MIS-MV. The practical issues involved in the implementation of these ideas are discussed, and results of using MIS-MV for input encoding on benchmark examples presented.>

Three relevant encoding problems are input, output and state encoding.Several algorithms have been proposed for their solutions that decompose the problem into symbolic minimization (yielding a set of constraints) and constraint satisfaction.At least two exact formulations of the input encoding constraint satisfaction problem exist.However, a more important use of encoding is in state assignment of finite state machines where both input and output encoding constraints must be satisfied to obtain the most effective implementations.We develop a framework for the simultaneous satisfaction of input and output encoding constraints.We describe an algorithm, polynomial in the number of symbols to be encoded, to check for the existence of a solution for a set of input and output constraints.We provide an efficient atgorithm that determines the minimum number of encoding bits required to satisfy all the given constraints.We demonstrate how heuristic algorithms can be developed within the framework.Firtatly, we discuss the use of this framework in solving a variety of encoding problems with different cost functions.Some preliminary results on medium sized machines are given for both exact and heuristic algorithms.

The authors introduce a novel method for the acceleration of general logic circuits based on the assumption that the delay of a circuit is its longest sensitizable (non-false) path. Hence, circuits are accelerated not by reducing path length but by making paths false. The method is based on generalizing the transformation used to obtain the bypass adder to automatically, in an area efficient way, reduce the delay of any combinational logic circuit with paths of varying length. The authors prove that a circuit realizing any function can be accelerated in this manner, give a general algorithm, and prove bounds on the size of the gain expected.>

The authors introduce an efficient method for generating the functional forms of path analysis problems. They demonstrate that the resulting function is linear in the size of the circuit. The functions are then tested for satisfiability either using a Boolean network satisfiability algorithm suggested by T. Larrabee (1989) or through the construction of BDDs. The effectiveness of the proposed approach is shown for timing analysis and robust path delay-fault test generation. This method also holds promise for both static and dynamic hazard analysis, and for test generation using all other delay-fault models, tau -irredundant fault models, and stuck-open fault models.>

The authors propose some syntactic and semantic extensions to a graphical specification called the signal transition graph (STG). They allow controlled-choice places to have fanout transitions of input signals and arbitrary Boolean expressions can be used as edge labels. They also allow one STG marking to represent more than one state. These extensions allow for a more natural and compact specification of asynchronous behavior. It is also shown that syntactic constraints on STGs are not sufficient to guarantee hazard-free implementations, and techniques are presented to synthesize hazard-free SOP, (sum of products) implementations under both SIC (single input change) and MIC (multiple input change) conditions. The synthesized circuits are speed-independent. They are hazard-free, independently of the gate delay variations, assuming that the circuit operates in fundamental mode.>

The authors address the problem of clustering a circuit for minimizing its delay, subject to capacity constraints on the clusters. They present an algorithm for combinational circuits and give sufficient conditions under which it is optimum. In addition, they address the problem of minimizing the number of clusters and nodes without increasing the maximum delay found by the algorithm. Finally, they extend the clustering algorithm to minimize the clock cycle of a sequential synchronous circuit.>

The authors address the problem of synthesis for a popular class of programmable gate array architecture-the table look-up architectures. These use lookup table memories to implement logic functions. The authors present improved techniques for minimizing the number of table look up blocks used to implement a combinational circuit. On average, the results obtained on a set of benchmarks are 15-29% better than results obtained by previous approaches.>

The authors address the problem of delay optimization for programmable gate arrays. The main considerations are the number of levels in the circuit and the wiring delay. The authors propose a two-phase approach: the first phase involves delay optimizations during logic synthesis before placement, while the second uses logic resynthesis in the case of a timing-driven placement technique. Results and comparisons on benchmarks are presented.>

The observability relation O(x,z) or the Boolean relation provides a description of all the flexibility one has in implementing a Boolean network N. The authors represent and use this flexibility in a logic synthesis system by adding a single output node to the Boolean network N. The node function for the new node is O(x,z). The newly constructed network N' (called the observability network) has only one output and computes 1 for every input x. It is shown that the observability don't cares (ODCs) for a node y/sub i/ in N' provide the maximum flexibility for implementing y/sub i/ and subsume the flexibility obtained for y/sub i/ in N even with don't cares provided at each output. This gives rise to new methods for computing complete ODCs for N' and hence for N.>

An algorithm for computing local don't cares (in terms of immediate fanin variables) at each intermediate node of a Boolean network is presented. These don't cares can be directly used for the simplification of each node by a two-level minimizer. The simplification is relatively fast and the optimized circuits are 100% testable in most cases. The method is more powerful than previous ones developed for node simplification because it computes almost the full local don't care set at each node using image computation techniques. External don't cares are used effectively and there is no restriction on how these are represented because BDDs (binary decision diagrams) are used to translate them into local don't cares. This algorithm has been implemented in the sequential interactive logic synthesis system (SIS), and experimental results are presented that show the effectiveness of the proposed algorithm on benchmark circuits with and without external don't cares.>

The authors propose a novel technology-independent algorithm to minimize circuit delay. The algorithm works in two steps. The first step performs a partial collapse of the circuit based on a delay-driven clustering. The second step factorizes and simplifies the circuit without increasing the number of levels of logic. The computational cost of the algorithm is dominated by the simplification step. To estimate circuit delay, a state-of-the-art technology mapper is used, incorporating fanout optimization and tree covering for delay minimization. On average over a representative set of benchmarks, a delay reduction of 18% is obtained for an area increase of 11%.>

The authors propose a heuristic procedure for the minimization problem of multiple-valued relations based on a paradigm of the more advanced two-level minimization techniques for regular functions. The goal of the procedure is to find a compatible representation with the minimum number of the product terms. The authors present some special properties associated with relations not found in functions. These properties must be carefully accounted for while implementing a procedure that is effective in achieving high quality results. The authors have implemented these algorithms in a program called GYOCRO, and provide experimental evidence of their effectiveness.>

A scheme for programmable logic array (PLA) decomposition that consists of one level of PLAs followed by a second level of simple two-input logic gates is presented. The propagation delay is therefore the sum of the delay through one level of PLA and one level of two-input gates. Since the delay through a two-input gate is significantly less than that through a PLA, the timing performance of the new scheme is generally superior to those of earlier PLA decomposition schemes. The sizes of the PLAs used depend on the choice of the two-input gates. An algorithm is presented that chooses the functionality of the gates such that the areas of the first-level PLAs are minimized, further improving performance. The new decomposition scheme was developed for the automatic programming of a programmable logic device (PLD) which had basically a three level architecture. The functional unit for such a PLD is described and the application of the algorithm to the programming of these functional units is discussed. Experimental results show that the new scheme significantly reduces the area over the single PLA implementation.>

An algorithm is developed for the retiming of single phase sequential circuits with level sensitive (transparent) latches. A set of constraints that permit retiming and optimal clock cycle computation are also developed. It is shown that a design with edge-triggered latches may be tested for speed-up using transparent latches.>

The problem of rectifying design incorrectness due to specification changes as well as design errors of VLSI circuits is formulated and a basic approach using logic synthesis techniques is presented. An efficient approach is presented for rectifying the functional incorrectness by attaching circuitry exterior to the original design. A necessary and sufficient condition for full rectification of the design is provided. It is shown that the proposed approach always succeeds in the rectification of arbitrary combinational circuits. The situation where rectification arises in a practical design process is briefly reviewed.>

A modified approach to two-level logic minimization is described which obviates the need to compute the offset, yet provides the same global picture available with the offset. This approach is based on a new concept called the reduced offset. It is shown that reduced offsets can be computed without using the offset. This scheme has been implemented in ESPRESSO with an interface to the multilevel minimization environment MIS, where it is used to minimize individual nodes (representing two-level functions with single outputs) in multilevel networks. Such functions usually have very large offsets because of a large number of variables in their don't care sets. The modified approach is up to 8.5 times faster than ESPRESSO on a set of benchmark examples.>

Sequential networks contain combinational logic blocks separated by registers. Application of combinational logic minimization techniques to the separate logic block results in improvement that is restricted by the placement of the registers; information about logical dependencies between blocks separated by registers is not utilized. Temporarily moving all the registers to the periphery of a network provides the combinational logic minimization tools with a global view of the logic. A technique is proposed for optimizing a sequential network by moving the registers to the boundary of the network using an extension of retiming, resynthesizing the combinational logic between the registers using existing logic minimization techniques, and replacing the registers throughout the network using retiming algorithms.>

The approaches to two-level logic minimization can be classified into two groups: those that use tautology for expansion of cubes and those that use the offset. Tautology based schemes are generally slower and often give somewhat inferior results, because of a limited global picture of the way in which the cube can be expanded. If the offset is used, usually the expansion can be done quickly and in a more global way because it is easier to see effective directions of expansion. The problem with this approach is that there are many functions that have a reasonable size onset and don't care set but the offset is unreasonably large. It was recently shown that for the minimization of such Boolean functions, a new approach using reduced offsets, provides the same global picture and can be computed much faster. In this paper we extend reduced offsets to logic functions with multi-valued inputs.

We consider the false path problem on precharge/unate networks, more commonly known as dynamic CMOS networks. We demonstrate that the tight criterion of dynamic sensitization is robust on such networks, though it has been shown to be non-robust on general networks. Tighter bounds may be obtained on the length of the critical path in precharge/unate networks than in general static networks. We derive a dynamic programming procedure to find the longest dynamically sensitizable path in a precharge/unate network.

The problem of combinational logic synthesis is addressed for two interesting and popular classes of programmable gate array architectures: table-look-up and multiplexor-based. The constraints imposed by some of these architectures require new algorithms for minimization of the number of basic blocks of the target architecture, taking into account the wiring resources.

We give an algorithm for computing subsets of observability don't cares at the nodes of a multi-level Boolean network. These subsets are based on an extension of the methods introduced in [4] for computing compatible sets of permissible functions (CSPF's) at the nodes of networks composed of NOR gates. The extensions presented are in four directions; an arbitrary logic function is allowed at any node, the don't cares are expressed in terms of both primary inputs and intermediate variables, a new ordering scheme is used, and maximal CSPF's are computed. These ideas are incorporated in an algorithm designed to take full advantage of the power of two-level minimization in multi-level logic synthesis systems. This has been implemented in MIS-II and we present results that demonstrate the effectiveness of these techniques.

Techniques are presented for the optimization of multi-level logic with multiple-valued input variables. The motivation for this is to tackle the input encoding problem in logic synthesis, where binary codes need to be found for the different values of a symbolic input variable. Multi-level multiple-valued optimization is used to generate constraints that are used to determine the codes. The state assignment problem in sequential logic synthesis can be approximated as an input encoding problem by ignoring the next state field, which is reasonable when the primary output logic, dominates the next state logic. A novel technique is presented for extracting common factors with multiple-valued variables, and it is shown how other multi-level optimization techniques are easily extended with multiple-valued variables. These ideas have been implemented as algorithms in the MIS-MV program. Practical issues are also presented regarding implementation. Experimental results are also given.>

The problem of minimizing the cycle time of a given pipelined circuit is considered. Existing approaches are sub-optimal since they do not consider the possibility of simultaneously resynthesizing the combinational logic and moving the latches using retiming. In the work of S. Malik et al. (Proc. of the Hawaii Inter. Conf. on System Sciences, 1990) the idea of simultaneous retiming and resynthesis was introduced. The authors use the concepts presented in that work to optimize a pipelined circuit to meet a given cycle time. Given an instance of the pipelined performance optimization problem, an instance of a combinational speedup problem is constructed. A constructive proof is given that the pipelined problem has a solution if and only if the combinational problem has a solution. This result is significant since it shows that it is enough to consider only the combinational speedup problem and all known techniques for that domain can be directly applied to generate a solution for the pipelined problem.>

Since redundancy is undesirable in high performance circuits, the authors explore timing optimization procedures to determine whether performance optimization may be achieved without introducing redundancy. They demonstrate the conditions under which timing optimization may introduce single stuck-fault redundancies into a given irredundant circuit and illustrate the difficulties in removing or preventing these redundancies. The authors then resolve the question of whether a testability criterion exists that may be retained or easily maintained as invariant during timing resynthesis.>

An investigation was made of the analogous graph structure for representing and manipulating discrete variable problems. The authors define the multi-valued decision diagram (MDD), analyze its properties (in particular prove a strong canonical form) and provide algorithms for combining and manipulating MDDs. They give a method for mapping an MDD into an equivalent BDD (binary decision diagram) which allows them to provide a highly efficient implementation using the previously developed BDD packages. A direct implementation of the MDD structure has also been carried out, but this initial implementation has not yet been tuned to the same extent as the BDDs to allow a reasonable comparison to be made. The authors have used the mapping to BDDs to provide an initial understanding of the limits on the sizes of real problems that can be executed. The results are encouraging.>

The authors propose a novel method based on transition relations that only requires the ability to compute the BDD (binary decision diagram) for f/sub i/ and outperforms O. Coudert's (1990) algorithm for most examples. The method offers a simple notational framework to express the basic operations used in BDD-based state enumeration algorithms in a unified way and a set of techniques that can speed up range computation dramatically, including a variable ordering heuristic and a method based on transition relations.>

The problem of computing the observability don't-care set (nonobservability) for a node in a Boolean network is considered. This problem is generally intractable. Recurrence relations are given for two easily computed subsets of the fanout don't-care set. It is demonstrated that these are, in fact, subsets, and that other subsets appearing in the literature are subsets of those given by the authors.>

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 set of multivariate Boolean functions over the variables χ1 …, χm is considered as the set of multilinear polynomials with coefficients in [0,1] over the literals {χ1, χ1, …, χm, χm}. We denote this set of polynomials as B[@@@@], and call the set of polynomial operations over them algebraic operations. It is shown that these polynomials, called logic expressions, have a unique algebraic prime factorization. An Ο(n log2 n) algorithm to find this factorization is presented. An improvement to the algorithm is presented which may reduce its average-case complexity to Ο(n).

We consider the elimination of false paths in combinational circuits. We give the single generic algorithm that is used to solve this problem, and demonstrate that it is parameterized by a Boolean function called the sensitization condition. We give two criteria which we argue that a valid sensitization condition must meet, and introduce four conditions that have appeared in the recent literature, of which two meet the criteria and two do not. We then introduce a dynamic programming procedure for the tightest of these conditions, the viability condition, and discuss the integration of all four sensitization conditions in the LLLAMA timing environment. We give results on the IWLS and ISCAS benchmark examples and on carry-bypass adders.

Simplification of a multi-level network is used to perform form transformations on parts of the network to obtain an alternate structure that is optimal with respect to area. A technique for obtaining such an optimal structure involves the use of two-level logic minimization on the components of the multi-level logic network. At each component, the structure of the network is captured by intermediate and fan-out don't care sets, which are utilized in the two-level minimization. However, the generation of all the don't cares yield very large sets for most networks and consequently the complete minimization of the components of the circuits require a very large amount of computer time. In this paper we describe algorithms to reduce the size of the don't care sets, so that only the portions that will be useful in minimization at each component of the circuit are retained. We develop both an exact filter and a heuristic filter that prove to be very effective for a large set of benchmark examples. Results show that our technique achieves the same quality as that obtained by doing complete minimizations at each component of the circuits but in much shorter time. This new approach to simplification of multi-level networks has been incorporated into the MIS (version 2.1) logic synthesis system.

SLIP (system-level interactive partitioning), a framework for algorithms that partition and implement complex VLSI-based systems as a hierarchy of electronic packages, is described. SLIP provides a policy for representing hierarchical systems on the OCT data model as well as an attribute mechanism which is used to annotate the representation and to build models of the system. Modifications to the hierarchy are made with routines which maintain the consistency of both the data representation and the attributes.>

Boolean relations are a generalization of incompletely specified logic functions. The authors give a procedure, similar to the Quine-McCluskey procedure, for finding the global optimum sum-of-product representation for a Boolean relation. This is formulated as a binate covering problem, i.e. as a generalization of the ordinary (unate) covering problem. They give an algorithm for it and review the relation of binate covering to tautology checking. The procedure has been implemented and results are presented.>

An m-function network on n primary inputs as forming an n+m-dimensional space is depicted. In this space there are points that can never occur due to mutual dependencies among the functions. This set has been called the satisfiability don't-care (SDC) set of the network and can be viewed as a function over the extended space. The authors demonstrate a sharp criterion for determining which transformations of the network preserve the SDC, and show that most of the operations of the MIS-II synthesis system preserve the SDC. This has importance for implications which are used in a number of network manipulations. This analysis also clarifies how other operations change the SDC, but in very predictable ways. It is shown that a most of the algebraic and some Boolean operations commonly used in logic synthesis preserve the testability of all but a single node in a network. An interesting example is algebraic division (or resubstitution) of one node into another.>

Two methods for two-level logic minimization tuned to a multilevel network environment are discussed. Each produces results superior to ESPRESSO. The tautology-based method is very simple and can be coded in less than 700 lines of C language using the existing data structures, and some routines in ESPRESSO. The reduced offset modification is somewhat more complicated but gives the best results. This algorithm has been incorporated into MISII. The authors have demonstrated that a simple filter applied to the don't care set in this application can be extremely effective.>

The minimization of Boolean functions is usually aimed at obtaining a minimum sum-of-products representation, measured in terms of the number of product terms produced. In multilevel logic, however, a better objective function is a minimized factored form. Traditionally, logic functions have been factored by using algebraic techniques on a minimized sum-of-products. Algebraic factorization techniques explore only part of the solution space. A technique for factoring based on Boolean operations is presented. This technique often leads to a better factored form for a logic function. The algorithm uses the Boolean operations which are the basis of the two-level minimizer ESPRESSO. The technique has been implemented in the multilevel logic minimization program MIS. Some results of Boolean factorization of individual nodes in multilevel networks are presented and then compared with other factoring methods in MIS.>

XPSim (formerly known as SuperCrystal), a multirate, event-driven circuit simulator suitable for large MOS VLSI circuits, is described. XPSim incorporates both static and dynamic partitioning of the circuit. Each partitioned subcircuit is numerically solved with a new integration method-the exponential function method. The voltage waveforms produced by this method are piecewise exponentials. Currently, XPSim supports up to a third-order explicit method. Preliminary tests indicate that XPSim exhibits a significant speedup over SPICE while retaining similar accuracy and is able to handle large circuits.>

External, intermediate, and fan-out don't care sets have been used to describe information about network structure required to optimize a node of a Boolean network locally. Another method to optimize a network has been called global flow analysis. The authors relate these approaches, generalize global flow to arbitrary Boolean networks, and suggest new algorithms for these problems.>

A methodology in which it is not necessary to compute the entire offset is presented, that still provides a global picture. This scheme has been implemented in ESPRESSO with an interface to the multilevel minimization environment MIS. Initial results show that for functions for which the ratio of the size of the cover to the size of the don't care set is small, the new approach is much faster. The initial interest was to use this mainly in a multilevel logic synthesis system where the desired don't care sets are typically large. Some results in this environment are given, and the new scheme is compared with ESPRESSO.>

The results of a formal logic verification system implemented as part of the multilevel logic synthesis system MIS are discussed. Combinational logic verification involves checking two networks for functional equivalence. Techniques that flatten networks or use cube enumeration and simulation cannot be used with functions that have very large cube covers. Binary decision diagrams (BDDs) are canonical representations for Boolean functions and offer a technique for formal logic verification. However, the size of BDDs is sensitive to the variable ordering. Ordering strategies based on the network topology are considered. Using these strategies with BDDs, it has been possible to carry out formal verification for a larger set of networks than with existing verification systems. The present method proved significantly faster on the benchmark set of examples tested.>

An algorithm for speeding up combinational logic with minimal area increase is presented. A static timing analyzer is used to identify the critical paths. Then a weighted min-cut algorithm is used to determine the subset of nodes to be resynthesized. This subset is selected so that the speedup is achieved with minimal area increase. Resynthesis is done by selectively collapsing the logic along the critical paths and then decomposing the collapsed nodes to minimize the critical delay. This process is iterated until either the timing requirements are satisfied or no further improvement can be made. The algorithm has been implemented and tested on many design examples with promising results.>

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.>

MIS is both an interactive and a batch-oriented multilevel logic synthesis and minimization system. MIS starts from the combinational logic extracted, typically, from a high-level description of a macrocell. It produces a multilevel set of optimized logic equations preserving the input-output behavior. The system includes both fast and slower (but more optimal) versions of algorithms for minimizing the area, and global timing optimization algorithms to meet system-level timing constraints. This paper provides an overview of the system and a description of the algorithms used. Included are some examples illustrating an input language used for specifying logic and don't-cares. Parts on an industrial chip have been re-synthesized using MIS with favorable results as compared to equivalent manual designs.

In the above paper, a misprint in a figure made a critical example incomprehensible.

Computer-Aided synthesis of sequential functions of VLSI systems, such as microprocessor control units, must include design optimization procedures to yield area-effective circuits. We model sequential functions as deterministic synchronous Finite State Machines (FSM's), and we consider a regular and structured implementation by means of Programmable Logic Arrays (PLA's) and feedback registers. State assignment, i.e., binary encoding of the internal states of the finite state machine, affects substantially the silicon area taken by such an implementation. Several state assignment techniques have been proposed in the past. However, to the best of our knowledge, no Computer-Aided Design tool is in use today for an efficient encoding of control logic. We propose an algorithm for optimal state assignment. Optimal state assignment is based on an innovative strategy: logic minimization of the combinational component of the finite state machine is applied before state encoding. Logic minimization is performed on a symbolic (code independent) description of the finite state machine. The minimal symbolic representation defines the constraints of a new encoding problem, whose solutions are the state assignments that allow the implementation of the PLA with at most as many product-terms as the cardinality of the minimal symbolic representation. In this class, an optimal encoding is one of minimal length satisfying these constraints. A heuristic algorithm constructs a solution to the constrained encoding problem. The algorithm has been coded in a computer program, KISS, and tested on several examples of finite state machines. Experimental results have shown that the method is an effective tool for designing finite state machines.

The purpose of the present study is to determine for the balanced-pair tunnel-diode circuit the minimum amount of control required when specified parameter imbalances are present in the system. The problem is formulated and the minimum control is determined numerically. These results are compared with an analytic formula for the minimum control which is presented here but is derived in another paper. The results obtained may be used to determine allowable tolerances on the circuit components for a given requirement on the maximum amplification or the total number of input and output connections.