Date: Tuesday 20 March 2018
Time: 17:00 - 18:30
Location / Room: Saal 2

Chair:
Patrick Vuillod, Synopsys, FR

Co-Chair:
Amaru Luca, Synopsys, US

Exact synthesis and SAT-based methods open new opportunities in design automation flows, where attaining the best possible logic implementation is key. This executive session covers recent advances on these two topics, which are tightly related, from both academic and industrial standpoints. The first paper shows how to find optimal circuit, on small number of variables, using SAT-solvers. The frontiers of circuits achievable by this method are discussed, together with known open problems. The second paper presents recent advancements on exact synthesis, with focus on implicit enumeration methods. Improvements on the SAT-formulation are delineated, which enable complex constraints to be considered while solving exact synthesis. The third paper introduces a redundancy removal engine based on SAT. Its integration in a commercial EDA tool is described, detailing challenges and opportunities arising in an industrial synthesis environment.

Time	Label	Presentation Title Authors
17:00	4.1.1	IMPROVING CIRCUIT SIZE UPPER BOUNDS USING SAT-SOLVERS Speaker and Author: Alexander Kulikov, Steklov Mathematical Institute at St. Petersburg, RU Abstract Boolean circuits is arguably the most natural model for computing Boolean functions. Despite intensive research, for many functions, we still do not know what optimal circuits look like. In this paper, we discuss how SAT-solvers can be used for constructing optimal circuits for functions on moderate number of variables. We first discuss why this problem is important and then indicate the current frontiers: what can and cannot be found by state-of-the-art SAT-solvers, and for what functions we are interested in finding efficient circuits. Download Paper (PDF; Only available from the DATE venue WiFi)
17:30	4.1.2	PRACTICAL EXACT SYNTHESIS Speaker: Winston Haaswijk, EPFL, CH Authors: Mathias Soeken1, Winston Haaswijk1, Eleonora Testa1, Alan Mishchenko2, Luca G. Amaru3, Robert K. Brayton2 and Giovanni De Micheli1 1EPFL, CH; 2University of California, Berkeley, US; 3Synopsys Inc., US Abstract In this paper, we discuss recent advances in exact synthesis, considering both their efficient implementation and various applications in which they can be employed. We emphasize on solving exact synthesis through Boolean satisfiability (SAT) encodings. Different SAT encodings for exact synthesis are compared, and examined the applications to multi-level logic synthesis, in both area and depth optimization. Another application of SAT based exact synthesis is optimization under many constraints. These constraints can, e.g., be a fixed fanout or delay constraints. Finally, we end our discussion by proposing directions for future research in exact synthesis. Download Paper (PDF; Only available from the DATE venue WiFi)
18:00	4.1.3	SAT-BASED REDUNDANCY REMOVAL Speaker and Author: Krishanu Debnath, Synopsys, IN Abstract Logic optimization is an integral part of digital circuit design. It reduces design area and power consumption, and quite often improves circuit delay as well. Redundancy removal is a key step in logic optimization, in which redundant connections in the circuit are determined and replaced by constant values 0 or 1. The resulting circuit is simplified, resulting in area and power savings. In this paper, we describe a redundancy removal approach for combinational circuits based on a combination of logic simulation and SAT. We show that this approach can handle large industrial-strength designs in a reasonable amount of CPU time. Download Paper (PDF; Only available from the DATE venue WiFi)
18:30		End of session Exhibition Reception in Exhibition Area The Exhibition Reception will take place on Tuesday in the exhibition area, where free drinks for all conference delegates and exhibition visitors will be offered. All exhibitors are welcome to also provide drinks and snacks for the attendees.