ABC: Industrial-Strength Academic Tool for Logic Synthesis and Formal Verification

Wednesday, 7 March 2012 at 16h45 in INF 328

Alan Mishchenko, Research Scientist, Department of Electrical Engineering and Computer Science, University of California, Berkeley

Abstract:  This talk summarizes a decade of working for industry in academia as part of Berkeley Verification and Synthesis Research Center (BVSRC) at UC Berkeley, where we are developing a public-domain system for logic synthesis and formal verification called ABC, which is widely used by both design houses and CAD tool companies. ABC combines scalable logic transformations based on And-Inverter Graphs (AIGs), with a variety of innovative algorithms, implemented with attention to detail such as runtime and memory usage, resulting in the industrial-strength code. Recognizing and exploiting synergy of sequential synthesis and sequential verification leads to improvements in both domains.

About the Speaker: Alan Mishchenko graduated from Moscow Institute of Physics and Technology (Moscow, Russia) in 1993 and Glushkov Institute of Cybernetics (Kiev, Ukraine) in 1997. From 1998 to 2002 he was an Intel-sponsored researcher at Portland State University. In 2002, he joined the EECS Department at UC Berkeley, where he is currently an associate researcher at Berkeley Verification and Synthesis Research Center (BVSRC). Alan is interested in developing efficient methods for synthesis and verification.