{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T22:01:20Z","timestamp":1784844080631,"version":"3.55.0"},"publisher-location":"Berlin, Heidelberg","reference-count":37,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642142949","type":"print"},{"value":"9783642142956","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14295-6_5","type":"book-chapter","created":{"date-parts":[[2010,7,8]],"date-time":"2010-07-08T18:36:09Z","timestamp":1278614169000},"page":"24-40","source":"Crossref","is-referenced-by-count":732,"title":["ABC: An Academic Industrial-Strength Verification Tool"],"prefix":"10.1007","author":[{"given":"Robert","family":"Brayton","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alan","family":"Mishchenko","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"5_CR1","doi-asserted-by":"crossref","unstructured":"Baumgartner, J., Kuehlmann, A.: Min-area retiming on flexible circuit structures. In: Proc. ICCAD\u00a0\u201901, pp. 176\u2013182 (2001)","DOI":"10.1109\/ICCAD.2001.968615"},{"key":"5_CR2","doi-asserted-by":"crossref","unstructured":"Baumgartner, J., Mony, H., Paruthi, V., Kanzelman, R., Janssen, G.: Scalable sequential equivalence checking across arbitrary design transformations. In: Proc. ICCD \u201906 (2006)","DOI":"10.1109\/ICCD.2006.4380826"},{"key":"5_CR3","unstructured":"Berkeley Verification and Synthesis Research Center (BVSRC), http:\/\/www.bvsrc.org"},{"key":"5_CR4","unstructured":"Biere, A.: AIGER: A format for And-Inverter Graphs, http:\/\/fmv.jku.at\/aiger\/"},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"Bjesse, P., Boralv, A.: DAG-aware circuit compression for formal verification. In: Proc. ICCAD \u201904, pp. 42\u201349 (2004)","DOI":"10.1109\/ICCAD.2004.1382541"},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"Bjesse, P., Kukula, J.H.: Automatic generalized phase abstraction for formal verification. In: Proc. ICCAD \u201905, pp. 1076\u20131082 (2005)","DOI":"10.1109\/ICCAD.2005.1560220"},{"key":"5_CR7","doi-asserted-by":"crossref","unstructured":"Brand, D.: Verification of large synthesized designs. In: Proc. ICCAD \u201993, pp. 534\u2013537 (1993)","DOI":"10.1109\/ICCAD.1993.580110"},{"issue":"6","key":"5_CR8","doi-asserted-by":"crossref","first-page":"1062","DOI":"10.1109\/TCAD.1987.1270347","volume":"6","author":"R.K. Brayton","year":"1987","unstructured":"Brayton, R.K., Rudell, R., Sangiovanni-Vincentelli, A.L., Wang, A.R.: MIS: A multiple-level logic optimization system. IEEE Trans. CAD\u00a06(6), 1062\u20131081 (1987)","journal-title":"IEEE Trans. CAD"},{"key":"5_CR9","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"R.K. Brayton","year":"1996","unstructured":"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.\u00a01102. Springer, Heidelberg (1996)"},{"key":"5_CR10","unstructured":"Brayton, R.: The synergy between logic synthesis and equivalence checking. In: Keynote at FMCAD\u201907 (2007), http:\/\/www.cs.utexas.edu\/users\/hunt\/FMCAD\/2007\/presentations\/fmcad07_brayton.ppt"},{"issue":"8","key":"5_CR11","first-page":"677","volume":"35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph based algorithms for Boolean function manipulation. IEEE TC\u00a035(8), 677\u2013691 (1986)","journal-title":"IEEE TC"},{"key":"5_CR12","doi-asserted-by":"crossref","unstructured":"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 \u201909, pp. 1686\u20131691 (2009)","DOI":"10.1109\/DATE.2009.5090934"},{"key":"5_CR13","unstructured":"Chai, D., Jiang, J.-H., Jiang, Y., Li, Y., Mishchenko, A., Brayton, R.: MVSIS 2.0 programmer\u2019s manual. UC Berkeley (May 2003)"},{"key":"5_CR14","unstructured":"Chatterjee, S., Mishchenko, A., Brayton, R., Wang, X., Kam, T.: Reducing structural bias in technology mapping. In: Proc. ICCAD \u201905, pp. 519\u2013526 (2005), http:\/\/www.eecs.berkeley.edu\/~alanmi\/publications\/2005\/iccad05_map.pdf"},{"key":"5_CR15","series-title":"Lecture Notes in Computer Science","volume-title":"Automatic Verification Methods for Finite State Systems","author":"O. Coudert","year":"1990","unstructured":"Coudert, O., Berthet, C., Madre, J.C.: Verification of sequential machines based on symbolic execution. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol.\u00a0407. Springer, Heidelberg (1990)"},{"issue":"4","key":"5_CR16","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1147\/rd.254.0272","volume":"25","author":"A. Darringer","year":"1981","unstructured":"Darringer, A., Joyner Jr., W.H., Berman, C.L., Trevillyan, L.: Logic synthesis through local transformations. IBM J. of Research and Development\u00a025(4), 272\u2013280 (1981)","journal-title":"IBM J. of Research and Development"},{"key":"5_CR17","unstructured":"Een, N., Mishchenko, A., Amla, N.: A single-instance incremental SAT formulation of proof- and counterexample-based abstraction. In: Proc. IWLS\u201910 (2010)"},{"key":"5_CR18","doi-asserted-by":"crossref","unstructured":"Jang, S., Chan, B., Chung, K., Mishchenko, A.: WireMap: FGPA technology mapping for improved routability. In: Proc. FPGA \u201908, pp. 47\u201355 (2008)","DOI":"10.1145\/1344671.1344680"},{"key":"5_CR19","unstructured":"Jang, S., Chung, K., Mishchenko, A., Brayton, R.: A power optimization toolbox for logic synthesis and mapping. In: Proc. IWLS\u00a0\u201909, pp. 1\u20138 (2009)"},{"issue":"12","key":"5_CR20","doi-asserted-by":"crossref","first-page":"2674","DOI":"10.1109\/TCAD.2006.882520","volume":"25","author":"J.-H.R. Jiang","year":"2006","unstructured":"Jiang, J.-H.R., Brayton, R.: Retiming and resynthesis: A complexity perspective. IEEE Trans. CAD\u00a025(12), 2674\u20132686 (2006), http:\/\/www.eecs.berkeley.edu\/~brayton\/publications\/2006\/tcad06_r&r.pdf","journal-title":"IEEE Trans. CAD"},{"key":"5_CR21","doi-asserted-by":"crossref","unstructured":"Jiang, J.-H.R., Hung, W.-L.: Inductive equivalence checking under retiming and resynthesis. In: Proc. ICCAD\u201907, pp. 326\u2013333 (2007)","DOI":"10.1109\/ICCAD.2007.4397285"},{"issue":"12","key":"5_CR22","doi-asserted-by":"crossref","first-page":"1377","DOI":"10.1109\/TCAD.2002.804386","volume":"21","author":"A. Kuehlmann","year":"2002","unstructured":"Kuehlmann, A., Paruthi, V., Krohm, F., Ganai, M.K.: Robust Boolean reasoning for equivalence checking and functional property verification. IEEE Trans. CAD\u00a021(12), 1377\u20131394 (2002)","journal-title":"IEEE Trans. CAD"},{"key":"5_CR23","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/BF01759032","volume":"6","author":"C.E. Leiserson","year":"1991","unstructured":"Leiserson, C.E., Saxe, J.B.: Retiming synchronous circuitry. Algorithmica\u00a06, 5\u201335 (1991)","journal-title":"Algorithmica"},{"key":"5_CR24","doi-asserted-by":"crossref","unstructured":"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\u201394 (2006)","DOI":"10.1109\/FPL.2006.311199"},{"issue":"5","key":"5_CR25","doi-asserted-by":"crossref","first-page":"743","DOI":"10.1109\/TCAD.2005.860955","volume":"25","author":"A. Mishchenko","year":"2006","unstructured":"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\u00a025(5), 743\u2013755 (2006)","journal-title":"IEEE Trans. CAD"},{"key":"5_CR26","doi-asserted-by":"crossref","unstructured":"Mishchenko, A., Chatterjee, S., Brayton, R.: DAG-aware AIG rewriting: A fresh look at combinational logic synthesis. In: Proc. DAC \u201906, pp. 532\u2013536 (2006), http:\/\/www.eecs.berkeley.edu\/~alanmi\/publications\/2006\/dac06_rwr.pdf","DOI":"10.1109\/DAC.2006.229287"},{"key":"5_CR27","doi-asserted-by":"crossref","unstructured":"Mishchenko, A., Chatterjee, S., Brayton, R., Een, N.: Improvements to combinational equivalence checking. In: Proc. ICCAD \u201906, pp. 836\u2013843 (2006)","DOI":"10.1145\/1233501.1233679"},{"key":"5_CR28","doi-asserted-by":"crossref","unstructured":"Mishchenko, A., Cho, S., Chatterjee, S., Brayton, R.: Combinational and sequential mapping with priority cuts. In: Proc. ICCAD \u201907, pp. 354\u2013361 (2007)","DOI":"10.1109\/ICCAD.2007.4397290"},{"key":"5_CR29","doi-asserted-by":"crossref","unstructured":"Mishchenko, A., Case, M.L., Brayton, R.K., Jang, S.: Scalable and scalably-verifiable sequential synthesis. In: Proc. ICCAD\u201908, pp. 234\u2013241 (2008)","DOI":"10.1109\/ICCAD.2008.4681580"},{"key":"5_CR30","doi-asserted-by":"crossref","unstructured":"Mishchenko, A., Brayton, R., Jang, S.: Global delay optimization using structural choices. In: Proc. FPGA\u201910, pp. 181\u2013184 (2010)","DOI":"10.1145\/1723112.1723144"},{"key":"5_CR31","unstructured":"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\u201910 (2010)"},{"key":"5_CR32","doi-asserted-by":"crossref","unstructured":"Mony, H., Baumgartner, J., Paruthi, V., Kanzelman, R.: Exploiting suspected redundancy without proving it. In: Proc. DAC\u201905, pp. 463\u2013466 (2005)","DOI":"10.1145\/1065579.1065700"},{"key":"5_CR33","doi-asserted-by":"crossref","unstructured":"Mony, H., Baumgartner, J., Mishchenko, A., Brayton, R.: Speculative reduction-based scalable redundancy identification. In: Proc. DATE\u201909, pp. 1674\u20131679 (2009)","DOI":"10.1109\/DATE.2009.5090932"},{"key":"5_CR34","unstructured":"Ray, S., Mishchenko, A., Brayton, R.K., Jang, S., Daniel, T.: Minimum-perturbation retiming for delay optimization. In: Proc. IWLS\u201910 (2010)"},{"key":"5_CR35","unstructured":"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)"},{"key":"5_CR36","unstructured":"Somenzi, F.: BDD package. CUDD v. 2.3.1, http:\/\/vlsi.colorado.edu\/~fabio\/CUDD\/cuddIntro.html"},{"key":"5_CR37","doi-asserted-by":"crossref","unstructured":"Yang, C., Ciesielski, M., Singhal, V.: BDS: a BDD-based logic optimization system. In: Proc. DAC\u201900, pp. 92\u201397 (2000), http:\/\/www.ecs.umass.edu\/ece\/labs\/vlsicad\/bds\/bds.html","DOI":"10.1145\/337292.337323"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14295-6_5.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,23]],"date-time":"2020-11-23T21:50:41Z","timestamp":1606168241000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14295-6_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642142949","9783642142956"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14295-6_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}