Abstract
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.
Chapter PDF
Similar content being viewed by others
Keywords
References
Baumgartner, J., Kuehlmann, A.: Min-area retiming on flexible circuit structures. In: Proc. ICCAD ’01, pp. 176–182 (2001)
Baumgartner, J., Mony, H., Paruthi, V., Kanzelman, R., Janssen, G.: Scalable sequential equivalence checking across arbitrary design transformations. In: Proc. ICCD ’06 (2006)
Berkeley Verification and Synthesis Research Center (BVSRC), http://www.bvsrc.org
Biere, A.: AIGER: A format for And-Inverter Graphs, http://fmv.jku.at/aiger/
Bjesse, P., Boralv, A.: DAG-aware circuit compression for formal verification. In: Proc. ICCAD ’04, pp. 42–49 (2004)
Bjesse, P., Kukula, J.H.: Automatic generalized phase abstraction for formal verification. In: Proc. ICCAD ’05, pp. 1076–1082 (2005)
Brand, D.: Verification of large synthesized designs. In: Proc. ICCAD ’93, pp. 534–537 (1993)
Brayton, R.K., Rudell, R., Sangiovanni-Vincentelli, A.L., Wang, A.R.: MIS: A multiple-level logic optimization system. IEEE Trans. CAD 6(6), 1062–1081 (1987)
Brayton, R.K., Hachtel, G.D., Sangiovanni-Vincentelli, A., Somenzi, F., Aziz, A., Cheng, S.-T., Edwards, S., Khatri, S., Kukimoto, Y., Pardo, A., Qadeer, S., Ranjan, R.K., Sarwary, S., Shiple, T.R., Swamy, G., Villa, T.: VIS: A system for verification and synthesis. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102. Springer, Heidelberg (1996)
Brayton, R.: The synergy between logic synthesis and equivalence checking. In: Keynote at FMCAD’07 (2007), http://www.cs.utexas.edu/users/hunt/FMCAD/2007/presentations/fmcad07_brayton.ppt
Bryant, R.E.: Graph based algorithms for Boolean function manipulation. IEEE TC 35(8), 677–691 (1986)
Cabodi, G., Camurati, P., Garcia, L., Murciano, M., Nocco, S., Quer, S.: Speeding up model checking by exploiting explicit and hidden verification constraints. In: Proc. DATE ’09, pp. 1686–1691 (2009)
Chai, D., Jiang, J.-H., Jiang, Y., Li, Y., Mishchenko, A., Brayton, R.: MVSIS 2.0 programmer’s manual. UC Berkeley (May 2003)
Chatterjee, S., Mishchenko, A., Brayton, R., Wang, X., Kam, T.: Reducing structural bias in technology mapping. In: Proc. ICCAD ’05, pp. 519–526 (2005), http://www.eecs.berkeley.edu/~alanmi/publications/2005/iccad05_map.pdf
Coudert, O., Berthet, C., Madre, J.C.: Verification of sequential machines based on symbolic execution. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407. Springer, Heidelberg (1990)
Darringer, A., Joyner Jr., W.H., Berman, C.L., Trevillyan, L.: Logic synthesis through local transformations. IBM J. of Research and Development 25(4), 272–280 (1981)
Een, N., Mishchenko, A., Amla, N.: A single-instance incremental SAT formulation of proof- and counterexample-based abstraction. In: Proc. IWLS’10 (2010)
Jang, S., Chan, B., Chung, K., Mishchenko, A.: WireMap: FGPA technology mapping for improved routability. In: Proc. FPGA ’08, pp. 47–55 (2008)
Jang, S., Chung, K., Mishchenko, A., Brayton, R.: A power optimization toolbox for logic synthesis and mapping. In: Proc. IWLS ’09, pp. 1–8 (2009)
Jiang, J.-H.R., Brayton, R.: Retiming and resynthesis: A complexity perspective. IEEE Trans. CAD 25(12), 2674–2686 (2006), http://www.eecs.berkeley.edu/~brayton/publications/2006/tcad06_r&r.pdf
Jiang, J.-H.R., Hung, W.-L.: Inductive equivalence checking under retiming and resynthesis. In: Proc. ICCAD’07, pp. 326–333 (2007)
Kuehlmann, A., Paruthi, V., Krohm, F., Ganai, M.K.: Robust Boolean reasoning for equivalence checking and functional property verification. IEEE Trans. CAD 21(12), 1377–1394 (2002)
Leiserson, C.E., Saxe, J.B.: Retiming synchronous circuitry. Algorithmica 6, 5–35 (1991)
Lamoureux, J., Wilton, S.J.E.: Activity estimation for Field-Programmable Gate Arrays. In: Proc. Intl Conf. Field-Prog. Logic and Applications (FPL), pp. 87–94 (2006)
Mishchenko, A., Zhang, J.S., Sinha, S., Burch, J.R., Brayton, R., Chrzanowska-Jeske, M.: Using simulation and satisfiability to compute flexibilities in Boolean networks. IEEE Trans. CAD 25(5), 743–755 (2006)
Mishchenko, A., Chatterjee, S., Brayton, R.: DAG-aware AIG rewriting: A fresh look at combinational logic synthesis. In: Proc. DAC ’06, pp. 532–536 (2006), http://www.eecs.berkeley.edu/~alanmi/publications/2006/dac06_rwr.pdf
Mishchenko, A., Chatterjee, S., Brayton, R., Een, N.: Improvements to combinational equivalence checking. In: Proc. ICCAD ’06, pp. 836–843 (2006)
Mishchenko, A., Cho, S., Chatterjee, S., Brayton, R.: Combinational and sequential mapping with priority cuts. In: Proc. ICCAD ’07, pp. 354–361 (2007)
Mishchenko, A., Case, M.L., Brayton, R.K., Jang, S.: Scalable and scalably-verifiable sequential synthesis. In: Proc. ICCAD’08, pp. 234–241 (2008)
Mishchenko, A., Brayton, R., Jang, S.: Global delay optimization using structural choices. In: Proc. FPGA’10, pp. 181–184 (2010)
Mishchenko, A., Een, N., Brayton, R.K., Jang, S., Ciesielski, M., Daniel, T.: Magic: An industrial-strength logic optimization, technology mapping, and formal verification tool. In: IWLS’10 (2010)
Mony, H., Baumgartner, J., Paruthi, V., Kanzelman, R.: Exploiting suspected redundancy without proving it. In: Proc. DAC’05, pp. 463–466 (2005)
Mony, H., Baumgartner, J., Mishchenko, A., Brayton, R.: Speculative reduction-based scalable redundancy identification. In: Proc. DATE’09, pp. 1674–1679 (2009)
Ray, S., Mishchenko, A., Brayton, R.K., Jang, S., Daniel, T.: Minimum-perturbation retiming for delay optimization. In: Proc. IWLS’10 (2010)
Sentovich, E.M., Singh, K.J., Lavagno, L., Moon, C., Murgai, R., Saldanha, A., Savoj, H., Stephan, P.R., Brayton, R.K., Sangiovanni-vincentelli, A.: SIS: A system for sequential circuit synthesis. Technical Report, UCB/ERI, M92/41, ERL, Dept. of EECS, UC Berkeley (1992)
Somenzi, F.: BDD package. CUDD v. 2.3.1, http://vlsi.colorado.edu/~fabio/CUDD/cuddIntro.html
Yang, C., Ciesielski, M., Singhal, V.: BDS: a BDD-based logic optimization system. In: Proc. DAC’00, pp. 92–97 (2000), http://www.ecs.umass.edu/ece/labs/vlsicad/bds/bds.html
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Brayton, R., Mishchenko, A. (2010). ABC: An Academic Industrial-Strength Verification Tool. In: Touili, T., Cook, B., Jackson, P. (eds) Computer Aided Verification. CAV 2010. Lecture Notes in Computer Science, vol 6174. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-14295-6_5
Download citation
DOI: https://doi.org/10.1007/978-3-642-14295-6_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-14294-9
Online ISBN: 978-3-642-14295-6
eBook Packages: Computer ScienceComputer Science (R0)