Sequential logic synthesis expands the solution space compared to combinational logic synthesis by reasoning about the reachable states of memory elements, leading to better Power-Performance-Area (PPA) outcomes. As gate costs continue to rise in advanced technologies, sequential logic synthesis is gaining significant traction within the EDA community as a powerful alternative. This paper introduces a scalable algorithm for don’t-care-based sequential logic synthesis, leveraging sequential k-step induction to perform redundancy removal and resubstitution under Sequential Observability Don’t Cares (SODCs). SODCs generalize Observability Don’t Cares (ODCs) by explicitly considering reachable states, making SODC-based optimization a challenging problem due to dependencies and alignment issues between the base case and inductive case in k-step induction. Our approach overcomes these challenges, fully utilizing the potential of SODCs without limiting the solution space. We rigorously prove the correctness of our approach, discuss some limitations arising from bounded-step induction, and analyze how our approach can effectively be used in practice to exploit obscure optimization opportunities. Implemented as part of an industrial tool, our algorithm achieves an average -6.9% area improvement after technology mapping compared to state-of-the-art sequential synthesis methods, and further provides 3.16% and 1.06% reductions in combinational and sequential areas, respectively, in post place-and-route results. Furthermore, all optimizations are efficiently verified using industrial sequential verification tools.

We address the problem of minimizing the area of circuits mapped to a technology library, with or without delay constraints. While traditional methods optimize first a technology-independent representation and then perform technology mapping to a library, this paper explores the potential for further optimizations through technology-dependent algorithms. We propose an optimization engine for mapped circuits that relies on a database of mapped sub-networks for efficient resynthesis. Experimental results on the EPFL benchmarks after area-oriented optimization and mapping show that the proposed method leads to average area improvements of 5.47% without degrading the delay.

High-effort logic synthesis has become an important research direction due to the increase in silicon cost and the growth of design complexity. The emphasis on security leads to complex cryptographic circuits, while the acceleration of AI/ML results in custom arithmetic blocks---all of which need to be highly optimized by EDA tools. In such applications, high-effort logic synthesis allows for an efficient exploration of larger solution spaces, leading to area and power savings beyond the capacity of traditional methods. This paper presents a novel variation of high-effort logic synthesis called transduction, which performs transformation and reduction using don't-cares to restructure the circuit. Integrating the proposed method into a stochastic optimization flow with dynamic scheduling saved 6.8% AIG nodes on average, compared to the original flow using the same runtime. An additional experiment further demonstrated the strength of the proposed method, which derived smaller AIGs than the previously synthesized minimum AIGs for 46 out of 100 benchmarks.

Combinational equivalence checking for hardware design tends to be slow due to the number and complexity of in-termediate node equivalences considered by the SAT solver. This is because the solver often spends extensive time disproving nodes that appear equivalent under random simulation. We propose SimGen, an open-source and expressive simulation pattern generator inspired by Automatic Test Pattern Generation (ATPG); it exploits the circuit's structure to disprove the equivalence of circuit nodes and avoid excessive SAT calls. We demonstrate the effectiveness of SimGen's simulation patterns over those generated by state-of-the-art random and guided simulation.

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.

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

This paper addresses the challenge of reducing the number of nodes in Look-Up Table (LUT) networks with two significant applications. First, Field-Programmable Gate Arrays (FPGAs) can be modelled as networks of LUTs, and minimizing the node count is imperative to meet resource constraints. Second, in area-oriented design space exploration for standard-cell designs, collapsing a circuit into a LUT network, restructuring it, and later remapping to the original representation helps escape local minima. Thus, the development of algorithms for optimizing and restructuring LUT networks holds considerable promise for area-oriented optimization. Substitution (also called resubstitution) is a powerful logic minimization method that can identify non-local logic dependencies and exploit them for logic minimization. State-of-the-art substitution algorithms for LUT networks rely heavily on SAT solving, limiting the number of optimization attempts and the size of the substitution sub-networks to one node mishchenko2011scalable. Conversely, our method relies on circuit simulation to increase the number of substitution candidates and enables substitutions with more than one node. The experimental results show that the proposed method identifies optimization opportunities overlooked by other methods, improving 11 out of 23 best-known results in the EPFL synthesis competition and yielding a 3.46% area reduction compared to the state-of-the-art.

Approximate computing is an emerging paradigm for designing error-resilient applications. It reduces circuit area, power, and delay at the cost of introducing errors. This article proposes a powerful technique, termed approximate resubstitution (AppResub), to approximately simplify the circuit. AppResub replaces a node’s function with a simpler approximate function on existing nodes in the circuit to reduce the hardware cost. Leveraging AppResub, an efficient flow for approximate logic synthesis (ALS) is developed by iteratively applying a set of promising AppResubs for circuit simplification. To evaluate errors caused by a set of AppResubs, a novel error model capable of efficiently computing an error upper bound is used to smartly apply AppResubs in the ALS flow. The experimental results demonstrate that compared to a state-of-the-art method, the proposed flow further reduces 20.9% area and 21.7% delay under the mean error distance constraint, while being$400\times $faster. The code of our flow is open-source.

Sequential logic synthesis can provide better Power-Performance-Area (PPA) than combinational logic synthesis since it explores a larger solution space. As the gate cost in advanced technologies keeps rising, sequential logic synthesis provides a powerful alternative that is gaining momentum in the EDA community. In this work, we present a new scalable algorithm for don't-care-based sequential logic synthesis. Our new approach is based on sequential k-step induction and can apply both redundancy removal and resubstitution transformations under Sequential Observability Don't Cares (SODCs). Using SODC-based optimizations with induction is a challenging problem due to dependencies and alignment of don't cares among the base case and the inductive case. We propose a new approach utilizing the full power of SODCs without limiting the solution space. Our algorithm is implemented as part of an industrial tool and achieves a 6.9% average area improvement after technology mapping when compared to state-of-the-art sequential synthesis methods. Moreover, all the new sequential optimizations can be verified using state-of-the-art sequential verification tools.

Many EDA applications deal with logic functions representing complex mathematical computations. Although in many cases, these functions depend on a small number of inputs, they often resemble random functions, making it hard to synthesize them using the traditional methods based on SOP minimization. This paper describes efficient synthesis and LUT mapping for this class of functions using a novel method that implements BDD-based minimization based on truth tables. The paper also investigates optimization with don't cares, when the outputs of a function are unspecified for some inputs, which is particularly useful in machine learning applications that trade accuracy for area. Compared to optimization and mapping used in academic and industrial tools, our method works faster and results in 1.5x smaller networks, while extra 20% area reduction was possible with don't cares at almost no accuracy cost.

Logic synthesis is an ensemble of algorithms that optimizes digital circuit representations and maps them to a chosen technology. Minimizing the number of gates is essential to reduce area occupation and power consumption. As the problem is intractable, heuristic logic transformations are used. In particular, resubstitution attempts to express the function of a node using other nodes already present in the network. State-of-the-art resubstitution engines can only identify new implementations with support of up to three inputs or being simply decomposable. This work aims at extending resubstitution to non-decomposable functions with more than three inputs and it outperforms previous methods. We apply our method on highly optimized designs from the ISCAS and EPFL benchmarks, achieving additional average improvements of 18.50% and 8.36%.

Modern logic synthesis techniques use multi-level technology-independent representations like And-Inverter-Graphs (AIGs) for digital logic. This involves structural rewriting, resubstitution, and refactoring based on directed-acyclic-graph (DAGs) traversal. Existing DAG-aware logic synthesis algorithms are designed to perform one specific optimization during a single DAG traversal. However, we empirically identify and demonstrate that these algorithms are limited in quality-of-results due to the solely considered optimization operation in the design concept. This work proposes Synthesis Orchestration, which is a fine-grained node-level optimization implying multiple optimizations during the single traversal of the graph. Our experimental results are comprehensively conducted on all 104 designs collected from ISCAS’85/89/99, VTR, and EPFL benchmark suites. The orchestration algorithms consistently outperform existing optimizations, rewriting, resubstitution, refactoring, leading to an average of 4% more node reduction with reasonable runtime cost for the single optimization. Moreover, we evaluate the orchestration algorithm in the sequential optimization, and as a plug-in algorithm in resyn and resyn3 flows in ABC, which demonstrate consistent logic minimization improvements (1%, 4.7% and 11.5% more node reduction on average). Finally, we integrate the orchestration into OpenROAD for end-to-end performance evaluations. Our results demonstrate the advantages of the orchestration optimization techniques, even after technology mapping and post-routing in the design flow.

Factored form is a powerful multi-level representation of a Boolean function that readily translates into an implementation of the function in CMOS technology. In particular, the number of literals in a factored form correlates strongly with the number of transistors in the CMOS implementation. This paper develops novel methods for optimizing factored forms while working on the efficient and-inverter graph (AIG) representation of combinational logic. This is in contrast to the traditional logic synthesis based on logic networks, and other AIG-based methods that minimize the AIG nodes count. Experiments show that applying these methods helps to reduce the area after technology mapping by an additional 2.8% on average, compared to a high-effort area-oriented baseline. It is expected that deploying these methods as part of an industrial standard-cell design flow will reduce design costs and power consumption. Additionally, this work enables efficient transistor-level logic synthesis of large designs with various applications in design automation.

Historically, open-source FPGA synthesis and technology mapping tools have been considered far inferior to industry-standard tools. We show that this is no longer true. Improvements in recent years to Yosys (Verilog elaborator) and ABC (technology mapper) have resulted in substantially better performance, evident in both the reduction of area utilization and the increase in the maximum achievable clock frequency. More specifically, we describe how ABC9 — a set of feature additions to ABC — was integrated into Yosys upstream and available in the latest version. Technology mapping now has a complete view of the circuit, including support for hard blocks (e.g., carry chains) and multiple clock domains for timing-aware mapping. We demonstrate how these improvements accumulate in dramatically better synthesis results, with Yosys-ABC9 reducing the delay gap from 30% to 0% on a commercial FPGA target for the commonly used VTR benchmark, thus matching Vivado's performance in terms of maximum clock frequency. We also measured the performance on a selection of circuits from OpenCores as well as literature, comparing the results produced by Vivado, Yosys-ABC1 (existing work), and the proposed Yosys-ABC9 integration.

The complexity of modern hardware designs necessitates advanced methodologies for optimizing and analyzing modern digital systems. In recent times, machine learning (ML) methodologies have emerged as potent instruments for assessing design quality-of-results at the Register-Transfer Level (RTL) or Boolean level, aiming to expedite design exploration of advanced RTL configurations. In this presentation, we introduce an innovative open-source framework that translates RTL designs into graph representation foundations, which can be seamlessly integrated with the PyTorch Geometric graph learning platform. Furthermore, the Verilog-to-PyG (V2PYG) framework is compatible with the open-source Electronic Design Automation (EDA) toolchain OpenROAD, facilitating the collection of labeled datasets in an utterly open-source manner. Additionally, we will present novel RTL data augmentation methods (incorporated in our framework) that enable functional equivalent design augmentation for the construction of an extensive graph-based RTL design database. Lastly, we will showcase several using cases of V2PYG with detailed scripting examples. V2PYG can be found at https://yu-maryland.github.io/Verilog-to-PyG/.

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.

The paper presents a novel DAG-aware Boolean rewriting algorithm for restructuring combinational logic before technology mapping. The algorithm, called window rewriting, repeatedly selects small parts of the logic and replaces them with more compact implementations. Window rewriting combines small-scale windowing with a fast heuristic Boolean resynthesis. The former uses sophisticated structural analysis to capture reconvergent paths in a multi-output window. The latter re-expresses the multi-output Boolean function of the window using fewer gates if possible. Experiments on the EPFL benchmarks show that a single iteration of window rewriting outperforms state-of-the-art AIG rewriting repeated until convergence in both quality and runtime.

LUT-based optimization techniques are finding new applications in synthesis of ASIC designs. Intuitively, packing logic into LUTs provides a better balance between functionality and structure in logic optimization. On this basis, the LUT-engine framework [1] was introduced to enhance the ASIC synthesis. In this paper, we present key improvements, at both algorithmic and flow levels, making a much stronger LUT-engine. We restructure the flow of LUT-engine, to benefit from a heterogeneous mixture of LUT sizes, and revisit its requirements for maximum scalability. We propose a dedicated LUT mapper for the new flow, based on FlowMap, natively balancing LUT-count and NAND2-count for a wide range LUT sizes. We describe a specialized Boolean factoring technique, exploiting the fanin bounds in LUT networks, resulting in a very fast LUT-based AIG minimization. By using the proposed methodology, we improve 9 of the best area results in the ongoing EPFL synthesis competition. Integrated in a complete EDA flow for ASICs, the new LUT-engine performs well on a set of 87 benchmarks: -4.60% area and -3.41% switching power at +5% runtime, compared to the baseline flow without LUT-based optimizations, and -3.02% area and -2.54% switching power with -1% runtime, compared to the original LUT-engine.

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

Look-up Table (LUT) mapping and optimization is an important step in Field Programmable Gate Arrays (FPGAs) design. The effectiveness of LUT synthesis improved dramatically in the last decades, thanks to optimization and mapping innovations naturally tailored for FPGAs. In this paper, we develop a new LUT-based optimization flow that is tailored for the synthesis of Application-Specific Integrated Circuits (ASICs) rather than FPGAs. We enhance LUT mapping to consider the literal/AIG cost of LUT nodes. We extend traditional Boolean methods to simplify and re-shape LUT-networks, targeting the best AIG/mapped-network implementation, after decomposition. Intuitively, literal-driven LUT packing behaves as a powerful fanin-bound node elimination, unveiling higher-order Boolean simplification opportunities. We embed our proposed LUT-based optimization flow, area oriented, in a commercial synthesis tool. Using our methodology, we improve 12 of the best area results in the EPFL synthesis competition. Employed in a commercial EDA flow for ASICs, our LUT optimization reduces area by 1.80%, total negative slack by 0.39%, and switching power by 1.72%, after physical implementation, at 5% runtime cost.

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.

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.

Most logic synthesis algorithms work on graph representations of logic functions with nodes associated with arbitrary logic expressions or simple logic functions and iteratively optimize such graphs. While recent multilevel logic synthesis efforts focused primarily on graphs with 2-input nodes such as AND and OR gates, the recently proposed paradigm of Majority-Inverter Graphs (MIGs) instead uses the 3-input Majority gate as the node function. As this technique proved to be a success, it is natural to ask: are there other 3-input gates better suited for logic synthesis? Motivated by this question, we investigate the relative advantages of 3-input gates as constituents of logic networks. We consider representative gates from each of the ten nondegenerate 3-input NPN classes and study how powerful they are at representing Boolean functions. Using SAT-based exact synthesis, we evaluate each 3-input gate using the minimum number of such gates (together with inverters) needed to synthesize all 4-input Boolean functions and a subset of frequent 5-input and 6-input Boolean functions. We show that the logic gate Dot(x,y,z) \mathrel \mathrel \mathop:= x ⊕(z Vxy) outperforms the rest in terms of expressive power. We further confirm this observation by showing that Dot-Inverter Graph representations are more than 14% smaller as compared to MIG representations of EPFL benchmarks.

SAT-sweeping is a powerful method for simplifying logic networks. It consists of merging gates that are proven equivalent (up to complementation) by running simulation and SAT solving in synergy. SAT-sweeping is used in both verification and synthesis applications within EDA. In this paper, we focus on the development of a highly efficient, synthesis-oriented, SAT-sweeping engine. We introduce a new algorithm to guide initial simulation, which strongly reduces the number of false candidates for merge, thus increasing the computational efficiency of the sweeper. We revisit the SAT-sweeping flow in light of practical considerations for synthesis, with the aim of proving all valid merges and ensuring fast execution. Experimental results confirm remarkable speedup deriving from our methodology, up to 10× for large combinational networks, and better QoR as compared to previous SAT-sweeping implementation. Embedded in a commercial synthesis flow, our proposes SAT-sweeper enables area and power savings of 1.98% and 1.81%, respectively, with neutral timing at negligible runtime overhead, over 36 testcases.

Approximate computing is an emerging design technique for error-resilient applications. It improves circuit area, power, and delay at the cost of introducing some errors. Approximate logic synthesis (ALS) is an automatic process to produce approximate circuits. This paper proposes approximate resubstitution with approximate care set and uses it to build a simulation-based ALS flow. The experimental results demonstrate that the proposed method saves 7%-18% area compared to state-of-the-art methods. The code of ALSRAC is made open-source.

We present a generic resynthesis framework for optimizing Boolean networks parameterized with a multi-level logic representation, a cut-computation algorithm, and a resynthesis algorithm. The framework allows us to realize powerful optimization algorithms in a plug-and-play fashion. We show the framework's versatility by composing an exact DAG-aware rewriting engine. Disjoint-support decomposition and SAT-based exact synthesis together with efficient caching strategies enable the algorithm to resynthesize larger parts of the logic. DAGaware rewriting is used to compute the gain of resynthesis while taking the benefit of structural hashing into account.

The focus of this paper is on intrinsic methods to detect overfitting. By intrinsic methods, we mean methods that rely only on the model and the training data, as opposed to traditional methods (we call them extrinsic methods) that rely on performance on a test set or on bounds from model complexity. We propose a family of intrinsic methods called Counterfactual Simulation (CFS) which analyze the flow of training examples through the model by identifying and perturbing rare patterns. By applying CFS to logic circuits we get a method that has no hyper-parameters and works uniformly across different types of models such as neural networks, random forests and lookup tables. Experimentally, CFS can separate models with different levels of overfit using only their logic circuit representations without any access to the high level structure. By comparing lookup tables, neural networks, and random forests using CFS, we get insight into why neural networks generalize. In particular, we find that stochastic gradient descent in neural nets does not lead to "brute force" memorization, but finds common patterns (whether we train with actual or randomized labels), and neural networks are not unlike forests in this regard. Finally, we identify a limitation with our proposal that makes it unsuitable in an adversarial setting, but points the way to future work on robust intrinsic methods.

NPN classification of Boolean functions is a powerful technique used in many practical applications, including logic synthesis, technology mapping, architecture exploration, circuit restructuring, and approximate logic synthesis. Computing the canonical form of a function is the most common approach to NPN classification. Exact classification of practical functions is an open problem because there are difficult functions beyond the capability of the state-of-the-art exact algorithms, which may take several months to compute a canonical form. This article proposes a new approach to exact NPN classification, in which a series of canonical forms and the algorithms to compute them are designed together. As a result, the runtime of the exact classification for difficult functions is effectively controlled by making both representation and computation cost-aware. Experimental results show that the proposed algorithm can perform exact classification of the worst-case 16-input functions in less than 3 minutes. This indicates that, for the first time, the problem of exact classification can be effectively solved for any Boolean functions with up to 16 inputs arising in practical applications.

Exact synthesis is a versatile logic synthesis technique with applications to logic optimization, technology mapping, synthesis for emerging technologies, and cryptography. In recent years, advances in SAT solving have led to a heightened research effort into SAT-based exact synthesis. Advantages of exact synthesis include the use of various constraints (e.g., synthesis of emerging technology circuits). However, although progress has been made, its runtime remains unpredictable. This paper identifies two key points as hurdles to further progress. First, there are open questions regarding the design and implementation of exact synthesis systems, due to the many degrees of freedom. For example, there are different CNF encodings, different symmetry breaks to choose from, and different encodings may be suitable for different domains. Second, SAT-based exact synthesis is difficult to parallelize. Indeed, this is a common drawback of logic synthesis algorithms. This paper proposes four ways to close some open questions and to reduce runtime: 1) quantifying differences between CNF encoding schemes and their impacts on runtime; 2) demonstrating impact of symmetry breaking constraints; 3) showing how directed acyclic graph topology information can be used to decrease runtime; and 4) showing how topology information can be used to leverage parallelism.

Combinational equivalence checking (CEC) has been widely applied to ensure design correctness after logic synthesis and technology-dependent optimization in digital integrated circuit design. CEC runtime is often critical for large designs, even when advanced techniques are employed. Three complementary ways for enabling parallelism in CEC are proposed, addressing different design and verification scenarios. The experimental results have demonstrated the speedups up to 63x when comparing the proposed approach to a single-threaded implementation of a similar CEC engine. A practical impact of such a speedup, for instance, is the runtime reduction from 19 h to only 18 min when checking equivalence of AND-inverter graphs comprising more than 20 million nodes. Therefore, the proposed solution presents great potential for improving current electronic design automation environments.

This paper proposes a novel methodology for multi-level logic synthesis that is independent from a specific graph data-structure, but formulates synthesis procedures using an abstract concept definition of a logic representation. The idea is to capture the essence of optimisations in a general manner and tailor only small performance-critical sections to the underlying logic representation. This generic, yet scalable approach, saves many man-months of development time and enables logic synthesis and technology-mapping procedures parameterised in a logic representation. We present the generic design methodology and demonstrate its practicality by providing a complete state-of-the-art logic synthesis flow.

The paper presents a generalization of DAG-aware AIG rewriting for k-feasible Boolean networks, whose nodes are k-input lookup tables (k-LUTs). We introduce a high-effort DAG-aware rewriting algorithm, called cut rewriting, which uses exact synthesis to compute replacements on the fly, with support for Boolean don't cares. Cut rewriting pre-computes a large number of possible replacement candidates, but instead of eagerly rewriting the Boolean network, stores the replacements in a conflict graph. Heuristic optimization is used to derive a best, maximal subset of replacements that can be simultaneously applied to the Boolean network from the conflict graph. We optimize LUT mapped Boolean networks obtained from the ISCAS and EPFL combinational benchmark suites. For 3-LUT networks, experiments show that we achieve an average size improvement of 5.58% and up to 40.19% after state-of-the-art Boolean rewriting techniques were applied until saturation. Similarly, for 4-LUT networks, we obtain an average improvement of 4.04% and up to 12.60%.

With the continuous push to improve Quality of Results (QoR) in EDA, Boolean methods in logic synthesis have been recently drawing the attention of researchers. Boolean methods achieve better QoR than algebraic methods but require higher computational cost. In this paper, we introduce the Scalable Boolean Method (SBM) framework. The SBM consists of 4 optimization engines designed to be scalable in a modern synthesis flow. The first presented engine is a generalized resubstitution framework based on computing, and implementing, the Boolean difference between two nodes. The second consists of a gradient-based AIG optimization, while the third one is based on heterogeneous elimination for kerneling. The last proposed engine is a revisiting of maximum set of permissible functions computation with BDDs. Altogether, the SBM framework enables significant synthesis results. We improve 12 of the best known area results in the EPFL synthesis competition. Embedded in a commercial EDA flow, the new Boolean methods enable -2.20% combinational area savings and -5.99% total negative slack reduction, after physical implementation, at contained runtime cost.

This paper presents a novel and effective logic synthesis flow able to identify threshold logic functions during the technology mapping process. It provides more efficient logic covering, exploring also redundant cuts. Moreover, the proposed design flow takes into account different circuit area estimations, such as the sum of input weights and threshold values, the gate fanin and the number of threshold logic gates. As a result, the mapped circuits present a reduction up to 47% and 67% in area and logic depth, respectively, in comparison to the most recent related approaches.

NPN classification of Boolean functions is a powerful technique used in many logic synthesis and technology mapping tools in both standard cell and FPGA design flows. Computing the canonical form is the most common approach of Boolean function classification. This article proposes two different hybrid NPN canonical forms and a new algorithm to compute them. By exploiting symmetries under different phase assignment as well as higher-order symmetries, the search space of NPN canonical form computation is pruned and the runtime is dramatically reduced. Nevertheless, the runtime for some difficult functions remains high. Fast heuristic method can be used for such functions to compute semi-canonical forms in a reasonable time. The proposed algorithm can be adjusted to be a slow exact algorithm or a fast heuristic algorithm with lower quality. For exact NPN classification, the proposed algorithm is 40× faster than state-of-the-art. For heuristic classification, the proposed algorithm has similar performance as state-of-the-art with a possibility to trade runtime for quality.

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

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

SAT based exact synthesis is a powerful technique, with applications in logic optimization, technology mapping, and synthesis for emerging technologies. However, its runtime behavior can be unpredictable and slow. In this paper, we propose to add a new type of constraint based on families of DAG topologies. Such families restrict the search space considerably and let us partition the synthesis problem in a natural way. Our approach shows significant reductions in runtime as compared to state-of-the-art implementations, by up to 63.43%. Moreover, our implementation has significantly fewer timeouts compared to baseline and reference implementations, and reduces this number by up to 61%. In fact, our topology based implementation dominates the others with respect to the number of solved instances: given a runtime bound, it solves at least as many instances as any other implementation.

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

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

FPGA performance depends in part on the choice of basic logic cell. Previous work dating back to 1999-2005 found that the best look-up table (LUT) sizes for area-delay product are 4-6, with 4 better for area and 6 for performance. Since that time several things have changed. A new 'LUT structure' mapping technique can target cells with a larger number of inputs (cut size) without assuming that the cell implements all possible functions of those inputs. We consider in particular a 7-input function composed of two tightly-coupled 4-input LUTs. Changes in process technology have increased the relative importance of wiring delay and configuration memory area. Finally, modern benchmark applications include carry chains, math and memory blocks. Due to these changes, we show that mapping to a 7-input LUT structure can approach the performance of 6-input LUTs while retaining the area and static power advantage of 4-input LUTs.

NPN classification of Boolean functions is a powerful technique used in many logic synthesis and technology mapping tools in FPGA design flows. Computing the canonical form of a function is the most common approach of Boolean function classification. In this paper, a novel algorithm for computing NPN canonical form is proposed. By exploiting symmetries under different phase assignments and higher-order symmetries of Boolean functions, the search space of NPN canonical form computation is pruned and the runtime is dramatically reduced. The algorithm can be adjusted to be a slow exact algorithm or a fast heuristic algorithm with lower quality. For exact classification, the proposed algorithm achieves a 30× speedup compared to a state-of-the-art algorithm. For heuristic classification, the proposed algorithm has similar performance as the state-of-the-art algorithm with a possibility to trade runtime for quality.

Parallel computing is a trend to enhance scalability of electronic design automation (EDA) tools using widely available multicore platforms. In order to benefit from parallelism, well-known EDA algorithms have to be reformulated and optimized for multicore implementation. This paper introduces a set of principles to enable a fine-grain parallel AND-inverter graph (AIG) rewriting. It presents a novel method to discover and rewrite in parallel parts of the AIG, without the need for graph partitioning. Experiments show that, when synthesizing large designs composed of millions of AIG nodes, the parallel rewriting on 40 physical cores is up to 36x and 68x faster than ABC commands rewrite −l and drw, respectively, with comparable quality of results in terms of AIG size and depth.

The paper describes a practical software tool for the verification of integer arithmetic circuits. It covers different types of integer multipliers, fused add-multiply circuits, and constant dividers - in general, circuits whose computation can be represented as a polynomial. The verification uses an algebraic model of the circuit and is accomplished by rewriting the polynomial of the binary encoding of the primary outputs (output signature), using the polynomial models of the logic gates, into a polynomial over the primary inputs (input signature). The resulting polynomial represents arithmetic function implemented by the circuit and hence can be used to extract functional specification from its gate-level implementation. The rewriting uses an efficient And-Inverter Graph (AIG) representation to enable extraction of the essential arithmetic components of the circuit. The tool is integrated with the popular ABC system. Its efficiency is illustrated with impressive results for integer multipliers, fused add-multiply circuits, and divide-by-constant circuits. The entire verification system is offered in an open source ABC environment together with an extensive set of benchmarks.

Detecting equivalence classes of injected faults for functional verification of electronic systems is an important task because it helps reducing the number of faults to qualify a verification environment, and hence, improves the performance of qualification process and the validation time required for large-scale electronic systems. This paper describes an efficient way of detecting equivalent injected faults in a mapped netlist in order to speedup the qualification process of a verification environment for functional safety. The presented fault models include general faults resulting in arbitrary functional changes, in addition to conventional stuck-at faults. The solution is based on structural pruning and functional analysis performed by a synergistic combination of iterative Boolean satisfiability and guided simulation. It should be noted that traditional brute-force-like methods would take many hours or even days to identify thousands of equivalent functional faults injected to a small circuit with only hundred of cells. The proposed approach can achieve excellent fault reduction ratios within few seconds for such small circuits. The implementation also scales well for the largest ISCAS'89 and OpenCores benchmarks containing over 35K gates and 490K general functional faults.

Constructing algebraic polynomials using computer algebra techniques is believed to be state-of-the-art in analyzing gate-level arithmetic circuits. However, the existing approach applies algebraic rewriting directly to the gate-level netlist, which has potential memory explosion problem. This paper introduces an algebraic rewriting technique based on the and-inverter graph (AIG) representation of gate-level designs. Using AIG-based cut-enumeration and truth table computation, an efficient order of algebraic rewriting is identified, resulting in dramatic simplifications of the polynomial under construction. An automatic approach, which further reduces the complexity of algebraic rewriting by handling redundant polynomials, is also proposed.

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

Boolean SAT solving can be used to find a minimum-size logic network for a given small Boolean function. This paper extends the SAT formulation to find a minimum-size network under delay constraints. Delay constraints are given in terms of input arrival times and the maximum depth. After integration into a depth-optimizing mapping algorithm, the proposed SAT formulation can be used to perform logic rewriting to reduce the logic depth of a network. It is shown that to be effective the logic rewriting algorithm requires (i) a fast SAT formulation and (ii) heuristics to quickly determine whether the given delay constraints are feasible for a given function. The proposed algorithm is more versatile than previous algorithms, which is confirmed by the experimental results.

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

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

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

Classifying functions according to some common properties into libraries of functions is an important step in many logic synthesis and technology mapping algorithms used in FPGA design flows. NPN classification is one of the frequently used classifications. Existing algorithms for NPN classification perform a sequence of steps to derive the resulting NPN class, but discard the intermediate results produced at the end of each step. The hierarchical method introduced in this paper uses the same sequence of steps, but it saves the intermediate results at each step and reuses them when classifying other functions. It is, on average, 3.7 times faster compared to a state-of-the-art non-hierarchical method, at the cost of a modest increase in memory needed to save the class hierarchy. The hierarchical approach enables a rapid exact NPN classification for functions up to 10 inputs-it exactly classifies one million 6-input functions in the same time as the heuristic state-of-the-art algorithm.

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

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

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

Carry chains facilitate the implementation of adders and improve the performance of arithmetic circuits in FPGAs. The last version of the commonly used open-source Verilog-to-Routing (VTR) CAD flow now enables modelling carry chains in FPGA architectures. However, one of the shortcomings of the existing flow lies in its inability to identify arithmetic operations when described as gate-level circuits. Moreover, the VTR flow squanders most of the LUTs preceding the chain logic. This paper focuses on these two problems and proposes preprocessing the circuit before technology mapping to allow for a more efficient use of carry chains. The first proposed method maps logic on the carry chains for circuits expressed using a gate-level description. On average, it identifies about 30% more meaningful full adders than the existing tool flow operating on the RTL descriptions. Area is thus improved by up to 15% with an average of 6% for almost no delay penalty. Secondly, we increase the use of the LUTs preceding the chain logic by a factor 2 on average. This reduces delay (up to 9%) and area (up to 2%), compared to the existing VTR flow. The new approach is independent of the specific carry-chain architecture and can be generically adapted to any FPGA with built-in hardened adders.

This paper presents a novel approach to synthesize circuits based on threshold logic gates (TLGs). Emerging technologies, such as memristors, spintronics devices and tunneling diodes, are able to build this class of gates efficiently. For this reason, threshold logic is a promising alternative to conventional CMOS logic. The proposed approach is based on pruning non-threshold-logic cuts in order to limit the search space during technology mapping. As a result, both the number of TLGs and logic depth of the synthesized circuits are reduced. Experimental results have shown that, compared to the state-of-the-art methods, the TLG count is reduced by 8% and logic depth is reduced by 46%.

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

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

Craig interpolation is a known method for expressing a target function f as a function of a given set of base functions G. The resulting interpolant represents the dependency function h, such that f = h(G). Generally, the set G contains enough base functions to enable the existence of multiple dependency functions whose quality mainly depends on which base functions were selected for reconstruction. The interpolation is not an optimisation problem and thus, often, it selects some random base functions and, particularly, omits others potentially required for an optimal implementation of the target function. Mainly, it is impossible to impose that the interpolant uses a specific base function. In this paper, we propose a method that forces a specific base function gias a primary input of a dependency function. Such a dependency function is built as a Shannon expansion of two constrained Craig interpolants for the assignments of the primary inputs for which gievaluates to 0 and 1, respectively. We also introduce a method that iteratively imposes a predefined set of base functions. In each iteration, we generate a new dependency function for use as the target function of the next iteration in order to force the use of a base function. We show that, unlike the standard Craig interpolation method, our carving method succeeds to impose the desired base functions with very high probability. It recomposes single-output logic circuits as their delay- or area-optimised implementations regardless of the input implementation. The proposed methods can be efficiently employed for rewriting circuits in some synthesis-based algorithms.

Due to the continuous shrinking of semiconductor technology, there are more and more subtle errors or faults widely distributed in manufactured chips, and traditional “single” stuck-at fault model may become inappropriate. It is definitely better if all combinations of multiple faults can be completely tested. In this paper, we present ATPG (Automatic Test Pattern Generation) techniques targeting all multiple stuck-at faults, i.e. all combinations of stuck-at faults. That is, given “n” possibly faulty locations in a circuit, the target set of faults consists of 3n- 1 fault combinations, as each possibly faulty location is under stuck-at 1, stuck-at 0, or normal/non-faulty. Traditional ATPG flows use fault simulators to eliminate all detectable faults by the current set of test vectors. The problem, however, fault simulators represent fault lists explicitly in the sense that all possible faults are enumerated in the fault lists. This prevents us from dealing with ultra large fault lists, such as 3n- 1 faults. We need “implicit” representation of faults in order to deal with such huge numbers of faults or fault combinations. We present SAT based formulations for ATPG of circuits having very large numbers of faults by implicitly eliminating detected faults. We solve a set of SAT problems whose constraints increase pure incrementally (here “pure” means never deleting constraints), and so the entire solving process can be very efficient, as all learnings obtained so far are valid in the following SAT problems. Experiments are performed on combinational parts of ISCAS89 circuits in their AIG (AND-Inverter Graph) representations. We have successfully generated the complete set of test vectors assuming that faults happen only at outputs of gates. Our ATPG techniques can also start with a given set of test vectors. If we start the ATPG processes with a set of test vectors for single stuck-at faults, we can obtain the set of additional test vectors required for multiple stuck-at faults. Results are a little bit surprising in the sense that we need very few additional test vectors for multiple faults, although the numbers of fault combinations are exponentially larger. As far as we know, for the first time, complete test vectors for all stuck-at faults for ISCAS89 circuits where faults happen only at outputs of gates in AIG representations of the circuits have been obtained.

We discuss about logic synthesis and formal verification of combinational circuits mapped to a given fixed topology. Here “fixed topology” means that circuit structures in terms of net lists except for gate/cell types are fixed in advance. That is, for logic synthesis, what should be generated are the types of gates/cells (or simply gates) in the circuits, and all the others are prefixed before synthesis. As the circuit topology is fixed in advance, placement and routing could be shared among different designs and minimum ECO can be realized by keeping the same layout. Also, we can show that we do not need many test vectors in order to guarantee 100% correctness of such synthesis. Small numbers of test vectors, such as only 100 test vectors for 30 input circuits, are sufficient to test if the circuits behave correctly for all possible input value combinations. That is, very efficient formal verification can be realized through simulations with small numbers of test vectors. We present SAT based implementation of the synthesis and a test vector generation method with preliminary but encouraging experimental results.

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

Automatic abstraction is an important component of modern formal verification flows. A number of effective SAT-based automatic abstraction methods use unsatisfiable cores to guide the construction of abstractions. In this paper we analyze the impact of unsatisfiable core minimization, using state-of-the-art algorithms for the computation of minimally unsatisfiable subformulas (MUSes), on the effectiveness of a hybrid (counterexample-based and proof-based) abstraction engine. We demonstrate empirically that core minimization can lead to a significant reduction in the total verification time, particularly on difficult testcases. However, the resulting abstractions are not necessarily smaller. We notice that by varying the minimization effort the abstraction size can be controlled in a non-trivial manner. Based on this observation, we achieve a further reduction in the total verification time.

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

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

This paper proposes a fast algorithm for Boolean matching of completely specified Boolean functions. The algorithm is based on the NPN classification and can be applied on-the-fly to millions of small practical functions appearing in industrial designs, leading to runtime and memory reduction in logic synthesis and technology mapping. The algorithm is conceptually simpler, faster, and more scalable than previous work.

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

Deriving a circuit for a Boolean function or improving an available circuit are typical tasks solved by logic synthesis. Numerous algorithms in this area have been proposed and implemented over the last 50 years. This paper presents a "lazy" approach to logic synthesis based on the following observations: (a) optimal or near-optimal circuits for many practical functions are already derived by the tools, making it unnecessary to implement new algorithms or even run the old ones repeatedly; (b) larger circuits are composed of smaller ones, which are often isomorphic up to a permutation/negation of inputs/outputs. Experiments confirm these observations. Moreover, a case-study shows that logic level minimization using lazy man's synthesis improves delay after LUT mapping into 4- and 6-input LUTs, compared to earlier work on high-effort delay optimization.

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

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

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

The paper introduces novel field programmable gate array (FPGA) circuits based on hybrid CMOS/resistive switching device (memristor) technology and explores several logic architectures. The novel FPGA structure is based on the combination of CMOL (Cmos + MOLecular scale devices) FPGA circuits and recent improvements and generalization of the CMOL concept to allow multilayer crossbar integration, compatibility with state-of-the-art foundries, and a wide range of available memristive crosspoint devices. Preliminary results indicate that with no optimization and only conventional CMOS technology, the proposed circuits can be at least ten times denser (and potentially faster) than CMOS FPGAs with the same design rules and similar power density. The second part of this paper shows that this performance can be further improved using optimal MUX-based logic architecture.

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

The ability to efficiently match logic functions to structures of K-input look-up tables (K-LUTs) is a central problem in FPGA resynthesis algorithms. This paper addresses the problem of matching logic functions of ~ 9 to 12 inputs to K-LUT structures. Our method is based on the off-line generation of libraries of LUT structures. During resynthesis, matching is accomplished efficiently using NPN encoding and hash table look-ups. Generating an effective library of LUT structures may seem prohibitive due to the overwhelming number of logic functions which must be considered and represented in the library. We show that, by careful consideration of which logic functions and LUT structures to keep, it is possible to generate useful, compact libraries. We present numerical results demonstrating the effectiveness of our ideas when used during area-oriented resynthesis after FPGA technology mapping.

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.

Traditional digital circuit synthesis flows start from an HDL behavioral definition and assume that circuit functions are almost completely defined, making don't-care conditions rare. However, recent design methodologies do not always satisfy these assumptions. For instance, third-party IP blocks used in a system-on-chip are often overdesigned for the requirements at hand. By focusing only on the input combinations occurring in a specific application, one could resynthesize the system to greatly reduce its area and power consumption. Therefore we extend modern digital synthesis with a novel technique, called SWEDE, that makes use of extensive external don't-cares. In addition, we utilize such don't-cares present implicitly in existing simulation-based verification environments for circuit customization. Experiments indicate that SWEDE scales to large ICs with half-million input vectors and handles practical cases well.

This paper uses under-approximation of unreachable states of a design to derive incomplete specification of combinational logic. The resulting incompletely-specified functions are decomposed to enhance the quality of technology-dependent synthesis. The decomposition choices are computed implicitly using novel formulation of symbolic bi-decomposition that is applied recursively to decompose logic in terms of simple primitives. The ability of BDDs to represent compactly certain exponentially large combinatorial sets helps us to implicitly enumerate and explore variety of decomposition choices improving quality of synthesized circuits. Benefits of the symbolic technique are demonstrated in sequential synthesis of publicly available benchmarks as well as on the realistic industrial designs.

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

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

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

This article presents a new technology mapper, WireMap. The mapper uses an edge flow heuristic to improve the routability of a mapped design. The heuristic is applied during the iterative mapping optimization to reduce the total number of pin-to-pin connections (or edges). On academic benchmark (ISCAS, MCNC, and ITC designs), the average edge reduction of 9.3% is achieved while maintaining depth and LUT count compared to state-of-the-art technology mapping. Placing and routing the resulting netlists leads to an 8.5% reduction in the total wirelength, a 6.0% reduction in minimum channel width, and a 2.3% reduction in critical path delay. This technique is applied in the Xilinx ISE Design tool to evaluate its effect on industrial Virtex5 circuits. In a set of 20 large designs, we find the edge reduction is 6.8% while total wirelength measured in the placer is reduced by 3.6%. Applying WireMap has an additional advantage of reducing an average number of inputs of LUTs without increasing the total LUT count and depth. The percentages of 5- and 6-LUTs in a typical design are reduced, while the percentages of 2-, 3-, and 4-LUTs are increased. These smaller LUTs can be merged into pairs and implemented using the dual-output LUT structure found in commercial FPGAs. For academic benchmarks, WireMap leads to 9.4% fewer dual-output LUTs after merging. For the industrial designs, WireMap leads to 6.3% fewer dual-output Virtex5 LUTs.

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

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

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

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

This paper presents a new technology mapper, WireMap. The mapper uses an edge flow heuristic to improve the routability of a mapped design. The heuristic is applied during the iterative mapping optimization to reduce the total number of pin-to-pin connections (or edges). The average edge reduction of 9.3% is achieved while maintaining depth and LUT count of state-of-the-art technology mapping. Placing and routing the resulting netlists leads to an 8.5% reduction in the total wire length, a 6.0% reduction in minimum channel width, and a 2.3% reduction in critical path delay. Applying WireMap has an additional advantage of reducing an average number of inputs of LUTs without increasing the total LUT count and depth. The percentages of 5- and 6-LUTs in a typical design are reduced, while the percentages of 2-, 3-, and 4-LUTs are increased. These smaller LUTs can be merged into pairs and implemented using the dual output LUT structure found in commercial FPGAs. WireMap leads to 9.4% fewer dual-output LUTs after merging

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

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

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

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

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

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.

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

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

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

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

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

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

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

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

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

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

This paper describes linear cofactor relationships (LCRs), which are defined as the exclusive sums of cofactors with respect to a pair of variables in Boolean functions. These relationships subsume classical symmetries and single-variable symmetries. The paper proposes an efficient algorithm to detect LCRs and discusses their potential applications in Boolean matching, minimization of decision diagrams, synthesis of regular layout-friendly logic circuits, and detection of support-reducing bound sets

Detecting support-reducing bound sets is an important step in Boolean decomposition. It affects both the quality and the runtime of several applications in technology mapping and re-synthesis. This paper presents an efficient heuristic method for detecting support-reducing bound sets using two-cofactor symmetries. Experiments on the MCNC and ITC benchmarks show an average 40x speedup over the published exhaustive method for bound set construction.

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

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

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

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.

In some cases, minimum Sum-Of-Products (SOP) expressions of Boolean functions can be derived by detecting decomposition and observing the functional properties such as unateness, instead of applying the classical minimization algorithms. This paper presents a systematic study of such situations and develops a divide-and-conquer algorithm for SOP minimization, which can dramatically reduce the computational effort, without sacrificing the minimality of the solutions. The algorithm is used as a preprocessor to a general-purpose exact or heuristic minimizer, such as ESPRESSO. The experimental results show significant improvements in runtime. The exact solutions for some large MCNC benchmark functions are reported for the first time.

Structuring and mapping of a Boolean function is an important problem in the design of complex integrated circuits. Library-aware constructive decomposition offers a solution to this problem. This paper proposes novel techniques to improve the quality and runtime of constructive decomposition. The improvements are effective both in the stand-alone mapping procedure and in the context of re-synthesis applied to a mapped multi-level network. Experiments with public and proprietary benchmarks show promising results.

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

Symmetry detection in completely specified Boolean functions is important for several applications in logic synthesis, technology mapping, binary decision diagram (BDD) minimization, and testing. This paper presents a new algorithm to detect four basic types of two-variable symmetries. The algorithm detects all pairs of symmetric variables in one pass over the shared BDD of the multioutput function. The worst case complexity of this method is cubic in the number of BDD nodes, but on typical logic synthesis benchmarks the complexity appears to be linear. The computation is particularly efficient when the functions have multiple symmetries or no symmetries. Experiments show that the algorithm is faster than other known methods, and in some cases achieves a speedup of several orders of magnitude.

This paper presents a satisfiability-based method for solving the board-level multiterminal net routing problem in the digital design of clos-folded field-programmable gate array (FPGA) based logic emulation systems. The approach transforms the FPGA board-level routing task into a Boolean equation. Any assignment of input variables that satisfies the equation specifies a valid routing. We use two of the fastest Boolean satisfiability (SAT) solvers: Chaff and DLMSAT to perform our experiments. Empirical results show that the method is time-efficient and applicable to large layout problem instances.

The paper presents a satisfiability-based method for solving the board-level multiterminal net routing problem in Clos-Folded FPGA based logic emulation systems. The approach transforms the FPGA board-level routing task into a single, large Boolean equation with the property that any assignment of input variables that satisfies the equation specifies a valid routing. The approach considers all nets simultaneously and the absence of a satisfying assignment implies that the layout is unroutable. We use two of the fastest SAT solvers: Chaff and DLM to perform our experiments. Empirical results show that the method is time-efficient and applicable to large layout problem instances.

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

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

We propose a new BDD-based method for decomposition of multi-output incompletely specified logic functions into netlists of two-input logic gates. The algorithm uses the internal don't-cares during the decomposition to produce compact well-balanced netlists with short delay. The resulting netlists are provably non-redundant and facilitate test pattern generation. Experimental results over MCNC benchmarks show that our approach outperforms SIS and other BDD-based decomposition methods in terms of area and delay of the resulting circuits with comparable CPU time.

Reversible logic is of increasing importance to many future computer technologies. We introduce a regular structure to realize symmetric functions in binary reversible logic. This structure, called a 2*2 net structure, allows for a more efficient realization of symmetric functions than the methods introduced by the other authors. Our synthesis method allows us to realize arbitrary symmetric function in a completely regular structure of reversible gates with relatively little "garbage". Because every Boolean function can be made symmetric by repeating input variables, our method is applicable to arbitrary multi-input multi-output Boolean functions and realizes such arbitrary function in a circuit with a relatively small number of additional gate outputs. The method can also be used in classical logic. Its advantages in terms of numbers of gates and inputs/outputs are especially seen for symmetric or incompletely specified functions with many outputs.

Finding the minimum column multiplicity for a bound set of variables is an important problem in Curtis decomposi-tion. To investigate this problem, we compared two graph-coloring programs: one exact, and another one based on heuristics which can give, however, provably exact results on some types of graphs. These programs were incorporated into the multi-valued decomposer MVGUD. We proved that the exact graph coloring is not necessary for high-quality functional decomposers. Thus we improved by orders of magnitude the speed of the column multiplicity problem, with very little or no sacrifice of decomposition quality. Comparison of our experimental results with competing de-composers shows that for nearly all benchmarks our solu-tions are best and time is usually not too high.