SAT-Based Logic Synthesis

Alan Mishchenko - University of California Berkeley
Date and time
Monday, June 5, 2017 at 5:30 PM - Sala Riunione II piano
Programme Director
External reference
Publication date
June 5, 2017
Computer Science  


This presentation focuses on the use of Boolean satisfiability as a computation engine in solving typical problems arising in logic synthesis. In particular, a new SAT-based algorithm is presented to compute canonical irredundant sums-of-products (ISOPs) similar to Minato’s well-known BDD/ZDD-based ISOP computation. In addition, a SAT-based formulation of Boolean resubstitution and Engineering Change Order (ECO) is presented. A practical advice is given on the efficient use of SAT solvers in a variety of other practical applications. Contact person: Tiziano Villa

© 2002 - 2021  Verona University
Via dell'Artigliere 8, 37129 Verona  |  P. I.V.A. 01541040232  |  C. FISCALE 93009870234