Publications

Ashenhurst-Curtis decomposition (ACD) is a Boolean decomposition technique widely used in logic synthesis for tasks such as the decomposition of multi-valued relations, the encoding of multi-valued networks, and technology mapping into standard cells for ASICs and lookup tables (LUTs) for FPGAs. A recent truth-table-based implementation of ACD has proven effective for delay-driven LUT mapping while reducing the number of lookup tables, but it does not leverage the flexibility provided by don't-care conditions. In this paper, we enhance ACD by incorporating controllability don't-cares extracted from cuts. Exploiting these additional degrees of freedom, the proposed method increases the decomposition success rate of practical functions into 6-LUTs from 51% to 53.4% and lowers the average number of LUTs per decomposition from 2.50 to 2.46, with even larger gains for large fixed free sets, at only a 1.5x runtime overhead.

This paper addresses the challenge of reducing the number of nodes in Look-Up Table (LUT) networks, with two significant applications: minimizing node count to meet FPGA resource constraints, and area-oriented design space exploration for standard-cell designs, where collapsing a circuit into a LUT network, restructuring it, and remapping helps escape local minima. State-of-the-art substitution algorithms for LUT networks rely heavily on SAT solving, limiting the number of optimization attempts and the size of substitution sub-networks to one node. Conversely, our method relies on circuit simulation to increase the number of substitution candidates and enables substitutions with more than one node. Experimental results show the 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.

Quantum oracle synthesis involves compiling arbitrary Boolean functions into quantum circuits using the gates supported by the target quantum computer. In fault-tolerant quantum computing, these gates (e.g., the Clifford+T library) must be further expressed by logical quantum error correction (QEC) code operations, a process known as back-end compilation. This paper enhances current XAG-based oracle synthesis techniques by establishing a link between the properties of XOR-AND-inverter graphs (XAGs) and the quality measures of back-end-compiled quantum oracles. This connection unlocks additional optimization opportunities: experimental results demonstrate average reductions of 4.49% in T count, 7.00% in logical time steps, and 14.89% in helper qubit count.

We address the problem of minimizing the area of circuits mapped to a technology library, with or without delay constraints. While traditional methods first optimize a technology-independent representation and then perform technology mapping, 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.

In Torus fully homomorphic encryption (TFHE), each look-up table (LUT) corresponds to a costly functional bootstrapping (FBS) operation, making TFHE circuit synthesis an area-oriented technology mapping problem in which the circuit evaluation time correlates with the number of LUTs. This paper presents methods to synthesize more compact homomorphic Boolean circuits: a systematic analysis of the Boolean properties that yield valid large LUTs to facilitate technology mapping, and techniques that maximize the use of multi-value functional bootstrapping (MVFBS) during mapping. Implemented in the mockturtle logic synthesis library, the approach achieves a 29.94% reduction in circuit execution time.

This thesis focuses on developing state-of-the-art logic synthesis methods for advanced technologies. These technologies include conventional CMOS for field-programmable gate arrays (FPGAs) and standard-cell-based designs, as well as superconducting electronics (SCE). In particular, we concentrate on the technology mapping problem, which involves translating a technology-independent circuit description into an interconnection of gates specific to a technology library.

Ashenhurst-Curtis decomposition (ACD) is a decomposition technique used, in particular, to map combinational logic into lookup tables (LUTs) structures when synthesizing hardware designs. 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.

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. In this paper, we identify that the AQFP legalization problem is a scheduling problem; propose linear-time depth-optimal scheduling and irredundant buffer insertion algorithms; present heuristic optimization algorithms to further reduce buffer count; and suggest an unsupervised design space exploration approach for AQFP technology mapping.

The majority-inverter graph (MIG) is a homogeneous logic network widely used in logic synthesis for majority-based emerging technologies. 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.

Ashenhurst-Curtis decomposition (ACD) is a decomposition technique used, in particular, to map combinational logic into lookup table (LUT) 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 formulation to compute two-level decompositions into a variable number of LUTs and enhance delay-driven LUT mapping by performing ACD on the fly. Experiments with heavily optimized benchmarks show an average delay improvement of 12.39% and an area reduction of 2.20% compared to state-of-the-art LUT mapping, with affordable run time, and improve the best-known delay for 4 benchmarks in the EPFL synthesis competition.

This paper focuses on area minimization for circuits already mapped to a technology library, possibly under delay constraints. Traditional methods first optimize a technology-independent representation and then perform technology mapping, assuming that reducing the number of technology-independent nodes correlates with reduced area after mapping. This paper investigates the validity of this assumption and the use of technology-dependent algorithms. We propose an area-oriented engine for mapped circuits that relies on a database of mapped sub-networks to achieve efficient resynthesis. Experimental results on EPFL and IWLS benchmarks, after aggressive technology-independent area-oriented optimization and mapping, show that the proposed method leads to an additional area reduction of 2.50% without worsening the delay.

This paper addresses the challenge of reducing the number of nodes in Look-Up Table (LUT) networks, relevant both to minimizing node count under FPGA resource constraints and to area-oriented design space exploration for standard-cell designs. State-of-the-art substitution algorithms for LUT networks rely heavily on SAT solving, limiting the number of optimization attempts and the size of substitution sub-networks to one node. Conversely, our method relies on circuit simulation to increase the number of substitution candidates and enables substitutions with more than one node, identifying optimization opportunities overlooked by other methods.

Superconducting electronics provide us with cryogenic digital circuits that can rival established technologies in performance and energy consumption. This review focuses on methods, algorithms, and open-source design tools for logic synthesis of superconducting circuits in two major families: single-flux quantum (SFQ) circuits and adiabatic quantum flux parametron (AQFP).

Logic rewriting is a powerful optimization technique that replaces small sections of a Boolean network with better implementations. In this paper, we propose a technique to enable the usage of don't cares in logic rewriting based on pre-computed databases. We show how to process the database and perform Boolean matching with Boolean don't cares, with negligible run time overhead.

Rapid single-flux quantum (RSFQ) is one of the most advanced and promising superconducting logic families, offering exceptional energy efficiency and speed. RSFQ technology requires delay registers (DFFs) and splitter cells to satisfy the path-balancing and driving-capacity constraints. In this paper, we present a comprehensive exploration of methods for synthesizing and optimizing SFQ circuits. In the experimental results, we show an average reduction in the area and delay of 43% and 34%, respectively, compared to the state-of-the-art.

Technology mapping transforms a technology-independent representation into a technology-dependent one given a library of cells. This process is performed by means of local replacements that are extracted by matching sections of the subject graph to library cells. Matching techniques are classified mainly into pattern and Boolean. These two techniques differ in quality and number of generated matches, scalability, and run time. This paper proposes hybrid matching, a new methodology that integrates both techniques in a technology mapping algorithm.

This paper presents a scalable method to increase the support of multi-output library cells in technology mapping. Our contributions include an approach to detect multi-output cells, a fast Boolean matching methodology, and a technology mapping algorithm that supports multi-output cells. Unlike previous work, we address the mapping problem over the whole network. This has the advantage of optimizing area and delay without requiring many incremental steps.

Rapid single-flux quantum (RSFQ) is one of the most advanced superconducting technologies with the potential to supplement or replace conventional VLSI systems. However, scaling RSFQ systems up to VLSI complexity is challenging due to fundamental differences between RSFQ and CMOS technologies. Gate compounding is a novel technique that substantially enriches the functionality realizable within a single clock cycle. In this paper, we propose a technology mapping method for RSFQ circuits that exploits compound gates. Our results show, on average, a 33% lower logic depth with 24% smaller area, as compared to the state of the art.

Factored form is a multi-level representation of a Boolean function that readily maps into CMOS technology. In particular, the number of literals of a factored form correlates well with the number of transistors. This paper focuses on developing techniques for minimizing the total factored form literals count in an and-inverter graph.

Ashenhurst-Curtis decomposition (ACD) is well-known and widely used in logic synthesis for logic restructuring to save area and reduce delay, and in technology dependent optimization to overcome structural bias when mapping into LUTs and LUT structures. The paper offers several simplifications that allow for a fast and flexible implementation of ACD using truth tables for functions up to 16 inputs. A practical extension allows for an efficient use of ACD in delay-driven mapping, which can enhance state-of-the-art LUT mappers.

The Adiabatic Quantum-Flux Parametron (AQFP) is an energy-efficient superconducting logic family. AQFP technology requires buffer and splitting elements (B/S) to be inserted to satisfy path-balancing and fanout-branching constraints. In this work, we study the B/S insertion and optimization methods. The paper proposes an algorithm for B/S insertion that guarantees global depth optimality, a new approach for B/S optimization based on minimum register retiming, and a B/S optimization flow.

A drawback of model checking is that the entire SysML model is used for the verification, even if the property targets a sub-system of the model. In this paper, it is suggested to rely on dependency graphs to avoid applying model checking to the entire system when only a subset of the latter needs to be taken into account.

Individual transistors based on emerging reconfigurable nanotechnologies exhibit electrical conduction for both types of charge carriers. These reconfigurable field-effect transistors (RFETs) enable dynamic reconfiguration to demonstrate either a p- or an n-type functionality. This duality is efficiently abstracted as a self-dual Boolean logic. 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 present a collection of modular open source C++ libraries for the development of logic synthesis applications. These libraries can be used to develop applications for the design of classical and emerging technologies, as well as for the implementation of quantum compilers.

Adiabatic superconducting devices are promising candidates to develop high-speed/low-power electronics. Being the technology fundamentally different from CMOS, new challenges are posed to design automation tools: library cells are controlled by multi-phase clocks, they implement the majority logic function, and they have limited fanout. We present a product-level RTL-to-GDSII flow for the design of Adiabatic Quantum-Flux-Parametron (AQFP) electronic circuits.

Incremental modeling of systems leads to the repeated verification of parts of systems models that were already verified in previous versions of the SysML model. This paper proposes to optimize the verification process by generating dependency graphs from SysML models.

This paper proposes a versatile mapping approach that has three objectives: it can map from one technology-independent graph representation to another; it can map to a cell library; it supports logic rewriting. The mapper is the first one of its kind to support remapping among various graph representations, thus enabling specialized mapping to emerging technologies and for security applications.

This paper proposes a versatile mapping approach for restructuring logic that has two objectives: it can map from one technology-independent graph representation to another; it can map to a cell library.

Model-checking of high-level models, e.g. SysML models, usually first requires a model transformation to a low level formal specification. This paper proposes a new model-checker that can be applied (almost) directly to the SysML model.

This thesis describes several techniques to be used in EDA synthesis tools to increase the QoR of digital circuits. We present circuit transformations able to improve the delay by pushing critical signals forward in the logic.