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.
Keywords for this software
References in zbMATH (referenced in 9 articles )
Showing results 1 to 9 of 9.
- Lonsing, Florian; Seidl, Martina; Van Gelder, Allen: The QBF gallery: behind the scenes (2016)
- Schlaipfer, Matthias; Weissenbacher, Georg: Labelled interpolation systems for hyper-resolution, clausal, and local proofs (2016)
- Soeken, Mathias; Tague, Laura; Dueck, Gerhard W.; Drechsler, Rolf: Ancilla-free synthesis of large reversible functions using binary decision diagrams (2016)
- Cabodi, Gianpiero; Loiacono, Carmelo; Vendraminetto, Danilo: Optimization techniques for Craig interpolant compaction in unbounded model checking (2015)
- Bloem, Roderick; Könighofer, Robert; Seidl, Martina: SAT-based synthesis methods for safety specs (2014)
- Cruanes, Simon; Hamon, Gregoire; Owre, Sam; Shankar, Natarajan: Tool integration with the evidential tool bus (2013)
- Křena, Bohuslav; Vojnar, Tomáš: Automated formal analysis and verification: an overview (2013)
- Cabodi, Gianpiero; Nocco, Sergio; Quer, Stefano: Benchmarking a model checker for algorithmic improvements and tuning for performance (2011)
- Sen, Alper; Aksanli, Baris; Bozkurt, Murat: Speeding up cycle based logic simulation using graphics processing units (2011)