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.

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 paper 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 area reduction of 2.20 improves 4 of the best delay results in the EPFL synthesis competition without employing design-space exploration techniques.

When synthesizing hardware designs, the frontend of a synthesis tool often elaborates control logic as multiplexers and selectors, which are next bit-blasted into simple gates and processed by a logic synthesis flow. This approach may lead to suboptimal results or take a prohibitive runtime to synthesize optimally. The present paper focuses on a specialized logic synthesis method applied to a word-level view of the control logic after elaboration before bit-blasting, or to the control logic extracted from a netlist after bit-blasting. The method detects clock-enables and other types of shared logic, resulting in substantially reduced area and delay, at a negligible 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.

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.

In this work, a CODEC design to eliminate/reduce the propagation delay across long on chip buses which are increasingly becoming a limiting factor in high-speed design has been proposed. Crosstalk between adjacent wires are transitioning in opposite direction create a significant portion of this delay. The coding scheme is based on the Fibonacci numeral system. The proposed CODEC design is efficient and a modular technique. Encoding and decoding algorithms are proposed for three different Fibonacci techniques. The experimental results show that the proposed CODEC reduces crosstalk delay when compared to that of existing approaches. The implementation has been done in verilog code. These codes were synthesized and verified using Cadence Encounter RTL compiler tool with geometries at

This paper proposes a new logic optimization paradigm based on circuit simulation, which reduces the need for Boolean computations such as SAT-solving or constructing BDDs. The paper develops a Boolean resubstitution framework to demonstrate the effectiveness of the proposed approach. Methods to generate highly expressive simulation patterns are developed, and the generated patterns are used in resubstitution for efficient filtering of potential resubstitution candidates to reduce the need for SAT validation. Experimental results show that improvements in circuit size reduction were achieved by up to 74%, compared to a state-of-the-art resubstitution algorithm.

This session presents recent progress in logic synthesis and technology mapping. The first paper discusses improvements to Boolean resynthesis using a theory on Boolean filtering and a more general notion of permissible functions. The second paper applies methods based on Boolean relations for the optimization of combinational logic networks. The third paper proposes a technology mapping approach for silicon nanowire reconfigurable FETs. The fourth paper presents for the first time an approximate synthesis methods for threshold logic circuits through an iterative approach that guarantees an error bound.

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

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

A representation of a Boolean function is canonical if, given a variable order, only one instance of the representation is possible for the function. A computation is canonical if the result depends only on the Boolean function and a variable order, and does not depend on how the function is represented and how the computation is implemented.In the context of Boolean satisfiability (SAT), canonicity of the computation implies that the result (a satisfying assignment for satisfiable instances and an abstraction of the unsat core for unsatisfiable instances) does not depend on the functional representation and the SAT solver used.This paper shows that SAT-based computations can be made canonical, even though the SAT solver is not using a canonical data structure. This brings advantages in EDA applications, such as irredundant sum of product (ISOP) computation, counter-example minimization, etc, where the uniqueness of solutions and/or improved quality of results justify a runtime overhead.

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.

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.

In this paper, we discuss recent advances in exact synthesis, considering both their efficient implementation and various applications in which they can be employed. We emphasize on solving exact synthesis through Boolean satisfiability (SAT) encodings. Different SAT encodings for exact synthesis are compared, and examined the applications to multi-level logic synthesis, in both area and depth optimization. Another application of SAT based exact synthesis is optimization under many constraints. These constraints can, e.g., be a fixed fanout or delay constraints. Finally, we end our discussion by proposing directions for future research in exact synthesis.

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.

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.

We survey some of the methods usedfor manipulating, representing, and optimizing multi-valued logic with the view of both building a better understanding of the more specialized binary-valued logic, as well as motivating re search towards a true multi-valued multi-level optimization package.

We introduce a scheme to simplify a multi-valued network using redundancy removal techniques. Recent methods [1], [2] for binary redundancy removal avoid the use of state traversal. Additionally, [2] finds multiple compatible redundancies simultaneously. We extend these powerful advances in the field ofbinary redundancy removal to perform redundancy removal for multi-valued networks. First we perform a one-hot encoding of all the multi-valued variables of the design. Multi-valued variables are written out as binary variables, using this one-hot encoding. At the end of this step, we have a binary network which is equivalent to the multi-valued network modulo encoding. Next, binary redundancy removal is invoked on the resulting network. In case a binary signal Siis determined to be stuck-at-0 redundant, this means that the multi-valued signal s can never take on a value i. Further, if the binary signal Si is determined to be stuck-at-1 redundant, this means that the multi-valued signal s takes on a constant value i. All redundant binary signals are recorded in a file. The original multi-valued network is modified based on the binary redundancies thus computed. *CAD Research Group, Department of Electrical Engineering and Computer Sciences, University of Califomia, Berkeley, CA 94720. This research was funded under the Semiconductor Research Corporation Grant SRC-324-040. Initial experiments using this technique show a10-20% reduction in the size of the multi-valued description.