Concept

Program synthesis

Related publications (34)

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

metaSMT: focus on your application and not on solver integration

Mathias Soeken, Heinz Riener

Many applications from artificial intelligence and formal methods use decision procedures as their core solving engines. In this context, automated reasoning based on Satisfiability (SAT) or Satisfiability Modulo Theories (SMT) is very effective. For a giv ...

Springer Verlag2017

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

Heuristic NPN classification for large functions using AIGs and LEXSAT

Giovanni De Micheli, Paolo Ienne, Mathias Soeken, Ana Petkovska

Two Boolean functions are NPN equivalent if one can be ob- tained from the other by negating inputs, permuting inputs, or negating the output. NPN equivalence is an equivalence relation and the number of equivalence classes is significantly smaller than th ...

Springer Int Publishing Ag2016

Approximation-aware Rewriting of AIGs for Error Tolerant Applications

Mathias Soeken, Arun Chandrasekharan

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ù, Maciej Jerzy Ciesielski

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

Graph Chatbot

Chat with Graph Search

Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.

DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.