Mediaspace scheduled maintenance: Aug 25, 2026 07:00 - 12:00 AM. During this time, videos will be temporarily unavailable. Check status updates.

Concept

Program synthesis

Related publications (22)

Three-Input Gates for Logic Synthesis

Giovanni De Micheli, Mathias Soeken, Heinz Riener, Eleonora Testa, Dewmini Sudara Marakkalage

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

IEEE-INST ELECTRICAL ELECTRONICS ENGINEERS INC2021

Preserving Self-Duality During Logic Synthesis for Emerging Reconfigurable Nanotechnologies

Giovanni De Micheli, Heinz Riener, Akash Kumar

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

IEEE2021

SAT-Sweeping Enhanced for Logic Synthesis

Giovanni De Micheli, Luca Gaetano Amarù, Eleonora Testa

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

IEEE2020

Extending Boolean Methods for Scalable Logic Synthesis

Giovanni De Micheli, Mathias Soeken, Pierre-Emmanuel Julien Marc Gaillardon, Eleonora Testa, Luca Gaetano Amarù

In recent years, Boolean methods in logic synthesis have been drawing the attention of EDA researchers due to the continuous push to advance quality of results. Boolean methods require high computational cost, as they rely on complete functional properties ...

2020

Data Structures and Algorithms for Logic Synthesis in Advanced Technologies

Eleonora Testa

Logic synthesis is a key component of digital design and modern EDA tools; it is thus an essential instrument for the design of leading-edge chips and to push the limits of their performance. In the last decades, the electronic circuits community has evolv ...

EPFL2020

Scaling Functional Synthesis and Repair

Emmanouil Koukoutos

Program synthesis was first proposed a few decades ago, but in the last decade it has gained increased momentum in the research community. The increasing complexity of software has dictated the urgent need for improved supporting tools that verify the soft ...

EPFL2019

SAT-Based Exact Synthesis for Multi-Level Logic Networks

Winston Jason Haaswijk

Today, the design of electronic systems is largely automated. The practice of using software automation technologies for the design of electronic hardware is commonly referred to as Electronic Design Automation (EDA). EDA comprises a large set of tools, fr ...

EPFL2019

A Rule Synthesis Algorithm for Programmable Stochastic Self-Assembly of Robotic Modules

Alcherio Martinoli, Bahar Haghighat

Programmable self-assembly of modular robots offers promising means for structure formation at different scales. Rule-based approaches have been previously employed for distributed control of stochastic self-assembly processes. The assembly rate in the pro ...

SPRINGER INTERNATIONAL PUBLISHING AG2019

SAT Based Exact Synthesis using DAG Topology Families

Giovanni De Micheli, Mathias Soeken, Winston Jason Haaswijk

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

IEEE2018

Exploiting Satisfiability Solvers for Efficient Logic Synthesis

Ana Petkovska

Logic synthesis is an important part of electronic design automation (EDA) flows, which enable the implementation of digital systems. As the design size and complexity increase, the data structures and algorithms for logic synthesis must adapt and improve ...

EPFL2017

Solving quantified linear arithmetic by counterexample-guided instantiation

Viktor Kuncak, Andrew Joseph Reynolds

This paper presents a framework to derive instantiation-based decision procedures for satisfiability of quantified formulas in first-order theories, including its correctness, implementation, and evaluation. Using this framework we derive decision procedur ...

2017

Majority-based Synthesis for Nanotechnologies

Giovanni De Micheli, Pierre-Emmanuel Julien Marc Gaillardon, Luca Gaetano Amarù

We study the logic synthesis of emerging nanotechnologies whose elementary devices abstraction is a majority voter. We argue that synthesis tools, natively supporting the majority logic abstraction, are the technology enablers. This is because they allow d ...

Ieee2016

Approximation-aware Rewriting of AIGs for Error Tolerant Applications

Mathias Soeken

Approximation circuits offer superior performance (speed and area) compared to traditional circuits at the cost of computational accuracy. The accuracy of the results in approximation circuits is evaluated based on several error metrics such as worst-case ...

Assoc Computing Machinery2016

Developing Verified Software Using Leon

Viktor Kuncak

We present Leon, a system for developing functional Scala programs annotated with contracts. Contracts in Leon can themselves refer to recursively defined functions. Leon aims to find counterexamples when functions do not meet the specifications, and proof ...

Springer-Verlag Berlin2015

Exploiting Circuit Duality to Speed Up SAT

Giovanni De Micheli, Pierre-Emmanuel Julien Marc Gaillardon, Luca Gaetano Amarù

In this paper, we establish a non-trivial duality between tautology and contradiction check to speed up circuit SAT. Tautology check determines if a logic circuit is true in every possible interpretation. Analogously, contradiction check dete ...

IEEE2015

New Data Structures and Algorithms for Logic Synthesis and Verification

Luca Gaetano Amarù

The strong interaction between Electronic Design Automation (EDA) tools and Complementary Metal-Oxide Semiconductor (CMOS) technology contributed substantially to the advancement of modern digital electronics. The continuous downscaling of CMOS Field Effec ...

EPFL2015

Verifying and Synthesizing Software with Recursive Functions

Viktor Kuncak

Our goal is to help people construct software that does what they wish. We develop tools and algorithms that span static and dynamic verification, constraint solving, and program synthesis. I will outline the current state our verification and synthesis sy ...

Springer-Verlag Berlin2014

Unlocking Controllable-Polarity Transistors Opportunities by Exclusive-OR and Majority Logic Synthesis

Giovanni De Micheli, Pierre-Emmanuel Julien Marc Gaillardon, Luca Gaetano Amarù

For more than four decades, Complementary Metal-Oxide- Semiconductor (CMOS) Field Effect Transistors (FETs) have been the baseline technology for implementing digital computation systems. CMOS transistors natively implement Not-AND ...

2014

Biconditional BDD: A Novel Canonical BDD for Logic Synthesis targeting XOR-rich Functions

Giovanni De Micheli, Pierre-Emmanuel Julien Marc Gaillardon, Luca Gaetano Amarù

We present a novel class of decision diagrams, called Biconditional Binary Decision Diagrams (BBDDs), that enable efficient logic synthesis for XOR-rich functions. BBDDs are binary decision diagrams where the Shannon’s expansion is replaced by the bicondit ...

2013

High-Level Synthesis of Dataflow Programs for Signal Processing Systems

Marco Mattavelli, Endri Bezati

The growing complexity of signal processing algorithms and platforms poses significant challenges to design methods and implementation tools. High-level dataflow programs, such as those in MPEG's RVC-CAL language, provide abstraction and the opportunity fo ...

2013