Dependency Quantified Boolean Formulas (DQBF) generalize QBF by explicitly specifying which universal variables each existential variable depends on, instead of relying on a linear quantifier order. The satisfiability problem of DQBF is NEXP-complete, and many hard problems can be succinctly encoded as DQBF. Recent work has revealed a strong analogy between DQBF and SAT: k-DQBF (with k existential variables) is a succinct form of k-SAT, and satisfiability is NEXP-complete for 3-DQBF but PSPACE-complete for 2-DQBF, mirroring the complexity gap between 3-SAT (NP-complete) and 2-SAT (NL-complete). Motivated by this analogy, we study the model counting problem for DQBF, denoted #DQBF. Our main theoretical result is that #2-DQBF is #EXP-complete, where #EXP is the exponential-time analogue of #P. This parallels Valiant's classical theorem stating that #2-SAT is #P-complete. As a direct application, we show that first-order model counting (FOMC) remains #EXP-complete even when restricted to a PSPACE-decidable fragment of first-order logic and domain size two. Building on recent successes in reducing 2-DQBF satisfiability to symbolic model checking, we develop a dedicated 2-DQBF model counter. Using a diverse set of crafted instances, we experimentally evaluated it against a baseline that expands 2-DQBF formulas into propositional formulas and applies propositional model counting. While the baseline worked well when each existential variable depends on few variables, our implementation scaled significantly better to larger dependency sets.

Engineering Change Order (ECO) is the task of finding the non-intrusive design implementation updates to comply with a specification revision. This paper states the rectification problem in quantified Boolean logic that gives sound and complete capture of the update choices for an ECO. Its closed-form statement offers an analytical search for small patches that maximize logic sharing in the implementation. With the abstraction-refinement paradigm assisted by relevance classification, we effectively generalize the sampled knowledge of a revision, enabling the identification of compact updates without undue computational costs. Our experimental evaluation demonstrates almost twice as few gates in synthesized patches compared to the reported state-of-the-art results.

Stochastic Satisfiability Modulo Theories (SSMT) has traditionally focused on the interplay between existential and randomized quantifiers, typically relying on numerical sampling or approximations. We present a generalized SSMT framework that integrates universal quantification, lifting the formalism to a robust stochastic game-theoretic setting. By treating universal quantifiers as the adversarial infimum of satisfaction probabilities, our framework enables the exact modeling of competitive interactions under uncertainty. Our approach leverages Cylindrical Algebraic Decomposition (CAD) to derive exact symbolic probability expressions for Nonlinear Real Arithmetic (NRA) formulas, moving beyond the limitations of linear constraints and point-value estimations. Central to our contribution is a recursive quantifier elimination algorithm designed to handle variable-dependent domains and non-algebraic expressions through a variable reparameterization technique. Experimental evaluation across baseline synthetic formulas, strategic economic models, and probabilistic program verification benchmarks demonstrates that our framework consistently computes exact symbolic solutions. By achieving a degree of symbolic precision and expressiveness unattainable by traditional numerical solvers, this work establishes a new baseline for exact reasoning in stochastic adversarial environments.

The satisfiability (SAT) problem of higher-order quantified Boolean formula (HOQBF) emerged as a natural generalization of SAT, quantified SAT, and second-order quantified SAT. It allows succinct encoding of k-EXPTIME problems beyond the reach of prior Boolean satisfiability formulations, but its application was hampered by the lack of solvers. In this paper, we present the first HOQBF solver that leverages techniques from the model-checking community. Our HOQBF solver is based on reduction to higher-order model checking, which is a generalization from model checking of while-programs to that of higher-order functional programs. The ability of a higher-order model checker to deal with higher-order functions in a program is used to reason about higher-order quantifiers in HOQBF.

When traditional logic synthesis algorithms reach saturation, yet the demand for improved synthesis quality remains high, research focus shifts toward identifying synergistic synthesis algorithms and efficient deployment strategies. This paper proposes a novel rewiring method that can substantially restructure a circuit using truth tables, though it does not scale beyond 16 inputs. To address this limitation, the method is integrated with a new concurrent resynthesis framework that partitions the circuit into support-limited subcircuits, enabling the application of rewiring at scale. Experimental results demonstrate the effectiveness of the proposed approach in minimizing various cost functions, including node count, transistor count, and area after standard-cell mapping, achieving substantial improvements over strong baselines.

Technology mapping is an essential step bridging logic synthesis and physical design in the electronic design automation (EDA) flow. However, technology mapping algorithms often assume a simplified delay model and may not faithfully optimize the circuit under a realistic cost function involving area, delay, and power objectives. In this work, we introduce GradMap, a gradient-descent-based technology mapping framework that integrates a differentiable static timing analysis (STA) engine with a linear delay model for accurate delay estimation. Additionally, it enables simultaneous buffer insertion and gate sizing during technology mapping, providing a holistic optimization solution. Experimental results show that the new method achieves an average improvement of 7% in area-driven optimization, 33% in delay-driven optimization, and 25% in area-delay-product optimization compared to the ABC technology mapper. We note that although the gradient-descent method has significant runtime overhead compared to the highly efficient ABC mapper, it is highly parallelizable with GPU acceleration (in a way similar to the neural network training process), besides attaining high optimization quality far beyond ABC’s ability.

Abstract , originally developed as the first exact quantum circuit simulator, is extended in this paper to provide capabilities for the analysis and verification of quantum states. It provides an interface for users to specify interested quantum states for querying the exact probability or expectation value of a user-defined property. Case studies on three quantum algorithms show the unique capability of benefiting exact quantum circuit analysis and verification, beyond the support by other tools.

Stochastic Boolean satisfiability (SSAT) is a natural formalism for optimization under uncertainty. Its decision version implicitly imposes a final threshold quantification on an SSAT formula. However, the single threshold quantification restricts the expressive power of SSAT. In this work, we enrich SSAT with an additional threshold quantifier, resulting in a new formalism SSAT(θ). The increased expressiveness allows SSAT(θ), which remains in the PSPACE complexity class, to subsume and encode the languages in the counting hierarchy. An SSAT(θ) solver, ClauSSat(θ), is developed. Experiments show the applicability of the solver in uniquely solving complex SSAT(θ) instances of parameter synthesis and SSAT extension.

Boolean matching is an important problem in logic synthesis and verification. Despite being well-studied for conventional Boolean circuits, its treatment for reversible logic circuits remains largely, if not completely, missing. This work provides the first such study. Given two (black-box) reversible logic circuits that are promised to be matchable, we check their equivalences under various input/output negation and permutation conditions subject to the availability/unavailability of their inverse circuits. Notably, among other results, we show that the equivalence up to input negation and permutation is solvable in quantum polynomial time, while its classical complexity is exponential. This result is arguably the first demonstration of quantum exponential speedup in solving design automation problems. Also, as a negative result, we show that the equivalence up to both input and output negations is not solvable in quantum polynomial time unless UNIQUE-SAT is, which is unlikely. This work paves the theoretical foundation of Boolean matching reversible circuits for potential applications, e.g., in quantum circuit synthesis.

Quantum circuit simulation is the basic tool for reasoning over quantum programs. Despite the tremendous advance in the simulator technology in the recent years, the performance of simulators is still unsatisfactory on non-trivial circuits, which slows down the development of new quantum systems. In this work, we develop a loop summarizing simulator based on multi-terminal binary decision diagrams (MTBDDs) with efficiently customized quantum gate operations. The simulator is capable of automatic loop summarization using symbolic execution, which saves repetitive computation for circuits with iterative structures. Experimental results show the simulator outperforms state-of-the-art simulators on some standard circuits, such as Grover's algorithm, by several orders of magnitude.

Qubit mapping is crucial in optimizing the performance of quantum algorithms for physical executions on quantum computing architectures. Many qubit mapping algorithms have been proposed for superconducting systems recently. However, due to their limitations on the physical qubit connectivity, costly SWAP gates are often required to swap logical qubits for proper quantum operations. Trapped-ion systems have emerged as an alternative quantum computing architecture and have gained much recent attention due to their relatively long coherence time, high-fidelity gates, and good scalability for multi-qubit coupling. However, the qubit mapping of the new trapped-ion systems remains a relatively untouched research problem. This paper proposes a new coupling constraint graph with multi-pin nets to model the unique constraints and connectivity patterns in one-dimensional trapped-ion systems. To minimize the time steps for quantum circuit execution satisfying the coupling constraints for trapped-ion systems, we devise a divide-and-conquer solution using Satisfiability Modulo Theories for efficient qubit mapping on trapped-ion quantum computing architectures. Experimental results demonstrate the superiority of our approach in scalability and effectiveness compared to the previous work.

Dependency stochastic Boolean satisfiability (DSSAT) generalizes stochastic Boolean satisfiability (SSAT) in existential variables being Henkinized allowing their dependencies on randomized variables to be explicitly specified. It allows NEXPTIME problems of reasoning under uncertainty and partial information to be compactly encoded. To date, no decision procedure has been implemented for solving DSSAT formulas. This work provides the first such tool by converting DSSAT into SSAT with dependency elimination, similar to converting dependency quantified Boolean formula (DQBF) to quantified Boolean formula (QBF). Moreover, we extend (D)QBF preprocessing techniques and implement the first standalone (D)SSAT preprocessor. Experimental results show that solving DSSAT via dependency elimination is highly applicable and that existing SSAT solvers may benefit from preprocessing.

Stochastic Boolean satisfiability (SSAT) is a formalism allowing decision-making for optimization under quantitative constraints. Although SSAT solvers are under active development, existing solvers do not provide Skolem-function witnesses, which are crucial for practical applications. In this work, we develop a new witness-generating SSAT solver, SharpSSAT, which integrates techniques, including component caching, clause learning, and pure literal detection. It can generate a set of Skolem functions witnessing the attained satisfying probability of a given SSAT formula. We also equip the solver ClauSSat with witness generation capability for comparison. Experimental results show that SharpSSAT outperforms current state-of-the-art solvers and can effectively generate compact Skolem-function witnesses. The new witness-generating solver may broaden the applicability of SSAT to practical applications.

Second-order quantified Boolean formulas (SOQBFs) generalize quantified Boolean formulas (QBFs) by admitting second-order quantifiers on function variables in addition to first-order quantifiers on atomic variables. Recent endeavors establish that the complexity of SOQBF satisfiability corresponds to the exponential-time hierarchy (EXPH), similar to that of QBF satisfiability corresponding to the polynomial-time hierarchy (PH). This fact reveals the succinct expression power of SOQBFs in encoding decision problems not efficiently doable by QBFs. In this paper, we investigate the second-order quantified Boolean logic with the following main results: First, we present a procedure of quantifier elimination converting SOQBFs to QBFs and a game interpretation of SOQBF semantics. Second, we devise a sound and complete refutation-proof system for SOQBF. Third, we develop an algorithm for countermodel extraction from a refutation proof. Finally, we show potential applications of SOQBFs in system design and multi-agent planning. With these advances, we anticipate practical tools for development.

Exclusive-OR Sum-of-Products expressions (ESOPs) are vital for circuit synthesis of arithmetic functions and emerging technologies. The state-of-the-art ESOP extraction methods are limited in their inefficient exhaustive exploration strategy, significant optimality loss in the divide-and-conquer process, and incapability of handling don’t-cares. This work overcomes these limitations by reduced decomposition exploration with a cost estimation and refinement strategy, generally applicable to incompletely specified functions. Experiments show up to 29× (average 12×) runtime and 28× (average 13×) memory-usage improvements with a quality close to the exact optimum obtained by exhaustive exploration for completely-specified functions, and substantial ESOP simplification with don’t-cares for incompletely-specified functions.

Extracting word-level functions from gate-level circuits is challenging and crucial in security, synthesis, and verification applications. State-of-the-art approaches identify subcircuits to match against a predefined library of components. However, they fail for highly-optimized arithmetic circuits due to the absence of intermediate word structures and the high complexity of verifying arithmetic functions. The challenge of learning arithmetic operations from gate-level netlists is posed in the 2022 ICCAD CAD Contest. This work tackles the challenge by devising and combining algebraic, statistical, and structural techniques into an operational flow for function extraction and simplification. Beyond the contest setting, our method also deals with circuits without their input-and output-pin information. Experiments on the contest benchmarks show that our method outperforms the winning teams in the contest in both the number of solved cases and the compactness of the extracted word-level expressions. Moreover, our method can effectively extract most word-level functions within 10 minutes.

Circuit learning has gained significant attention due to machine learning advancements and approximate synthesis applications. The task is to learn a circuit to model an unknown Boolean function subject to different design constraints. When circuit size is hard constrained, decision-tree-based learning plays a crucial role in state-of-the-art methods. However, it can be ineffective due to its structural restriction. This work proposes graph learning to overcome the limitation, provide tradeoffs between circuit size and accuracy, and enrich the portfolio of circuit learning tools. Experimental results show the superiority of our approach to prior work in accuracy, training time, and circuit size.

Hardware acceleration enables neural network (NN) inferencing on edge devices and for high throughput applications. Most approaches use neural processing elements for computation while storing weights in memory blocks. To avoid costly memory access, recent efforts seek direct logic implementation with weights hardwired into the circuit. However, special training strategies are often needed, and they could not maintain accuracy. In contrast, we take a trained and quantized NN as input and synthesize it by Booth encoding and logic sharing, resulting in a hardware accelerator without degrading accuracy. Experiments demonstrate that our method outperforms existing work in area reduction and/or throughput and power efficiency.

Quantum circuit verification is essential, ensuring that quantum program compilation yields a sequence of primitive unitary operators executable correctly and reliably on a quantum processor. Most prior quantum circuit equivalence checking methods rely on edge-weighted decision diagrams and suffer from scalability and verification accuracy issues. This work overcomes these issues by extending a recent BDD-based algebraic representation of state vectors to support unitary operator manipulation. Experimental results demonstrate the superiority of the new method in scalability and exactness in contrast to the inexactness of prior approaches. Also, our method is much more robust in verifying dissimilar circuits than previous work.

Language equations are a powerful tool for compositional synthesis, modeled as the unknown component problem. Given a (sequential) system specification S and a fixed component F, we are asked to synthesize an unknown component X such that whose composition with F fulfills S. The synthesis of X can be formulated with language equation solving. Although prior work exploits partitioned representation for effective finite automata manipulation, it remains challenging to solve language equations involving a large number of states. In this work, we propose variants of Boolean automata as the underlying succinct representation for regular languages. They admit logic circuit manipulation and extend the scalability for solving language equations. Experimental results demonstrate the superiority of our method to the state-of-the-art in solving nine more cases out of the 36 studied benchmarks and achieving an average of 740× speedup.

Statistical inference is a powerful technique in various applications. Although many statistical inference tools are available, answering inference queries involving complex quantification structures remains challenging. Recently, solvers for Stochastic Boolean Satisfiability (SSAT), a powerful formalism allowing concise encodings of PSPACE decision problems under uncertainty, are under active development and applied in more and more applications. In this work, we exploit SSAT solvers for the inference of Probabilistic Graphical Models (PGMs), an essential representation for probabilistic reasoning. Specifically, we develop encoding methods to systematically convert PGM inference problems into SSAT formulas for effective solving. Experimental results demonstrate that, by using our encoding, SSAT-based solving can complement existing PGM tools, especially in answering complex queries.

Homing sequence derivation for nondeterministic finite state machines (NFSMs) has important applications in software/hardware system testing and verification. Unlike prior methods based on explicit tree-based search, in this article we formulate the derivation of a preset/adaptive homing sequence in terms of quantified Boolean formula (QBF) solving. This formulation exploits compact circuit representation of NFSMs and QBF encoding of the existence condition of homing sequence for effective computation. The implicit circuit representation effectively avoids explicit state enumeration, and can be more scalable. Different encoding schemes and QBF solvers are evaluated for their suitability for the homing sequence derivation. Experiments on various computation methods and benchmarks show the generality and feasibility of a proposed approach.

Neural networks (NNs) are key to deep learning systems. Their efficient hardware implementation is crucial to applications at the edge. Binarized NNs (BNNs), where the weights and output of a neuron are of binary values {−1,+1} (or encoded in {0, 1}), have been proposed. As no multiplier required, BNNs are particularly attractive and suitable for hardware realization. Most prior NN synthesis methods target on hardware architectures with neural processing elements (NPEs), where the weights of a neuron are loaded and the output of the neuron is computed. The load-and-compute method, though area efficient, requires expensive memory access, which deteriorates energy and performance efficiency. In this work we aim at synthesizing BNN layers into dedicated logic circuits. We formulate the corresponding model pruning problem and matrix covering problem to reduce the area and routing cost of BNNs. For model pruning, we propose and compare three strategies at the BNN training stage. For matrix covering, we propose a scalable logic-sharing algorithm. By combining these two methods, experimental results justify the effectiveness of the method in terms of area and net savings on FPGA implementation. Our method provides an alternative implementation of BNNs, and can be applied in combination with NPE-based implementation for area, speed, and power tradeoffs.

Stochastic Boolean Satisfiability (SSAT) is a powerful representation for the concise encoding of quantified decision problems with uncertainty. While it shares commonalities with quantified Boolean formula (QBF) satisfiability and has the same PSPACE-complete complexity, SSAT solving tends to be more challenging as it involves expensive model counting, a.k.a. Sharp-SAT. To date, SSAT solvers, especially those imposing no restrictions on quantification levels, remain much lacking. In this paper, we present a new SSAT solver based on the framework of clause selection and cube distribution previously proposed for QBF solving. With model counting integrated and learning techniques strengthened, our solver is general and effective. Experimental results demonstrate the overall superiority of the proposed algorithm in both solving performance and memory usage compared to the state-of-the-art solvers on a number of benchmark formulas.

Stochastic Boolean Satisfiability (SSAT) is a logical formalism to model decision problems with uncertainty, such as Partially Observable Markov Decision Process (POMDP) for verification of probabilistic systems. SSAT, however, is limited by its descriptive power within the PSPACE complexity class. More complex problems, such as the NEXPTIME-complete Decentralized POMDP (Dec-POMDP), cannot be succinctly encoded with SSAT. To provide a logical formalism of such problems, we generalize the Dependency Quantified Boolean Formula (DQBF), a representative problem in the NEXPTIME-complete class, to its stochastic variant, named Dependency SSAT (DSSAT), and show that DSSAT is also NEXPTIME-complete. We demonstrate the potential applications of DSSAT to circuit synthesis of probabilistic and approximate design. Furthermore, to study the descriptive power of DSSAT, we establish a polynomial-time reduction from Dec-POMDP to DSSAT. With the theoretical foundations paved in this work, we hope to encourage the development of DSSAT solvers for potential broad applications.

Recent advancements in quantum technologies shed light on viable quantum computation in near future. Quantum circuit simulation plays a key role in the toolchain of quantum hardware and software development. Due to the enormous Hilbert space of quantum states, simulating quantum circuits with classical computers is notoriously challenging. This work enhances quantum circuit simulation in two dimensions: accuracy (by representing complex numbers algebraically) and scalability (by bit-slicing number representation and achieving matrix-vector multiplication with symbolic Boolean manipulation). Experiments demonstrate the superiority of our method to the state-of-the-art tools over various quantum circuits with up to tens of thousands of qubits.

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.

Logic synthesis is a fundamental step in hardware design whose goal is to find structural representations of Boolean functions while minimizing delay and area. If the function is completely-specified, the implementation accurately represents the function. If the function is incompletely-specified, the implementation has to be true only on the care set. While most of the algorithms in logic synthesis rely on SAT and Boolean methods to exactly implement the care set, we investigate learning in logic synthesis, attempting to trade exactness for generalization. This work is directly related to machine learning where the care set is the training set and the implementation is expected to generalize on a validation set. We present learning incompletely-specified functions based on the results of a competition conducted at IWLS 2020. The goal of the competition was to implement 100 functions given by a set of care minterms for training, while testing the implementation using a set of validation minterms sampled from the same function. We make this benchmark suite available and offer a detailed comparative analysis of the different approaches to learning.

The X-value arises in various contexts of system design. It often represents an unknown value or a don't-care value depending on the application. Verification of X-valued circuits is a crucial task but relatively unaddressed. The challenge of equivalence checking for X-valued circuits, named compatible equivalence checking, is posed in the 2020 ICCAD CAD Contest. In this paper, we present our winning method based on X-value preserving dual-rail encoding and incremental identification of compatible equivalence relation. Experimental results demonstrate the effectiveness of the proposed techniques and the outperformance of our approach in solving more cases than the commercial tool and the other teams among the top 3 of the contest.

In recent years SAT solving has been widely used to implement various circuit transformations in logic synthesis. However, off-the-shelf CNF-based SAT solvers often have suboptimal performance on these challenging optimization problems. This paper describes an application-specific circuit-based SAT solver for logic synthesis. The solver is based on Glucose, a state-of-the-art CNF-based solver and adds a number of novel features, which make it run faster on multiple incremental SAT problems arising in redundancy removal and logic restructuring among others. In particular, the circuit structure of the problem instance is leveraged in a new way to guide variable decisions and to converge to a solution faster for both satisfiable and unsatisfiable instances. Experimental results indicate that the proposed solver leads to a 2-4x speedup, compared to the original Glucose.

Threshold logic (TL) circuits gain increasing attention due to their feasible realization with emerging technologies and strong bind to neural network applications. In this work, we devise techniques for automatic synthesis and verification of TL circuits based on constraint solving. For synthesis, we formulate a fundamental operation to collapse TL functions, and derive a necessary and sufficient condition of collapsibility for linear combination of two TL functions. An approach based on solving the subset sum problem is proposed for fast circuit transformation. For verification, we propose a procedure to convert a TL function to a multiplexer (MUX) tree and to pseudo-Boolean (PB) constraints for formal Boolean and PB reasoning, respectively. Experiments on synthesis show that the collapse operation further reduces gate counts of synthesized TL circuits by an average of 18%. Experiments on verification demonstrate good scalability of the MUX-based method for equivalence checking of synthesized TL circuits, and efficiency of PB constraint conversion in cases where the conjunctive normal form (CNF) formula conversion and MUX tree conversion suffer from memory explosion.

In modern integrated circuit design, bus routing is a challenge because of complex design rules and wiring constraints. Despite extensive research, state-of-the-art in bus routing is not effective when nonuniform tracks, various obstacles, wire width constraints, and multiple spacing rules should be handled simultaneously. A new bus routing framework proposed in this article is based on maze routing and Boolean satisfiability. It produces high-quality results quickly and allows for additional optimizations, such as minimizing wire length on the critical paths. A number of challenging bus routing benchmarks appeared in 2018 ICCAD Contest. Experiments on these benchmarks not only show that the framework is faster than the winners of the competition and previous work but also produces better results, improving the overall cost by 12% while at the same time minimizing the number of spacing violations.

Logic regression aims to find a Boolean model involving binary covariates that predicts the response of an unknown system. It has many important applications, e.g., in data analysis and system design. In the 2019 ICCAD CAD Contest, the challenge of learning a compact circuit representing a black-box input-output pattern generator in a high dimensional Boolean space is formulated as the logic regression problem. This paper presents our winning approach to the problem based on a decision-tree reasoning procedure assisted with a template based preprocessing. Our methods outperformed other contestants in the competition in both prediction accuracy and circuit size.

Time multiplexing is an important technique to overcome the bandwidth bottleneck of limited input-output pins in FPGAs. Most prior work tackles the problem from a physical design standpoint to minimize the number of cut nets or Time Division Multiplexing (TDM) ratio through circuit partitioning or routing. In this work, we formulate a new orthogonal approach at the logic level to achieve time multiplexing through structural and functional circuit folding. The new formulation provides a smooth trade-off between bandwidth and throughput. Experiments show the effectiveness of the structural method and improved optimality of the functional method on look-up-table and flip-flop usage.

Fanouts are an essential element for signal cloning to achieve logic sharing, but can be a very limited resource in certain emerging technologies, such as quantum circuits, superconducting electronic circuits, photonic integrated circuits, and biological circuits. Although fanout synthesis has been intensively studied for high performance circuit synthesis, prior methods often treat fanout as a soft constraint for critical path optimization or target on specific high-fanout nets such as clock and reset signals. They are not particularly suited for circuit synthesis of these emerging technologies. By treating fanouts as first class citizens, the problem of fanout-bounded logic synthesis was posed as a challenge in the 2019 IWLS Programming Contest. In this paper, we present our winning method, which achieved the overall best quality in the competition, based on fanout load redistribution among existing or expanded equivalent signals.

Engineering change order (ECO) becomes a crucial element in VLSI design flow to rectify function or fix non-functional requirements in late design stages. Even though commercial ECO solutions are available, ECO remains much room for improvement due to its high computational complexity and stringent physical restrictions. It is under active research and development. In this tutorial, we survey recent developments and list some challenges and future directions to make ECO tools more powerful and practical.

The behavioral revisions to the design are frequent in the late stage of the semiconductor chip development. Quite often, their realization emphasizes incrementality that seeks minimum perturbation of the existing implementation. This tutorial paper poses the engineering change order (ECO) problem as the functional decomposition and proposes its solution in the form of the Boolean equations. We hope that the sufficient generality of the statement will be useful in extending the existing stateof-the-art design revision techniques. To assist in this process, we present an observed variety of design revisions encountered in the chip development cycle. The knowledge of such frequent and realistic ECOs is essential in advancing a tool's ability to yield compact implementation updates. We believe that sharing our experience of practical ECOs would benefit the research community in developing an open-source tool.

Synthetic biology has become an important technology in biomedical and many other applications. Despite the enormous progress made, engineering biochemical circuits especially from natural reactions in the real world remains challenging. Most prior work on biochemical circuit synthesis either assumed abstract or hypothetical species and reactions that may not be associated with real-world instances, or lacked scalability due to inefficient search procedures. In this work we propose a Boolean reasoning approach to mining biochemical circuits from enzyme databases to implement a design specification. Experimental results show that our method can synthesize desired biosensor circuits from an enzyme database with more than 200 reactions, and outperforms the state-of-the-art tool.

Uniform sampling is an important method in statistics and has various applications in model counting, system verification, algorithm design, among others. Symbolic sampling in a Boolean space is a recently proposed technique that combines sampling and symbolic representation for effective Boolean reasoning. Under the framework of symbolic sampling, we propose a method to construct compact XOR circuits achieving uniform sampling in a given Boolean space. The method is further extended to biased sampling within a focused subspace of interest. Experimental results show the effectiveness of compact sampling circuit generation and its potential to facilitate Boolean reasoning.

Dependency quantified Boolean formulas (DQBFs) are a powerful formalism, which subsumes quantified Boolean formulas (QBFs) and allows an explicit specification of dependencies of existential variables on universal variables. This enables a succinct encoding of decision problems in the NEXPTIME complexity class. As solving general DQBFs is NEXPTIME complete, in contrast to the PSPACE completeness of QBF solving, characterizing DQBF subclasses of lower computational complexity allows their effective solving and is of practical importance.Recently a DQBF proof calculus based on a notion of fork extension, in addition to resolution and universal reduction, was proposed by Rabe in 2017. We show that this calculus is in fact incomplete for general DQBFs, but complete for a subclass of DQBFs, where any two existential variables have either identical or disjoint dependency sets over the universal variables. We further characterize this DQBF subclass to be ΣP3 complete in the polynomial time hierarchy. Essentially using fork extension, a DQBF in this subclass can be converted to an equisatisfiable 3QBF with only a linear increase in formula size. We exploit this conversion for effective solving of this DQBF subclass and point out its potential as a general strategy for DQBF quantifier localization. Experimental results show that the method outperforms state-of-the-art DQBF solvers on a number of benchmarks, including the 2018 DQBF evaluation benchmarks.

The broad applications of lithium-ion batteries in cyber-physical systems attract intensive research on building energy-efficient battery systems. Reconfigurable battery packs have been proposed to improve reliability and energy efficiency. Despite recent efforts, how to simultaneously maximize battery usage time and minimize switching count during reconfiguration is rarely addressed. In this work, we devise a control algorithm that, under a simplified battery model, achieves the longest usage time under a given constant power-load while the switching count is at most twice above the minimum. It is further generalized for arbitrary power-loads and adjusted for refined battery models. Simulation experiments show promising benefits of the proposed algorithm.

Threshold logic circuits are artificial neural networks with their neuron outputs being binarized, thus amenable for efficient, multiplier-free, hardware implementation of machine learning applications. In the reviving threshold logic synthesis, this work lays the foundations of disjoint-support decomposition and extraction operation of threshold logic functions. They lead to a synthesis procedure for interconnect minimization of threshold logic circuits, an important, but not well addressed, objective in both neural network and nanometer circuit designs. Experimental results show that our method can efficiently and effectively reduce interconnect as well as weight/threshold value over highly optimized circuits, thus suitable for implementation using emerging technologies.

The task of an engineering change order (ECO) is to update the current implementation of a design according to its revised specification with minimum modification. Prior studies show that the amount of design modification majorly depends on the selection of rectification points, i.e., the input pins of gates whose functionality should be rectified with some patch circuitry. In realistic ECOs, as the netlist of the current implementation has been heavily optimized to meet design objectives, it is usually structurally dissimilar to the netlist of a revised specification, which is synthesized only by lightweight optimization. This paper proposes an ECO solution for optimized designs, which is robust against structural dissimilarity caused by design optimization. It locates candidate rectification points in a sampling domain, which significantly improves the scalability of rectification search. To synthesize the circuitry of patches, a structurally independent rewiring formulation is proposed to reuse existing logic in the implementation. Based on the proposed method, a newly developed engine is evaluated on the engineering changes arising in the design of microprocessors. Its ability to derive patches of superior quality is demonstrated in comparison to industrial tools.

In this paper we formulate time-frame folding (TFF) as the reverse operation of time-frame unfolding (TFU), or commonly known as time-frame expansion in automatic test pattern generation (ATPG) and (un)bounded model checking. While the latter converts a sequential circuit into a combinational one with respect to some expansion bound of k time-frames, the former attempts the opposite. TFF arises naturally in the context of testbench generation and bounded strategy generalization, and yet remains unstudied. Unlike TFU, TFF can be highly nontrivial as the subcircuit of each time-frame can be distinct. We propose an algorithm that finds a minimum-state finite state machine consistent with the input-output behavior of the combinational circuit under folding. Empirical evaluation of our method demonstrates its ability in circuit size compaction and suggests potential use in different application domains.

The threshold logic (TL) function, parameterized by a vector of weights and a threshold value, is an important class of Boolean functions that imitate neural information processing. When multiple TL functions are to be implemented in circuits or to be valuated through hardware acceleration, weight sharing among them may provide an effective way for circuit minimization or data compression. We study the condition for a set of TL functions to be implementable with a common weight vector, i.e., representable with parallel separating hyperplanes, and devise a new parameter compression technique. Experimental results demonstrate a 7-fold compression ratio for libraries of TL functions with up to 6 inputs and a data storage reduction to about 45% of the original parameter size for the depthwise convolution layers of an activation-binarized neural network aiming at CIFAR10 dataset classification.

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

As Engineering Change Order (ECO) has attracted substantial attention in modern VLSI design, the open net problem, which aims at constructing a shortest obstacle-avoiding path to reconnect the net shapes in an open net, becomes more critical in the ECO stage. This paper addresses a multi-layer obstacle-avoiding region-to-region Steiner minimal tree (SMT) construction problem that connects all net shapes by edges on a layer or vias between layers, and avoids running through any obstacle with a minimal total cost. Existing multi-layer obstacle-avoiding SMT algorithms consider pin-to-pin connections instead of region-to-region ones, which would limit the solution quality due to its lacking region information. In this paper, we present an efficient algorithm based on our new multi-layer obstacle-avoiding region-to-region spanning graph to solve the addressed problem, which guarantees to find an optimal solution for a net connecting two regions on a single layer. Experimental results show that our algorithm outperforms all the participating routers of the 2017 CAD Contest at ICCAD in both solution quality and runtime.

The increasing system complexity makes engineering change order (ECO) mostly inevitable and a common practice in integrated circuit design. Despite extensive research being made, prior methods are not effectively applicable to instances where rectification is to be done by simultaneously fixing multiple target points using intermediate signals. Moreover, how to efficiently generate low-cost patch functions is rarely addressed. These challenges are posed as a problem in the 2017 ICCAD CAD Contest. Based on Boolean satisfiability and interpolation, we propose a sound and complete algorithm for resource-aware patch generation of multi-target ECO. Experiments show our high quality results compared to other winning teams in the contest.

Neural networks (NNs) are key to deep learning systems. Their efficient hardware implementation is crucial to applications at the edge. Binarized NNs (BNNs), where the weights and output of a neuron are of binary values {–1, +1} (or encoded in {0, 1}), have been proposed recently. As no multiplier is required, they are particularly attractive and suitable for hardware realization. Most prior NN synthesis methods target on hardware architectures with neural processing elements (NPEs), where the weights of a neuron are loaded and the output of the neuron is computed. The load-and-compute method, though area efficient, requires expensive memory access, which deteriorates energy and performance efficiency. In this work we aim at synthesizing BNN dense layers into dedicated logic circuits. We formulate the corresponding matrix covering problem and propose a scalable algorithm to reduce the area and routing cost of BNNs. Experimental results justify the effectiveness of the method in terms of area and net savings on FPGA implementation. Our method provides an alternative implementation of BNNs, and can be applied in combination with NPE-based implementation for area, speed, and power tradeoffs.

Threshold logic functions gain revived attention due to their connection to neural networks employed in deep learning. Despite prior endeavors in the characterization of threshold logic functions, to the best of our knowledge, the quest for a canonical representation of threshold logic functions in the form of their realizing linear inequalities remains open. In this paper we devise a procedure to canonicalize a threshold logic function such that two threshold logic functions are equivalent if and only if their canonicalized linear inequalities are the same. We further strengthen the canonicity to ensure that symmetric variables of a threshold logic function receive the same weight in the canonicalized linear inequality. The canonicalization procedure invokes $O(m)$ queries to a linear programming (resp. an integer linear programming) solver when a linear inequality solution with fractional (resp. integral) weight and threshold values is to be found, where $m$ is the number of symmetry groups of the given threshold logic function. The guaranteed canonicity allows direct application to the classification of NP (input negation, input permutation) and NPN (input negation, input permutation, output negation) equivalence of threshold logic functions. It may thus enable applications such as equivalence checking, Boolean matching, and library construction for threshold circuit synthesis.

Stochastic Boolean satisfiability (SSAT) is an expressive language to formulate decision problems with randomness. Solving SSAT formulas has the same PSPACE-complete computational complexity as solving quantified Boolean formulas (QBFs). Despite its broad applications and profound theoretical values, SSAT has received relatively little attention compared to QBF. In this paper, we focus on exist-random quantified SSAT formulas, also known as E-MAJSAT, which is a special fragment of SSAT commonly applied in probabilistic conformant planning, posteriori hypothesis, and maximum expected utility. Based on clause selection, a recently proposed QBF technique, we propose an algorithm to solve E-MAJSAT. Moreover, our method can provide an approximate solution to E-MAJSAT with a lower bound when an exact answer is too expensive to compute. Experiments show that the proposed algorithm achieves significant performance gains and memory savings over the state-of-the-art SSAT solvers on a number of benchmark formulas, and provides useful lower bounds for cases where prior methods fail to compute exact answers.

Strings with length constraints are prominent in software security analysis. Recent endeavors have made significant progress in developing constraint solvers for strings and integers. Most prior methods are based on deduction with inference rules or analysis using automata. The former may be inefficient when the constraints involve complex string manipulations such as language replacement; the latter may not be easily extended to handle length constraints and may be inadequate for counterexample generation due to approximation. Inspired by recent work on string analysis with logic circuit representation, we propose a new method for solving string with length constraints by an implicit representation of automata with length encoding. The length-encoded automata are of infinite states and can represent languages beyond regular expressions. By converting string and length constraints into a dependency graph of manipulations over length-encoded automata, a symbolic model checker for infinite state systems can be leveraged as an engine for the analysis of string and length constraints. Experiments show that our method has its unique capability of handling complex string and length constraints not solvable by existing methods.

In the nanometer regime of integrated circuit fabrication, device variability imposes serious challenges to the design and manufacturing of reliable systems. A new computation paradigm of approximate and probabilistic design has been proposed recently to accept design imperfection as a resource for certain applications. Despite recent intensive study on approximate design, probabilistic design receives relatively few attentions. This paper provides a general formulation for the evaluation and verification of probabilistic design. We establish their connection to stochastic Boolean satisfiability (SSAT), (weighted) model counting, and probabilistic model checking. Moreover, a novel SSAT solver based on binary decision diagram (BDD) is proposed, and a comparative experimental study is performed to contrast the strengths and weaknesses of different solutions. The proposed BDD-based SSAT solver obtains the best scalability among all techniques in our experiments. We also compare the BDD-based SSAT solver to a prior method based on Bayesian network modeling. Experimental results show that our method outperforms the prior method by orders of magnitude in both runtime and memory usage. Our work can be an essential step towards automated synthesis of probabilistic design.

Functional timing analysis (FTA) overcomes the limitation of static timing analysis (STA) to allow distinction of false and true paths. Modern FTA methods exploit timed characteristic functions (TCFs) to implicitly calculate the longest true delay of a circuit. However, they are inadequate for the verification of timing exceptions, which is crucial for timing signoff, due to their implicit enumeration of all paths rather than specific paths of concern. We present the first TCF-based FTA method for path-specific timing verification under both floating and transition modes of operation. Experiments demonstrate the unique benefit and scalability of our method.

Asynchronous methodologies are gaining their presence in modern integrated circuit design. Cycle-time analysis of asynchronous design is nontrivial and crucial to circuit optimization. Among prior methods, linear programming-based analysis (LPA) and static performance analysis (SPA) are two representatives with high accuracy (but inefficient) and high efficiency (but inaccurate), respectively. However, the exactness of LPA remains unknown and the accuracy of SPA remains room for improvement. In this work, we demonstrate the inexactness of LPA and enhance the accuracy of SPA. Experimental results suggest our enhanced SPA almost always returns exact cycle-times while achieving up to 4000x speedup over LPA.

Engineering change order (ECO) is pivotal in rectifying late design changes that occur commonly due to ever-increasing system complexity. Existing functional ECO methods focus on combinational equivalence assuming a known input correspondence between the old implementation and new specification. They are inadequate for rectifying circuits under sequential transformations. This inadequacy hinders the utilization of powerful and effective sequential optimization methods using retiming and resynthesis. As retiming and/or resynthesis gains increasing adoption in industry, incorporating sequential ECO techniques into the hardware design flow becomes essential. In this paper, we provide the first attempt to extend ECO to designs under retiming and resynthesis in an industrial flow by leveraging conventional combinational ECO engine. Experimental results over industrial ECO benchmarks justify the promising practicality of our methods.

Stochastic Boolean Satisfiability (SSAT) is a powerful formalism to represent computational problems with uncertainly, such as belief network inference and propositional probabilistic planning. Solving SSAT formulas lies in the same complexity class (PSPACE-complete) as solving Quantified Boolean Formula (QBF). While many endeavors have been made to enhance QBF solving, SSAT has drawn relatively less attention in recent years. This paper focuses on random-exist quantified SSAT formulas, and proposes an algorithm combining binary decision diagram (BDD), logic synthesis, and modern SAT techniques to improve computational efficiency. Unlike prior exact SSAT algorithms, the proposed method can be easily modified to solve approximate SSAT by deriving upper and lower bounds of satisfying probability. Experimental results show that our method outperforms the state-of-the-art algorithm on random k-CNF formulas and has effective application to approximate SSAT on circuit benchmarks.

Self-aligned triple patterning (SATP) lithography is one of the most promising technologies for next-generation semiconductor manufacturing process. Self-aligned patterning attracts much interest because of its significant advantage over the litho-etch-litho-etch patterning in reducing the overlay problem in lithography. However, pattern decomposition in SATP is challenging due to its counterintuitive mask synthesis. It remains relatively unstudied and its practical solutions remain to be proposed. This paper proposes an effective algorithm for SATP layout decomposition without grid-based quantization and thus substantially reduces the number of variables and constraints in solution search. Boolean satisfiability (SAT) and integer linear programming (ILP) are exploited for efficient computation. In addition to deriving high-quality layout decomposition solutions with overlay minimization, our method also allows nondecomposable spot identification to facilitate layout rectification. Experimental results demonstrate the superiority of our method compared to prior work and show the relative advantages of SAT and ILP formulations.

Equivalence checking and functional correction are important steps ensuring design correctness. Direct verification of large industrial designs is challenging and often requires a divide-and-conquer approach. The 2015 CAD Contest at ICCAD poses the challenge of large-scale equivalence checking and functional correction. This paper reports our work in the competition. An algorithm to identify cut-points in both equivalent and inequivalent circuit pairs is proposed for design partitioning. To obtain high quality cuts, we take into consideration their proximity information in cone sizes and circuit depths. Experiments on the contest benchmarks show our method achieves top quality results among all contestants.

Threshold logic circuits gain increasing attention due to their feasible realization with emerging technologies and strong bind to neural network applications. In this paper, for logic synthesis we formulate the fundamental operation of collapsing threshold logic gates, not addressed by prior efforts. A necessary and sufficient condition of collapsibility is obtained for linear combination of two threshold logic gates, and an analytic approach is proposed for fast circuit transformation. On the other hand, for equivalence verification we propose a linear time translation from threshold logic circuits to pseudo-Boolean constraints, in contrast to prior exponential translation costs. Experimental results demonstrate the effectiveness of circuit transformation by the collapse operation and the memory efficiency of equivalence verification by our pseudo-Boolean translation.

Skolem and Herbrand functions are important certificates validating the truth and falsity, respectively, of quantified Boolean formulas (QBFs). They are essential in various synthesis and verification applications. Recent advancement established a linear time extraction of Skolem/Herbrand functions from QBF consensus/resolution proofs. However, the obtained functions are often excessively large and improper for practical applications. To overcome this limitation, this paper characterizes various flexibilities of QBF certificates, and exploits them for certificate simplification. Experiments show substantial reduction on QBF certificates in terms of circuit size and depth, which are of primary concerns for synthesis applications.

Extreme ultraviolet (EUV) flare and post-chemical mechanical polishing (CMP) metal thickness are two main manufacturability concerns that introduce critical dimension distortions in nanometer process technology. Dummification, the addition of dummy patterns, is an effective technique to address the two concerns. However, while the two dummification objectives are competing in nature, existing works only tackle them separately, leading to problem-prone solutions because optimizing one would unavoidably deteriorate the other. This paper presents a new and effective method that simultaneously considers both concerns during dummification. Manufacturing sensitivity toward the two concerns are taken into account with a user-specified evaluation model adaptive to the adopted technology. Given the point spread function of a system and the evaluation model, our proposed two-stage method is able to find at the first stage an initial dummy assignment with better EUV flare uniformity than that obtained by a previous quasi-inverse method. With the initial assignment as the starting point, the gradient-guided optimization is then adopted to iteratively refine dummy distribution toward improved CMP quality. Experimental results on industrial test cases show the effectiveness of our method.

The increasing cost paid in clocking integrated circuits and combating timing variations forces designers to rethink asynchronous approaches to system realization. Among various techniques, quasi-delay insensitive design is promising due to its very relaxed timing assumption. Its expensive logic overhead, however, often nullifies its promise of performance and power improvements, and remains a major obstacle on the way of its adoption. To overcome this obstacle, this paper proposes an efficient static performance analysis procedure and a synthesis flow for precharged half buffer and weak-conditioned half buffer circuit optimization. Experimental results demonstrate efficient performance analysis and effective area reduction under pipeline cycle time constraints.

Many computer science problems can be naturally and compactly expressed using quantified Boolean formulas (QBFs). Evaluating thetruth or falsity of a QBF is an important task, and constructing the corresponding model or countermodel can be as important and sometimes even more useful in practice. Modern search and learning based QBF solvers rely fundamentally on resolution and can be instrumented to produce resolution proofs, from which in turn Skolem-function models and Herbrand-function countermodels can be extracted. These (counter)models are the key enabler of various applications. Not until recently the superiority of long-distanceresolution (LQ-resolution) to short-distance resolution(Q-resolution) was demonstrated. While a polynomial algorithm exists for (counter)model extraction from Q-resolution proofs, it remains open whether it exists forLQ-resolution proofs. This paper settles this open problem affirmatively by constructing a linear-time extraction procedure. Experimental results show the distinct benefits of the proposed method in extracting high quality certificates from some LQ-resolution proofs that are not obtainable from Q-resolution proofs.

Retention registers are utilized in power gating design to hold design state during power down and to allow safe and fast system reactivation. Since a retention register consumes more power and costs more area than a non-retention register, it is desirable to minimize the use of retention registers. However, relaxing retention requirement to a minimal subset of registers can be computationally challenging. In this paper, we adopt satisfiability solving for scalable selection of registers whose retention is unnecessary and exploit input sequence constraints to increase the number of non-retention registers. Empirical results on industrial benchmarks show that our proposed methods are efficient and effective in identifying non-retention registers.

Reactive system synthesis from safety specifications is a promising approach to the correct-by-construction methodology. The synthesis process is often divided into two separate steps: First, check specification realizability by computing the winning region of states under a game-theoretic interpretation; second, synthesize the implementation circuit based on the computed winning region if the specification is realizable. Moreover, recent results suggest that methods based on satisfiability (SAT) solving outperform those based on Binary Decision Diagrams (BDDs) especially on large benchmark instances. In this paper, we focus on the the winning region computation and propose a SAT-based algorithm. By adopting the concepts from the state-of-the-art model checking algorithm property directed reachability (PDR, a.k.a. IC3), we aim at devising an efficient computation method for automatic controller synthesis. Experimental results on the benchmarks from the synthesis competition (SyntComp 2014) show that our proposed algorithm outperforms the existing SAT-based and QBF-based methods by some margin.

Asynchronous circuits are promising in resolving the emerging issue of process variation and high synchronization power consumption. Among various asynchronous delay models, quasi-delay insensitive (QDI) model is the most robust and yet practical one due to its relaxed timing assumption. However, automatic synthesis of QDI circuits from signal transition graph (STG) protocol specification has not yet been proposed, despite the fact that algorithms synthesizing circuits under other delay models do exist. In this paper we propose the first algorithm synthesizing protocols specified in STGs into QDI circuits by analyzing STG structures without utilizing state graph assignment techniques. Furthermore, an optimization technique is proposed to simplify QDI circuits. In our synthesis algorithm, the state explosion issue is avoided, and restrictions on STGs are relaxed. Case studies on Advanced Microcontroller Bus Architecture (AMBA) and other protocols indicate the feasibility of our method.

Asynchronous design methodologies gain recent extensive attention due to the variability issues in fabricating nanometer integrated circuits. Prior work on asynchronous pipeline performance analysis mostly focused on full buffer pipelines. To date half buffer performance analysis still lacks a systematic and precise treatment. In this paper, we propose a general framework abstracting four-phase asynchronous protocols and thus uniquely enable efficient performance analysis on various acyclic quasi-delay insensitive (QDI) pipelines (including the well-known pre-charged full buffer (PCFB), pre-charged half buffer (PCHB), weak-conditioned half buffer (WCHB), and null convention logic (NCL)) whose analysis has been challenging, if not impossible. Two approaches, linear programming-based performance analysis (LPA) and static performance analysis (SPA), that were applicable only to restricted set of full-buffer and half-buffer pipelines, respectively, are extended to support the entire set of considered pipelines. Thereby the two approaches can be directly compared for the first time. Experiments show that on average SPA achieve five orders of magnitude speedup over LPA, while LPA may provide 7% to 22% tighter cycle time estimation than SPA. Our results are essential to scalable performance analysis for a comprehensive set of QDI circuits.

Performance analysis and deadlock verification are two critical issues in asynchronous circuit design, which can be advantageous over the synchronous counterpart in terms of robustness against timing variability, security against side-channel attack, and other benefits. Nevertheless, asynchronous design automation tools are far away from mature. In this paper, we advance the synthesis of quasi-delay insensitive (QDI) circuits of pre-charged half buffer (PCHB) and weak-conditioned half buffer (WCHB) pipelines in three respects. First, static performance analysis (SPA) with linear time complexity is generalized from acyclic to cyclic PCHB and WCHB pipelines. Second, a deadlock verification (DV) algorithm with linear time complexity is proposed for checking PCHB and WCHB pipelines using their four-phase marked graph models. Third, we propose a new simple register circuitry for PCHB and WCHB pipelines that consists of one reset-latch and one buffer-latch and is amenable to circuit minimization. With the above two algorithms, we develop an efficient synthesis flow for buffer-latch minimization while maintaining the system throughput and deadlock-free property. Experimental results show the efficiency of our SPA and DV algorithms and demonstrate the effectiveness of our synthesis method with an average of 37% reduction on the number of buffer-laches. As our SPA and DV algorithms are applicable to arbitrary PCHB and WCHB pipelines and our buffer-latch minimization algorithm is orthogonal to existing synthesis methods such as cut-based technology mapping and slack matching, our methods can be generally useful in the analysis, verification, and synthesis of PCHB and WCHB pipelines.

The composition of two arbitrary component automata can have deadlock states. A method is proposed to minimally reduce a component automaton such that the resulting composition with the other automaton is deadlock-free. The method is applied to deriving compositionally deadlock-free solutions of automata equations over the synchronous composition.

The increasing cost paid in clocking integrated circuits and combating timing variations forces designers to rethink asynchronous approaches to system realization. Among various techniques, quasi-delay-insensitive (QDI) design is promising due to its very relaxed timing assumption. Its expensive logic overhead, however, often nullifies its promise of performance and power improvements, and remains a major obstacle against its adoption. To overcome this obstacle, this paper proposes an efficient static performance analysis procedure and a synthesis flow for precharged half buffer (PCHB) and weak-conditioned half buffer (WCHB) circuit optimization. Experimental results demonstrate efficient performance analysis and effective area reduction under pipeline cycle time constraints.

EUV flare and CMP metal thickness are two main manufacturability concerns for nanometer process technology. The two dummification objectives, however, are conflicting with each other in nature, but existing works only tackle them separately, leading to problem-prone solutions because optimizing one would deteriorate the other. This paper presents the first work that simultaneously considers both concerns during manufacturability optimization. Given a system's point spread function, our proposed method first finds an initial solution with better-than-state-of-the-art EUV flare uniformity, then followed by gradient-guided optimization to iteratively refine density uniformity. Experimental results show the effectiveness of our method.

In the nanometer regime of integrated circuit fabrication, device variability imposes serious challenges to the design of reliable systems. A new computation paradigm of approximate and probabilistic design has been proposed recently to accept design imperfection as a resource for certain applications. Despite recent intensive study on approximate design, probabilistic design receives relatively few attentions. This paper provides a general formulation for the evaluation and verification of probabilistic design. We establish its connection to stochastic Boolean satisfiability (SSAT), (weighted) model counting, signal probability calculation, and probabilistic model checking. A comparative experimental study is performed to contrast the strengths and weaknesses of different solutions. Our study can be an essential step towards automated synthesis of probabilistic design.

Encoding and decoding are common practice in data processing. Designing encoder and decoder circuitry manually can be error prone and time consuming. Although great progress has been made on automating decoder synthesis from its encoder specification, prior specification was limited to an uninitialized encoder only, whose decoder in turn cannot depend on the entire execution history of the encoder. Prior decoder existence condition is unnecessarily stringent as encoders are often initialized to some specific starting states. This paper shows how decoders of initialized encoders can be practically synthesized. Experimental results demonstrate effective decoder synthesis of initialized encoders, beyond existing methods' capabilities.

Testing integrated circuits under delay defects becomes an essential quality control step in nanometer fabrication technologies, which encounter inevitable process variations. Prior methods on automatic test pattern generation (ATPG) for delay defects, however, are either overly simplified (e.g., timing unaware) or computationally too expensive. This paper proposes a viable ATPG method based on a satisfiability (SAT) formulation using timed characteristic functions (TCFs), which gained notable scalability enhancement very recently. The approach provides a balanced trade-off between accuracy and efficiency. Experimental results show promising runtime and fault coverage improvements over prior SAT-based timing-aware ATPG methods. Moreover, our method provides a nice complement to commercial tools in enhancing test quality.

In high-level designs, variables are often naturally represented in a symbolic multi-valued form. Binary encoding is an essential step in realizing these designs in Boolean circuits. This paper poses the encoding problem with the objective of maximizing the degree of symmetry, which has many useful applications in logic optimization, circuit rewiring, functional decomposition, etc. In fact, it is guaranteed that there exists a full symmetry encoding with respect to every input multivalued variable for all multi-valued functions. We propose effective computation for finding such encoding by solving a system of subset-sum constraints. Experiments show unique benefits of symmetry encoding.

In contrast to structural timing analysis, functional timing analysis for circuit delay computation is accurate, but computationally expensive in refuting false critical paths. Despite recent progress on satisfiability-based functional timing analysis, the formulation generality and computation efficiency remain room for further improvement. This paper provides a unified view on different notions of timed characteristic functions and efficient transformation for satisfiability solving. Experimental results show that functional timing analysis on industrial designs can be made up to several orders of magnitude faster and more generally applicable than prior methods.

Due to the ever-increasing complexity of system design, it becomes not uncommon for some design error escaping all verification efforts and settling in final silicon realization. As hardware-based fixing is much more expensive than software-based fixing, this paper proposes a methodology as a first step toward generating software workarounds for erroneous processor designs. A generic formulation is introduced based on Skolem and Herbrand function extraction from quantified Boolean formula solving; reduction techniques are devised to further enhance practicality. Thereby, a program can be recompiled at the assembly code level for correct execution on a buggy processor. Experimental results show the feasibility of the proposed method.

With increasing circuit complexities, design bugs are commonly found in late design stages, and thus engineering change orders (ECOs) have become an indispensable process in modern VLSI design. Most prior approaches to the timing ECO problem are concerned about combinational logic optimization. In contrast, this paper addresses the problem in the sequential domain to explore more optimization flexibility. We propose an orthogonal method of post-mask clock scheduling with spare cells. Compared to traditional clock scheduling, clock scheduling in the ECO stage is more challenging in that it confronts limited spare-cell resources and dynamic changes of wiring cost incurred by different spare-cell selections. Based on mixed-integer linear programming (MILP), our formulation considers not only gate sizing and buffer insertion using spare cells, but also wire snaking. Experimental results based on five industrial designs show the effectiveness of our work. Our framework has been integrated into a commercial design flow.

Functional, in contrast to structural, timing analysis is accurate, but computationally expensive in refuting false critical paths. Although satisfiability-based analysis using timed characteristic functions has been proposed, its efficiency and generality remain room for improvement. This paper shows functional timing analysis on industrial designs can be made up to several orders of magnitude faster and more generally applicable than prior methods.

Computing with biochemical reactions emerges in synthetic biology. With high-level programming languages, a target computation can be intuitively and effectively specified. As control flows form the skeleton of most programs, how to translate them into biochemical reactions is crucial but remains ad hoc. This paper shows a systematic approach to transforming control flows into robust molecular reactions. Case studies demonstrate its usefulness.

Achieving high coverage is an important goal in design verification. Fixing coverability problems found at the verification stage, however, can require tremendous effort. To address this problem, we propose a flow for analyzing code and variable-toggle coverability at the early-RTL block-level stage. In addition, we devise a novel technique to analyze the coverability problems so that engineers can resolve the issues more efficiently. By identifying coverability problems at early RTL design stages, design verifiability can be improved, thus reducing the effort required at the verification phase.

Due to increasing integrated circuit design complexity, engineering change orders (ECOs) have become a necessary technique to resolve late-found functional errors and/or performance deficiencies. To fix timing violations, gate sizing and buffer insertion are commonly used in postmask ECO. These techniques, however, may not be powerful enough, especially when spare cells are inserted to balance between functional and timing repair capabilities. We propose a postmask ECO technique, called TRECO, to remedy timing violations based on technology remapping, which also supports functional ECO. Unlike conventional technology mapping, TRECO performs technology mapping with respect to a limited set of spare cells and confronts dynamic changes of wiring cost incurred by selection of different spare cells. With a precomputed lookup table of representative circuit templates, TRECO iteratively performs technology remapping to restructure timing critical subcircuits until no timing violation can be further removed. Experimental results on five industrial designs show the effectiveness of TRECO in ECO timing optimization and in timing-aware functional ECO.

Upon receiving the output sequence streaming from a sequential encoder, a decoder reconstructs the corresponding input sequence that streamed to the encoder. Such an encoding and decoding scheme is commonly encountered in communication, cryptography, signal processing, and other applications. Given an encoder specification, decoder design can be error-prone and time consuming. Its automation may help designers improve productivity and justify encoder correctness. Though recent advances showed promising progress, there is still no complete method that decides whether a decoder exists for a finite state transition system. The quest for completely automatic decoder synthesis remains. This paper presents a complete and practical approach to automating decoder synthesis via incremental Boolean satisfiability solving and Craig interpolation. Experiments show that, for decoder-existent cases, our method synthesizes decoders effectively; for decoder-nonexistent cases, our method concludes the nonexistence instantly while prior methods may fail. Case studies are also conducted in synthesizing decoders for linear error-correcting codes.

Upon receiving the output sequence streaming from a sequential encoder, a decoder reconstructs the corresponding input sequence that streamed to the encoder. Such an encoding and decoding scheme is commonly encountered in communication, cryptography, signal processing, and other applications. Given an encoder specification, decoder design can be error-prone and time consuming. Its automation may help designers improve productivity and justify encoder correctness. Though recent advances showed promising progress, there is still no complete method that decides whether a decoder exists for a finite state transition system. The quest for completely automatic decoder synthesis remains. This paper presents a complete and practical approach to automating decoder synthesis via incremental SAT solving and Craig interpolation. Experiments show that, for decoder-existent cases, our method synthesizes decoders effectively; for decoder-nonexistent cases, our method concludes the non-existence instantly while prior methods may fail.

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.

Due to the increasing IC design complexity, Engineering Change Orders (ECOs) have become a necessary technique to resolve late-found functional and/or timing deficiencies. To fix timing violations, the principles of gate sizing and buffer insertion are commonly used in post-mask ECO. These techniques however may not be powerful enough, especially when spare cells are inserted in a way of striking a balance between functional and timing repair capabilities. We propose a post-mask ECO technique, called TRECO, to remedy timing violations based on technology remapping, which supports functional ECO as well. Unlike conventional technology mapping, TRECO performs technology mapping with respect to a limited set of spare cells and confronts dynamic changes of wiring cost incurred by different spare-cell selections. With a pre-computed lookup table of representative circuit templates, TRECO iteratively performs technology remapping to restructure timing critical sub-circuits until no timing violation remains. Experimental results on five industrial designs show the effectiveness of TRECO in ECO timing optimization.

Boolean matching determines whether two given (in)completely-specified Boolean functions can be identical or complementary to each other under permutation and/or negation of their input variables. Due to its broad applications in logic synthesis and verification, it attracted much attention. Most prior efforts however were incomplete and/or restricted to certain special matching conditions. In contrast, this paper focuses on the computation kernel of Boolean matching and proposes a complete generic framework. Through conflict-driven learning and abstraction, the capacity of Boolean matching scales up due to the effective pruning of infeasible matching solutions. Experiments show encouraging results in resolving hard instances that are otherwise unsolvable.

Boolean matching for multiple-output functions determines whether two given (in)completely-specified function vectors can be identical to each other under permutation and/or negation of their inputs and outputs. Despite its importance in design rectification, technology mapping, and other logic synthesis applications, there is no much direct study on this subject due to its generality and consequent computational complexity. This paper extends our prior Boolean matching decision procedure BooM to consider multiple-output functions. Through conflict-driven learning and partial assignment reduction, Boolean matching in the most general setting can still be accomplishable even when all other techniques lose their foundation and become unapplicable. Experiments demonstrate the indispensable power of strengthened learning for practical applications.

Functional rectification in late design stages has been a crucial process in modern complex system design. This paper proposes a robust functional ECO engine, which applies SAT proof minimization and interpolation techniques to automate patch construction to make old implementation and golden specification functionally equivalent. The SAT proof minimization technique provides a sound and efficient way of fixing easy errors, and the interpolation technique provides a complete and robust way of fixing remaining errors. Experimental results show that our engine performs robustly to generate small patches in fixing various design rectification instances.

Functional dependency is concerned with rewriting a Boolean function f as a function h over a set of base functions {g1,¿,gn}, i.e., f = h(g1,¿,gn). It plays an important role in many aspects of electronic design automation (EDA). Prior approaches to the exploration of functional dependency are based on binary decision diagrams (BDDs), which may not be easily scalable to large designs. This paper formulates both single-output and multiple-output functional dependencies as satisfiability (SAT) solving and exploits extensively the capability of a modern SAT solver. Thereby, functional dependency can be detected effectively through incremental SAT solving, and the dependency function h, if it exists, is obtained through Craig interpolation. The proposed method enables (1) scalable detection of functional dependency, (2) fast enumeration of dependency function under a large set of candidate base functions, and (3) potential application to large-scale logic synthesis and formal verification. Experimental results show that the proposed method is far superior to prior work and scales well in dealing with the largest ISCAS and ITC benchmark circuits with up to 200 K gates.

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.

Boolean relations are an important tool in system synthesis and verification to characterize solutions to a set of Boolean constraints. For physical realization as hardware, a deter-ministic function often has to be extracted from a relation. Prior methods however are unlikely to handle large problem instances. From the scalability standpoint this paper demon-strates how interpolation can be exploited to extend deter-minization capacity. A comparative study is performed on several proposed computation techniques. Experimental re-sults show that Boolean relations with thousands of variables can be effectively determinized and the extracted functional implementations are of reasonable quality. 1.

Boolean function bi-decomposition is a fundamental operation in logic synthesis. A function f(X) is bi-decomposable under a variable partition XA,XB,XC on X if it can be written as h(fA(XA,XC),fB(XB, XC)) for some functions h, fA, and fB. The quality of a bi-decomposition is mainly determined by its variable partition. A preferred decomposition is disjoint, i.e. XC = ø, and balanced, i.e. |XA| ã |XB|. Finding such a good decomposition reduces communication and circuit complexity, and yields simple physical design solutions. Prior BDD-based methods may not be scalable to decompose large functions due to the memory explosion problem. Also as decomposability is checked under a fixed variable partition, searching a good or feasible partition may run through costly enumeration that requires separate and independent decomposability checkings. This paper proposes a solution to these difficulties using interpolation and incremental SAT solving. Preliminary experimental results show that the capacity of bi-decomposition can be scaled up substantially to handle large designs.

Functional decomposition is a fundamental operation in logic synthesis. Prior BDD-based approaches to functional decomposition suffer from the memory explosion problem and do not scale well to large Boolean functions. Variable partitioning has to be specified a priori and often restricted to a few bound-set variables. Moreover, non-disjoint decomposition requires substantial sophistication. This paper shows that, when Ashenhurst decomposition (the simplest and preferable functional decomposition) is considered, both single-and multiple-output decomposition can be formulated with satisfiability solving, Craig interpolation, and functional dependency. Variable partitioning can be automated and integrated into the decomposition process without the bound-set size restriction. The computation naturally extends to non-disjoint decomposition. Experimental results show that the proposed method can effectively decompose functions with up to 300 input variables.

Technology mapping aims at searching an optimal implementation for a Boolean netlist using gates from a technology library. Compared with its NP-complete area minimization counterpart, DAG mapping for delay minimization is considered much sophisticated because matching choices must be made without knowing actual arrival times and output loads. Traditional approaches to this problem involve too many approximate simplifications, and are far from accurate. In contrast, this paper tackles this problem directly under load-dependent DAG mapping. The enabling techniques for accurate optimization include on-the-fly load-estimation refinement, breadth-first backward covering for load consolidation, and use of a piecewise linear model for accurate timing calculation. Experimental results show that, compared with the state-of-the-art mapper, our method averagely reduces circuit delay by 39%, with 11% increase in area, for large benchmark circuits.

Retiming and resynthesis are among the most important tech- niques for practical sequential circuit optimization. However, their applicability is much limited due to verification con- cerns. Overcoming the verification bottleneck is a supreme task. This paper studies both the theoretical and practical aspects of inductive verification on the equivalence between circuits under retiming and resynthesis transformation. We study the completeness condition of the inductive approach to equivalence checking and show that prior work is only com- plete for circuits transformed under retiming or resynthesis, but not both. We overcome prior limitation and make complete the equivalence checking for circuits transformed up to retiming+resynthesis+retiming. The theoretical insights lead to a robust satisfiability formulation of verification un- der various retiming and resynthesis scenarios. Experimental results demonstrate the scalability of the approach. Several previously unverifiable circuits and unverifiable transforma- tion scenarios can now be verified effectively.

Functional dependency is concerned with rewriting a Boolean function f as a function h over a set of base functions {g1, ..., gn), i.e. f = h(g1, ..., gn). It plays an important role in many aspects of electronic design automation (EDA), ranging from logic synthesis to formal verification. Prior approaches to the exploration of functional dependency are based on binary decision diagrams (BDDs), which may not be easily scalable to large designs. This paper proposes a novel reformulation that extensively exploits the capability of modern satisfiability (SAT) solvers. Thereby, functional dependency is detected effectively through incremental SAT solving, and the dependency function h, if it exists, is obtained through Craig interpolation. The main strengths of the proposed approach include: (1) fast detection of functional dependency with modest memory consumption and thus scalable to large designs, (2) a full capacity to handle a large set of base functions and thus discovering dependency whenever exists, and (3) potential application to large-scale logic optimization and verification reduction. Experimental results show the proposed method is far superior to prior work and scales well in dealing with the largest ISCAS89 and ITC99 benchmark circuits with up to 200 K gates.

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

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.

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.

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.

Functional decomposition has recently been adopted for look-up table (LUT)-based field-programmable gate array (FPGA) technology mapping with good results. In this paper we propose a novel method to unify functional single-output and multiple-output decomposition. We first address a compatible class encoding algorithm to minimize the number of compatible classes in the image function. After applying the encoding algorithm, we can therefore improve the decomposability in the subsequent decomposition of the image function. The above encoding algorithm is then extended to encode multiple-output functions through the construction of a hyperfunction. Common subexpressions among these multiple-output functions can be extracted during the decomposition of the hyperfunction. Consequently, we can handle multiple-output decomposition in the same manner as single-output decomposition. Experimental results show that our algorithms are promising.

With increasing density and capacity due to technology scaling, augmenting data (especially in semiconductor memories) burden selection circuitry with exponentially growing capacitive loads. This tendency violates stringent timing requirements. This work ameliorates the situation for k-stage tree-type decision circuitry. We show that for a k-stage binary decision tree, there always exists an optimum solution such that, after the select-signal arrangement, the worst case loading among select signals equals a lower bound. Our proposed procedure not only provides an optimum solution but also minimizes the loading variance. The worst case loading can be reduced up to nearly k/2 times, thus speeding up and saving power up to W2 times or so for the select signal with the heaviest loading. In contrast, excluding one unit-loading select signal, the empirical variance of the remaining (k-1) signals is always less than 1 instead of diverging. Hence, our approach, for timing-driven layout synthesis, is competent to design high-performance tree-type decision circuitry with more accurate timing and power prediction. In addition, by the presented approach, we can have the alternative of optimizing either for k-stage or for (k-1)-stage, meanwhile possibly minimizing the other. Our algorithm, also, can easily be extended for a general k-stage decision tree with r descendants per node, not restricted to a binary tree; the resultant worst case loading could be quite close to the lower bound and reduced up to nearly k(r-1)/r times.

Recently, functional decomposition has been adopted for LUT based FPGA technology mapping with good results. In this paper, we propose a novel method for functional multiple-output decomposition. We first address a compatible class encoding method to minimize the compatible classes in the image function. After the encoding algorithm is applied, the decomposability will be improved in the subsequent decomposition of the image function. The above encoding algorithm is then extended to encode multiple-output functions through the construction of a hyper-function. Common sub-expressions among these multiple-output functions can be extracted during the decomposition of the hyper-function. Therefore, we can handle the multiple-output decomposition in the same manner as the single-output decomposition. Experimental results show that our algorithms are very promising.

Field Programmable Gate Arrays (FPGAs) are important devices for rapid system prototyping. Roth-Karp decomposition is one of the most popular decomposition techniques for Look-Up Table (LUT)-based FPGA technology mapping. In this paper, we propose a novel algorithm based on Binary Decision Diagrams (BDDs) for selecting good lambda set variables in Roth-Karp decomposition to minimize the number of consumed configurable logic blocks (CLBs) in FPGAs. The experimental results on a set of benchmarks show that our algorithm can produce much better results than those of the previous approach (Wen-Zen Shen et al., 1995).