The Synergy Between Logic Synthesis and Formal Verification
Our research group has been working on logic synthesis with forays into formal verification for several decades. As a result, we have become increasingly aware of the similarity between these two lines of research, resulting in a synergistic approach, which is our main research focus these days. For example, formal verification systems often use And-Invertor-Graphs (AIGs). Verification experts developed these and came up with very fast methods to reduce the AIG representation for use in verification engines. Recently, these computations have been extended to work in synthesis, resulting in improved quality and scalability, as exemplified by its successful adoption in several FPGA synthesis tools. Investigation of the commonalities between logic synthesis and formal verification led us to develop a new CAD tool, ABC, which is both a synthesis and verification tool. ABC is a public domain system in development at Berkeley. It has become popular with academic institutions as well as industrial companies. In the talk, ABC will be overviewed and some of the synthesis techniques borrowed from verification will be described.
Prof. Robert K. Brayton and Prof. Alan Mishchenko, University of California Berkeley