During technology mapping, complex cells such as adders and multiplexers are often available in the standard cell library, which helps improve the final PPA results. However, technology-independent optimization tends to over-optimize towards the cost metrics measurable with technology-independent representations (e.g., AIG size) by decomposing blocks of logic that could have been mapped into complex cells. Besides, it is also of practical interest to model and preserve some special logic components, such as the enable logic of flops, during optimization. This paper studies “boxing” logic blocks before technology-independent optimization and preserving them during optimization. A wire-based resubstitution is proposed to optimize boxed networks. Experiments with academic and industrial benchmarks show that transparent-boxing, i.e., preserving boxes while utilizing the information on their logic, achieves better results than black-boxing, i.e., completely ignoring the logic in boxes. Specifically, in the technology-independent evaluation, transparentboxing reduces the mapped network size by 4% more than blackboxing; in the full-flow evaluation, transparent-boxing achieves 1.8% more improvement on timing and similar improvements in area, power, and wire length compared to black-boxing.

Adiabatic quantum-flux parametron (AQFP) is an energy-efficient superconducting technology. Before physical design can be performed, AQFP technology mapping involves not only mapping logic into supported gate types but also legalizing the circuit to fulfill the technology-imposed constraints on path balancing and fanout branching by inserting buffer and splitter cells. These cells account for a significant amount of the circuit’s area, delay, as well as for increasing energy consumption. In this paper, we (a) identify that the AQFP legalization problem is a scheduling problem; (b) propose linear-time depth-optimal scheduling and irredundant buffer insertion algorithms; (c) present heuristic optimization algorithms to further reduce buffer count; and (d) suggest an unsupervised design space exploration approach for AQFP technology mapping, mixing and interleaving logic optimization and technology legalization. Experimental results show that our design space exploration, utilizing the proposed technology legalization and optimization flow, achieves 44% improvement on the energy-delay product compared to the state of the art.

The majority-inverter graph (MIG) is a homogeneous logic network widely used in logic synthesis for majority-based emerging technologies. Many logic optimization algorithms have been proposed for MIGs, including rewriting, resubstitution, and graph mapping. However, unlike AIGs, research on optimization flows for MIGs is limited. In this paper, we explore combinations of well-developed MIG optimization algorithms using an on-the-fly design space exploration strategy and present the latest best results on MIG size minimization of EPFL benchmarks. Significant reductions (of 88% and 79%) are observed for two specific benchmarks and an average of 14% improvement is achieved compared to the state-of-the-art flow.

Individual transistors based on emerging reconfigurable nanotechnologies exhibit electrical conduction for both types of charge carriers. These transistors [referred to as reconfigurable field-effect transistors (RFETs)] enable dynamic reconfiguration to demonstrate either a p- or an n-type functionality. This duality of functionality at the transistor level is efficiently abstracted as a self-dual Boolean logic, that can be physically realized with fewer RFET transistors compared to the contemporary CMOS technology. Consequently, to achieve better area reduction for RFET-based circuits, the self-duality of a given circuit should be preserved during logic optimization and technology mapping. In this article, we specifically aim to preserve self-duality by using Xor-majority graphs (XMGs) as the logic representation during logic synthesis and technology mapping. We propose a synthesis flow that uses new restructuring techniques, called rewriting and resubstitution for XMGs to preserve self-duality during technology-independent logic synthesis. For technology mapping, we use a novel open-source and a logic-representation agnostic mapping tool. Using the above-proposed XMG-based flow, we demonstrate its benefits by comparing post-mapping areas for synthetic and cryptographic benchmarks with three different synthesis flows: 1) AIG-based optimization and AIG-based mapping; 2) XMG-based optimization with AIG-based mapping; and 3) AIG-based optimization with logic-representation agnostic mapping. Our experiments show that the proposed XMG-based flow efficiently preserves self-duality and achieves the best area results for RFET-based circuits (up to 12.36% area reduction) with respect to the baseline.

This paper proposes a versatile mapping approach that has three objectives: i) it can map from one technology-independent graph representation to another; ii) it can map to a cell library; iii) it supports logic rewriting. The method is cut-based, mitigates logic-sharing issues of previous graph mapping approaches, and exploits structural hashing. The mapper is the first one of its kind to support remapping among various graph representations, thus enabling specialized mapping to emerging technologies (such as AQFP) and for security applications (such as XAG-based design). We show that mapping to MIGs improves area by 10% as compared to the state of the art, and that technology mapping is 18% faster than ABC with slightly better results.

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.

Adiabatic quantum-flux parametron (AQFP) is an energy-efficient superconducting technology. Buffer and splitter (B/S) cells must be inserted to an AQFP circuit to meet the technology-imposed constraints on path balancing and fanout branching. These cells account for a significant amount of the circuit's area and delay. In this paper, we identify that B/S insertion is a scheduling problem, and propose (a) a linear-time algorithm for locally optimal B/S insertion subject to a given schedule; (b) an SMT formulation to find the global optimum; and (c) an efficient heuristic for global B/S optimization. Experimental results show a reduction of 4% on the B/S cost and 124X speed-up compared to the state-of-the-art algorithm, and capability to scale to a magnitude larger benchmarks.

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.

Adiabatic quantum-flux-parametron (AQFP) circuits are a family of superconducting electronic (SCE) circuits that have recently gained growing interest due to their low-energy consumption, and may serve as alternative technology to overcome the down-scaling limitations of CMOS. AQFP logic design differs from classic digital design because logic cells are natively abstracted by the majority function, require data and clocking in specific timing windows, and have fan-out limitations. We describe here a novel majority-based logic synthesis flow addressing AQFP technology. In particular, we present both algebraic and Boolean methods over majority-inverter graphs (MIGs) aiming at optimizing size and depth of logic circuits. The technology limitations and constraints of the AQFP technology (e.g., path balancing and maximum fanout) are considered during optimization. The experimental results show that our flow reduces both size and depth of MIGs, while meeting the constraint of the AQFP technology. Further, we show an improvement for both area and delay when the MIGs are mapped into the AQFP technology.

Emerging reconfigurable nanotechnologies allow the implementation of self-dual functions with a fewer number of transistors as compared to traditional CMOS technologies. To achieve better area results for Reconfigurable Field-Effect Transistors (RFET)-based circuits, a large portion of a logic representation must be mapped to self-dual logic gates. This, in turn, depends upon how self-duality is preserved in the logic representation during logic optimization and technology mapping. In the present work, we develop Boolean size-optimization methods-a rewriting and a resubstitution algorithm using Xor-Majority Graphs (XMGs) as a logic representation aiming at better preserving self-duality during logic optimization. XMGs are more compact for both unate and binate logic functions as compared to conventional logic representations such as And-Inverter Graphs (AIGs) or Majority-Inverter Graphs (MIGs). We evaluate the proposed algorithm over crafted benchmarks (with various levels of self-duality) and cryptographic benchmarks. For cryptographic benchmarks with a high self-duality ratio, the XMG-based logic optimisation flow can achieve an area reduction of up to 17% when compared to AIG-based optimization flows implemented in the academic logic synthesis tool ABC.

We propose a flow for automated quantum compilation. Our flow takes a Boolean function implemented in Python as input and translates it into a format appropriate for reversible logic synthesis. We focus on two quantum compilation tasks: uniform state preparation and oracle synthesis. To illustrate the use of our flow, we solve IBM's virtual hackathon challenge of 2019, called the Zed city problem, an instance of vertex coloring, by using quantum search algorithms. The expressiveness of Python in combination with automated compilation algorithms allows us to express quantum algorithms at a high level of abstraction, which reduces the effort to implement them, and leads to better and more flexible implementations. We show that our proposed flow generates a lower-cost circuit implementation of the oracle needed to solve IBM's challenge when compared to the winning submission.

Logic resynthesis is the problem of finding a dependency function to re-express a given Boolean function in terms of a given set of divisor functions. In this paper, we study logic resynthesis of majority-based circuits, which is motivated by the increasing interest in majority logic optimization due to the recent development of beyond-CMOS technologies. To meet the need for an efficient majority resynthesis heuristic, we propose a top-down decomposition algorithm, whose complexity is linear to both n and m, where n is the number of divisors and m is the number of majority operations in the dependency function. We evaluate the resynthesis algorithms by using them in a resubstitution run applied on the EPFL benchmark suite. The experimental results show that, comparing to the state-of-the-art enumeration algorithm whose complexity grows exponentially with m, using the proposed decomposition Algorithm leads to 1.5% more circuit size reduction by lifting the limitation on m, within comparable runtime.

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.

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

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.

Logic synthesis is a fundamental step in the realization of modern integrated circuits. It has traditionally been employed for the optimization of CMOS-based designs, as well as for emerging technologies and quantum computing. Recently, it found application in minimizing the number of AND gates in cryptography benchmarks represented as xor-and graphs (XAGs). The number of AND gates in an XAG, which is called the logic network's multiplicative complexity, plays a critical role in various cryptography and security protocols such as fully homomorphic encryption (FHE) and secure multi-party computation (MPC). Further, the number of AND gates is also important to assess the degree of vulnerability of a Boolean function, and influences the cost of techniques to protect against side-channel attacks. However, so far a complete logic synthesis flow for reducing the multiplicative complexity in logic networks did not exist or relied heavily on manual manipulations. In this paper, we present a logic synthesis toolbox for cryptography and security applications. The proposed tool consists of powerful transformations, namely resubstitution, refactoring, and rewriting, specifically designed to minimize the multiplicative complexity of an XAG. Our flow is fully automatic and achieves significant results over both EPFL benchmarks and cryptography circuits. We improve the best-known results for cryptography up to 59%, resulting in a normalized geometric mean of 0.82.

The problem of generating a minimal implementation of a given Boolean function is called exact synthesis. The parameter to be minimized is often the total number of gates used for the implementation. The exact synthesis engine is considered an essential tool for most state-of-the-art logic optimization flows. In this paper, we present an algorithm that, using enumeration over non-isomorphic graph structures, generates minimal circuits implementing specified Boolean functions using a set of predefined gate types. In our experiments, we show that our prototype implementation of this technique can be compared to state-of-the-art tools for small functions. Moreover, we show that this technique can be parallelized effectively.

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

We present an exact approach to synthesize temporal-logic formulas in linear temporal logic (LTL) from a set of given positive and negative example traces. Our approach uses topology structures, in particular partial DAGs, to partition the search space into small and manageable subproblems. The algorithm then solves each subproblem independently with the aid of an oracle for deciding satisfiability modulo propositional logic. This strategy is capable of achieving a super-linear speedup when parallelized. We have implemented a bounded synthesis approach to find an LTL formula of minimum size using the proposed topology-guided exact synthesis approach. In an experimental evaluation, we show that the proposed approach achieves a 20× runtime improvement over the state-of-the-art approach.

Abstract Constructing good test cases is difficult and time-consuming, especially if the system under test is still under development and its exact behavior is not yet fixed. We propose a new approach to compute test strategies for reactive systems from a given temporal logic specification using formal methods. The computed strategies are guaranteed to reveal certain simple faults ineveryrealization of the specification and foreverybehavior of the uncontrollable part of the system’s environment. The proposed approach supports different assumptions on occurrences of faults (ranging from a single transient fault to a persistent fault) and by default aims at unveiling the weakest one. We argue that such tests are also sensitive for more complex bugs. Since the specification may not define the system behavior completely, we use reactive synthesis algorithms with partial information. The computed strategies areadaptive test strategiesthat react to behavior at runtime. We work out the underlying theory of adaptive test strategy synthesis and present experiments for a safety-critical component of a real-world satellite system. We demonstrate that our approach can be applied to industrial specifications and that the synthesized test strategies are capable of detecting bugs that are hard to detect with random testing.

We present an outline of the field of Design Understanding and summarize state-of-the-art research in deriving human-understandable knowledge in form of logic properties from an unknown design.

The Exists-Forall (EF) synthesis problem deals with finding parameters such that for all input assignments a correctness specification is met. Many standard problems from computer-aided design and verification can be formulated as an instance of EF synthesis when a function template with holes - parameters to be synthesized - is provided. In this paper, we generalize the idea of EF synthesis in the context of Boolean logic by allowing existential quantification over the domain of Boolean functions (rather than Boolean variables) and present a bounded synthesis approach guided by counterexamples to generate them using techniques from Boolean learning. As an application, we present circuit rectification as an EF synthesis problem and apply the presented approach to incrementally synthesize patches for digital circuits with multiple seeded faults.

CPS, that consist of a cyber part – a computing system – and a physical part – the system in the physical environment – as well as the respective interfaces between those parts, are omnipresent in our daily lives. The application in the physical environment drives the overall requirements that must be respected when designing the computing system. Here, reliability is a core aspect where some of the most pressing design challenges are: monitoring failures throughout the computing system, determining the impact of failures on the application constraints, and ensuring correctness of the computing system with respect to application-driven requirements rooted in the physical environment. This paper provides an overview of techniques discussed in the special session to tackle these challenges throughout the stack of layers of the computing system while tightly coupling the design methodology to the physical requirements.

We propose EASY, an algorithm for functional equivalence checking of ESL descriptions written in a high-level programming language like C++. Given two ESL descriptions, in a PDR-like fashion EASY systematically refines a candidate invariant to characterize the reachable states of a miter of the descriptions until either the invariant becomes inductive or a counterexample has been found. The algorithm is flexible and allows to incorporate a priori knowledge about the design to speed up the verification process. We provide an implementation of EASY on top of a standard model checker and show in two case studies that EASY outperforms other state-of-the-art equivalence checking tools.

We propose an exact algorithm to model-free diagnosis with an application to fault localization in digital circuits. We assume that a faulty circuit and a correctness specification, e.g., in terms of an un-optimized reference circuit, are available. Our algorithm computes the exact set of all minimal diagnoses up to cardinality k considering all possible assignments to the primary inputs of the circuit. This exact diagnosis problem can be naturally formulated and solved using an oracle for Quantified Boolean Satisfiability (QSAT). Our algorithm uses Boolean Satisfiability (SAT) instead to compute the exact result more efficiently. We implemented the approach and present experimental results for determining fault candidates of digital circuits with seeded faults on the gate level. The experiments show that the presented SAT-based approach outperforms state-of-the-art techniques from solving instances of the QSAT problem by several orders of magnitude while having the same accuracy. Moreover, in contrast to QSAT, the SAT-based algorithm has any-time behavior, i.e., at any-time of the computation, an approximation of the exact result is available that can be used as a starting point for debugging. The result improves while time progresses until eventually the exact result is obtained.

We propose an approach for overapproximating the Worst-Case Execution Time (WCET) of embedded control software using formal methods. Model checking is iteratively applied to compute the WCET from the machine code of the software considering a platform and an environment model. We implemented the approach and present first experiments for a thermal controller application executed on a LEON3 processor under different environment constraints.

Equivalence checking is applied when a system description is refined iteratively to reduce the manual effort required to check the consistency before and after modifications. We present a novel functional equivalence checking algorithm which is especially designed to verify equivalence of two hardware descriptions on the system level. Our algorithm uses a stepwise induction proof guided by counterexamples and incorporates a priori knowledge provided by a designer to speed up reasoning. The a priori knowledge is given symbolically in form of a hypothesis, i.e., A logical formula, which approximates the set of all possible equivalence states of the two designs. The algorithm step wisely refines the hypothesis until either a counterexample has been found disproving equivalence or the hypothesis over approximating all equivalence states. Preliminary experiments for two case studies, a scalable parallel counter and a processor model, show the applicability of our approach in practice.

Various problems from artificial intelligence and formal methods are solved utilizing Satisfiability Modulo Theories (SMT) solvers. Selecting the best SMT solver for a specific application, however, is a daunting task. In this paper, we present the novel metaSMT TCP server and client architecture which can be used to solve SMT instances expressed in SMT-LIB2 by multiple solver processes in parallel. The metaSMT TCP server provides a unified interface for SMT-LIB2 instances with the capability to either use the API or the file interface of a solver process and thus serves as a highly customizable portfolio solver. We show that the run-time overhead required by the metaSMT TCP server and client architecture is marginal using selected benchmarks from SMT-LIB.

Embedded systems consist of hardware and software and are ubiquitous in safety-critical and mission-critical fields. The increasing integration density of modern, digital circuits causes an increasing vulnerability of embedded systems to transient faults. Techniques to improve the fault tolerance are often either implemented in hardware or in software. In this paper, we focus on synthesis techniques to improve the fault tolerance of embedded systems considering hardware and software. A greedy algorithm is presented which iteratively assesses the fault tolerance of a processor-based system and decides which components of the system have to be hardened choosing from a set of existing techniques. We evaluate the algorithm in a simple case study using a Traffic Collision Avoidance System (TCAS).

Debugging techniques assist a developer in localizing and correcting faults in a system's description when the behavior of the system does not conform to its specification. Two fault localization techniques are model-based diagnosis and error explanation. Model-based diagnosis computes a subset of the system's components which when replaced correct the system. Error explanation determines potential causes of the system's misbehavior by comparing faulty and correct execution traces. In this paper we focus on fault localization for imperative, non-concurrent programs. We compare the two fault localization techniques in a unified setting presenting SAT-based algorithms for both. The algorithms serve as a vantage point for a fair comparison and allow for efficient implementations leveraging state-of-the-art decision procedures. Firstly, in our comparison we use constructed programs to study strengths and weaknesses of the two fault localization techniques. We show that in general none of the fault localization techniques is superior but that the computed fault candidates depend on the program structure. Secondly, we implement the SAT-based algorithms in a prototype tool utilizing a Satisfiability Modulo Theories (SMT) solver and evaluate them on mutants of the ANSI-C program TCAS from the Software-Artifact Infrastructure Repository (SIR).