ABC: An Academic Industrial-Strength Verification Tool

ABC is a public-domain system for logic synthesis and formal verification of binary logic circuits appearing in synchronous hardware designs. ABC combines scalable logic transformations based on And-Inverter Graphs (AIGs), with a variety of innovative algorithms. A focus on the synergy of sequential synthesis and sequential verification leads to improvements in both domains. This paper introduces ABC, motivates its development, and illustrates its use in formal verification.

• Type: Conference
• Year: 2010
• Where: CAV
• Authors: Robert K. Brayton, Alan Mishchenko
• Keywords: CAV 2010, Formal Verification, Hardware, Logic, Scalable Logic Transformations