{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,31]],"date-time":"2022-03-31T16:49:05Z","timestamp":1648745345756},"reference-count":38,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2010,1,30]],"date-time":"2010-01-30T00:00:00Z","timestamp":1264809600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Electron Test"],"published-print":{"date-parts":[[2010,4]]},"DOI":"10.1007\/s10836-010-5144-0","type":"journal-article","created":{"date-parts":[[2010,1,28]],"date-time":"2010-01-28T22:51:08Z","timestamp":1264719068000},"page":"261-278","source":"Crossref","is-referenced-by-count":0,"title":["Finding Multiple Equivalence-Preserving Transformations in Combinational Circuits through Incremental-SAT"],"prefix":"10.1007","volume":"26","author":[{"given":"Gianpiero","family":"Cabodi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Leandro","family":"Dipietro","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marco","family":"Murciano","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sergio","family":"Nocco","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2010,1,30]]},"reference":[{"key":"5144_CR1","doi-asserted-by":"crossref","unstructured":"Baumgartner J, Mony H, Aziz A (2008) Optimal constraint-preserving netlist simplification. In: Proc\u00a0formal methods in computer-aided design","DOI":"10.1109\/FMCAD.2008.ECP.7"},{"key":"5144_CR2","volume-title":"IDTC\u201996: international design and testing conference","author":"G Berry","year":"1996","unstructured":"Berry G, Shiple TR, Touati H (1996) Constructive analysis of cyclic circuits. In: IDTC\u201996: international design and testing conference, Paris, France"},{"key":"5144_CR3","unstructured":"Biere A, Jussila T (2008) The model checking competition web page. http:\/\/fmv.jku.at\/hwmcc08"},{"key":"5144_CR4","series-title":"LNCS","volume-title":"Proc formal methods in computer-aided design","author":"P Bjesse","year":"2000","unstructured":"Bjesse P, Claessen K (2000) SAT-based verification without state space traversal. In: Proc formal methods in computer-aided design. LNCS, vol 1954. Springer, Austin"},{"key":"5144_CR5","volume-title":"dcc02: designing correct circuits 2002","author":"A Bouali","year":"2002","unstructured":"Bouali A, Bres Y, Berry G, Sentovich EM (2002) State abstraction techniques for the verification of synchronous circuits. In: dcc02: designing correct circuits 2002. Grenoble, France"},{"key":"5144_CR6","first-page":"205","volume-title":"Proc. formal methods in computer-aided design","author":"G Cabodi","year":"2008","unstructured":"Cabodi G, Camurati P, Garcia L, Murciano M, Nocco S, Quer S (2008) Trading-off SAT search and variable quantifications for effective unbounded model checking. In: Proc. formal methods in computer-aided design. Portland, Oregon, pp 205\u2013212"},{"key":"5144_CR7","first-page":"129","volume-title":"Proc int\u2019l conf on computer-aided design","author":"G Cabodi","year":"2008","unstructured":"Cabodi G, Camurati P, Murciano M (2008) Automated abstraction by incremental refinement in interpolant-based model checking. In: Proc int\u2019l conf on computer-aided design. ACM, San Jose, pp 129\u2013136"},{"key":"5144_CR8","volume-title":"Proc design automation & test in Europe conf","author":"G Cabodi","year":"2005","unstructured":"Cabodi G, Crivellari M, Nocco S, Quer S (2005) Circuit based quantification: back to state set manipulation within unbounded model checking. In: Proc design automation & test in Europe conf., IEEE Computer Society, Munich"},{"key":"5144_CR9","doi-asserted-by":"crossref","unstructured":"Cabodi G, Dipietro L, Murciano M, Nocco S (2009) Exploiting incrementality in sat-based search for multiple equivalence-preserving transformations in combinational circuits. In: Proceedings of the 2009 IEEE international high level design validation and test workshop. IEEE Computer Society","DOI":"10.1109\/HLDVT.2009.5340177"},{"key":"5144_CR10","first-page":"772","volume-title":"Proc int\u2019l conf on computer-aided design","author":"G Cabodi","year":"2006","unstructured":"Cabodi G, Murciano M, Nocco S, Quer S (2006) Stepping forward with interpolants in unbounded model checking. In: Proc int\u2019l conf on computer-aided design. ACM, San Jose, pp 772\u2013778"},{"issue":"1","key":"5144_CR11","doi-asserted-by":"crossref","first-page":"309","DOI":"10.1145\/1297666.1297669","volume":"13","author":"G Cabodi","year":"2008","unstructured":"Cabodi G, Murciano M, Nocco S, Quer S (2008) Boosting interpolation with dynamic localized abstraction and redundancy removal. ACM Trans Des Automat Electron Syst 13(1):309\u2013340","journal-title":"ACM Trans Des Automat Electron Syst"},{"key":"5144_CR12","doi-asserted-by":"crossref","unstructured":"Chang SC, Cheng DI, Yeh CW (1998) On removing multiple redundancies in combinational circuits. In: Proc design automation & test in Europe conf, pp 738\u2013742","DOI":"10.1109\/DATE.1998.655940"},{"key":"5144_CR13","doi-asserted-by":"crossref","unstructured":"Chang SC, Marek-Sadowska M (1996) Perturb and simplify: optimizing combinational circuits with external don\u2019t cares. In: Proc European design and test conference, pp 402\u2013406","DOI":"10.1109\/EDTC.1996.494332"},{"issue":"5","key":"5144_CR14","doi-asserted-by":"crossref","first-page":"386","DOI":"10.1109\/43.703921","volume":"17","author":"M Chatterjee","year":"1998","unstructured":"Chatterjee M, Pradhan DK,\u00a0Kunz W (1998) LOT: logic optimization with testability\u2014new transformations for logic synthesis. IEEE Trans Comput-Aided Des 17(5):386\u2013398","journal-title":"IEEE Trans Comput-Aided Des"},{"key":"5144_CR15","doi-asserted-by":"crossref","unstructured":"Chen G, Reddy SM, Pomeranz I, Rajski J (2006) New procedures to identify redundant stuck-at faults and removal of redundant logic. In: Proc int conf on VLSI, pp 419\u2013424","DOI":"10.1109\/VLSID.2006.120"},{"key":"5144_CR16","first-page":"1","volume":"4","author":"KD Cooper","year":"2001","unstructured":"Cooper KD, Harvey TJ, Kennedy K (2001) A simple, fast dominance algorithm. Software Pract Ex 4:1\u201310","journal-title":"Software Pract Ex"},{"issue":"4","key":"5144_CR17","doi-asserted-by":"crossref","first-page":"543","DOI":"10.1016\/S1571-0661(05)82542-3","volume":"89","author":"N E\u00e9n","year":"2003","unstructured":"E\u00e9n N, S\u00f6rensson N (2003) Temporal induction by incremental sat solving. Electron Notes Theor Comp Sci 89(4):543\u2013560","journal-title":"Electron Notes Theor Comp Sci"},{"key":"5144_CR18","unstructured":"E\u00e9n N, S $\\ddot{\\mbox{o}}$ rensson N (2009) The minisat SAT solver. http:\/\/minisat.se"},{"key":"5144_CR19","doi-asserted-by":"crossref","unstructured":"Fraer R, Ikram S, Kamhi G, Leonard T, Mokkedem A (2002) Accelerated verification of RTL assertions based on satisfiability solvers. In: Proc HLDVT","DOI":"10.1109\/HLDVT.2002.1224437"},{"issue":"1","key":"5144_CR20","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1109\/T-C.1972.223428","volume":"21","author":"JW Gault","year":"1972","unstructured":"Gault JW, Robinson JP, Reddy SM (1972) Multiple fault detection in combinational networks. IEEE Trans Comput C-21(1):31\u201336","journal-title":"IEEE Trans Comput C-"},{"key":"5144_CR21","first-page":"593","volume-title":"BMC\u201903: first international workshop on bounded model checking","author":"Z Khasidashvili","year":"2003","unstructured":"Khasidashvili Z, Hanna Z (2003) Sat-based methods for sequential hardware equivalence verification without synchronization. In: BMC\u201903: first international workshop on bounded model checking. Boulder, Colorado, pp 593\u2013607"},{"key":"5144_CR22","unstructured":"Kim J, Marques-Silva J, Savoj H, Sakallah KA (1997) RID-GRASP: redundancy identification and removal using GRASP. In: Proc int\u2019l workshop on logic synthesis"},{"key":"5144_CR23","unstructured":"Kunz W (1993) HANNIBAL: an efficient tool for logic verification based on recursive learning. In: Proc int\u2019l conf on computer-aided design"},{"key":"5144_CR24","unstructured":"Kunz W, Menon PR (1994) Multi-level logic optimization by implication analysis. In: Proc int\u2019l conf on computer-aided design, pp 6\u201313"},{"key":"5144_CR25","doi-asserted-by":"crossref","first-page":"950","DOI":"10.1109\/43.293952","volume":"13","author":"S Malik","year":"1994","unstructured":"Malik S (1994) Analysis of cyclic combinational circuits. IEEE Trans Comput-Aided Des 13:950\u2013956","journal-title":"IEEE Trans Comput-Aided Des"},{"key":"5144_CR26","unstructured":"Marques-Silva JP, Sakalla KA (1996) GRASP\u2014a new search algorithm for satisfiability. In: Int\u2019l conference on tool with artificial intelligence"},{"key":"5144_CR27","unstructured":"McMillan KL (2005) Don\u2019t-care computation using k-clause approximation. In: Proc int\u2019l workshop on logic synthesis"},{"key":"5144_CR28","doi-asserted-by":"crossref","unstructured":"Mill\u00e1n ES, Entrena LA, Espejo JA (2008) Logic transformations by multiple wire network addition. In: Proc EUROMICRO conf on digital system design architectures, methods and tools, pp 779\u2013786","DOI":"10.1109\/DSD.2008.79"},{"key":"5144_CR29","unstructured":"Mishchenko A (2005) ABC: a system for sequential synthesis and verification. http:\/\/www.eecs.berkeley.edu\/~alanmi\/abc\/"},{"key":"5144_CR30","doi-asserted-by":"crossref","unstructured":"Mishchenko A, Brayton RK (2005) SAT-based complete don\u2019t-care computation for network optimization. In: Proc design automation & test in Europe conf, pp 412\u2013417","DOI":"10.1109\/DATE.2005.264"},{"key":"5144_CR31","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1007\/11560548_21","volume-title":"Proc. correct hardware design and verification methods","author":"H Mony","year":"2005","unstructured":"Mony H, Baumgartner J, Aziz A (2005) Exploiting constraints in transformation-based verification. In: Borrione D, Paul W (eds) Proc. correct hardware design and verification methods. LNCS, vol 3275. Springer, Edimburgh, pp 269\u2013284"},{"key":"5144_CR32","unstructured":"Pomeranz I, Reddy SM (1996) On finding functionally identical and functionally opposite lines in combinational logic circuits. In: Proc int conf on VLSI, pp 254\u2013259"},{"key":"5144_CR33","doi-asserted-by":"crossref","unstructured":"Saldanha A, Wang AR, Brayton RK, Sangiovanni-Vincentelli AL (1989) Multi-level logic simplification using don\u2019t cares and filters. In: Proc design automation conf, pp 277\u2013282","DOI":"10.1145\/74382.74429"},{"key":"5144_CR34","doi-asserted-by":"crossref","unstructured":"Saluja N, Khatri SP (2004) A robust algorithm for approximate compatible observability don\u2019t care computation. In: Proc design automation conf, pp 422\u2013427","DOI":"10.1145\/996566.996688"},{"key":"5144_CR35","doi-asserted-by":"crossref","unstructured":"Savoj H, Brayton RK (1990) The use of observability and external don\u2019t cares for the simplification of multi-level networks. In: Proc design automation conf, pp 297\u2013301","DOI":"10.1145\/123186.123280"},{"key":"5144_CR36","doi-asserted-by":"crossref","unstructured":"Sinz C (2005) Towards an optimal CNF encoding of boolean cardinality constraints. In: Proc principles and practice of constraint programming, pp 827\u2013831","DOI":"10.1007\/11564751_73"},{"key":"5144_CR37","doi-asserted-by":"crossref","unstructured":"Veneris A, Abadir MS, Amiri M (2002) Design rewiring using ATPG. In: Proc int\u2019l test conf, pp 223\u2013232","DOI":"10.1109\/TEST.2002.1041764"},{"key":"5144_CR38","doi-asserted-by":"crossref","unstructured":"Zhu Q, Kitchen N, Kuehlmann A, Sangiovanni-Vincentelli A (2006) SAT sweeping with local observability don\u2019t-cares. In: Proc design automation conf, pp 229\u2013234","DOI":"10.1145\/1146909.1146970"}],"container-title":["Journal of Electronic Testing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10836-010-5144-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10836-010-5144-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10836-010-5144-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T21:57:45Z","timestamp":1559253465000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10836-010-5144-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,1,30]]},"references-count":38,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2010,4]]}},"alternative-id":["5144"],"URL":"https:\/\/doi.org\/10.1007\/s10836-010-5144-0","relation":{},"ISSN":["0923-8174","1573-0727"],"issn-type":[{"value":"0923-8174","type":"print"},{"value":"1573-0727","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,1,30]]}}}