Logic Synthesis Software School

June 20, 2019 · EPFL · Lausanne, Switzerland · co-organized with IWLS

About the event

The Logic Synthesis Software School (LSSS) is an informal meeting on software tools for logic synthesis and verification. The goal of the meeting is to bring together researchers and tool developers in the fields of electronic design automation, logic synthesis, and verification to foster research on open science infrastructure and tools for logic synthesis and verification. LSSS is a joint event of IWLS and will take place on June 20 at EPFL in Switzerland.

Program (Room: INF328)

Confirmed speakers:

09:00 – 09:15 Welcome
09:15 – 10:45 Tutorial on Modern SAT Solving (Armin Biere) Slides (External)
This tutorial covers algorithmic aspects of conflict-driven clause learning and important extensions developed in recent years, including decision heuristics, restart schemes, various pre- and inprocessing techniques as well as proof generation and checking. Programmatic incremental usage of SAT solvers is discussed next. The talk closes with an overview on the state-of-the-art in parallel SAT solving and open challenges in general.
10:45 – 11:00 Coffee break
11:00 – 12:30 Programming Z3 (Nikolaj Bjorner)
This tutorial provides a programmer's introduction to the Satisfiability Modulo Theories Solver Z3. It describes how to use Z3 through scripts, provided in the Python scripting language, and it describes several of the algorithms underlying the decision procedures within Z3. During the tutorial we dive into selected case studies to cover some of the main available features and give an idea of underlying algorithms.
12:30 – 14:15 Lunch break
14:15 – 15:45 ABC: An industrial-strength logic synthesis and verification tool (Alan Mishchenko) Slides (External)
The talk presents ABC on three levels. On the basic level, ABC is discussed in general, what it has to offer for different users, and what are the most important computations and commands. On the advanced level, there is an overview of different ABC packages and the lessons learned while developing them, as well as an in-depth look into the important data-structures and coding patterns that make ABC fast and efficient. Finally, there is an overview of future research efforts and an invitation for contributions.
15:45 – 16:00 Coffee break
16:00 – 17:30 EPFL Logic Synthesis Libraries (Heinz Riener) Slides
This talk provides an introduction to the EPFL logic synthesis libraries, a set of modular and open-source C++ libraries developed to tackle complex research problems in logic synthesis and verification. The talk describes the overall design principles of the libraries and presents a snapshot of the current development. By example, it is shown how the libraries can be used to solve various logic synthesis problems.
17:30 – 17:45 Closing and Discussion