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.

References in zbMATH (referenced in 14 articles )

Showing results 1 to 14 of 14.
Sorted by year (citations)

  1. Chakraborty, Supratik; Khasidashvili, Zurab; Seger, Carl-Johan H.; Gajavelly, Rajkumar; Haldankar, Tanmay; Chhatani, Dinesh; Mistry, Rakesh: Symbolic trajectory evaluation for word-level verification: theory and implementation (2017)
  2. Könighofer, Bettina; Alshiekh, Mohammed; Bloem, Roderick; Humphrey, Laura; Könighofer, Robert; Topcu, Ufuk; Wang, Chao: Shield synthesis (2017)
  3. Lonsing, Florian; Seidl, Martina; Van Gelder, Allen: The QBF Gallery: behind the scenes (2016)
  4. Schlaipfer, Matthias; Weissenbacher, Georg: Labelled interpolation systems for hyper-resolution, clausal, and local proofs (2016)
  5. Soeken, Mathias; Mishchenko, Alan; Petkovska, Ana; Sterin, Baruch; Ienne, Paolo; Brayton, Robert K.; De Micheli, Giovanni: Heuristic NPN classification for large functions using AIGs and LEXSAT (2016)
  6. Soeken, Mathias; Tague, Laura; Dueck, Gerhard W.; Drechsler, Rolf: Ancilla-free synthesis of large reversible functions using binary decision diagrams (2016)
  7. Cabodi, Gianpiero; Loiacono, Carmelo; Vendraminetto, Danilo: Optimization techniques for Craig interpolant compaction in unbounded model checking (2015)
  8. Ignatiev, Alexey; Previti, Alessandro; Marques-Silva, Joao: SAT-based formula simplification (2015)
  9. Bloem, Roderick; Könighofer, Robert; Seidl, Martina: SAT-based synthesis methods for safety specs (2014)
  10. Cruanes, Simon; Hamon, Gregoire; Owre, Sam; Shankar, Natarajan: Tool integration with the evidential tool bus (2013)
  11. Křena, Bohuslav; Vojnar, Tomáš: Automated formal analysis and verification: an overview (2013)
  12. Cabodi, Gianpiero; Nocco, Sergio; Quer, Stefano: Benchmarking a model checker for algorithmic improvements and tuning for performance (2011)
  13. Sen, Alper; Aksanli, Baris; Bozkurt, Murat: Speeding up cycle based logic simulation using graphics processing units (2011) ioport
  14. Brayton, Robert; Mishchenko, Alan: ABC: an academic industrial-strength verification tool (2010) ioport