{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T20:09:44Z","timestamp":1694635784585},"reference-count":26,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2008,11,26]],"date-time":"2008-11-26T00:00:00Z","timestamp":1227657600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Des Autom Embed Syst"],"published-print":{"date-parts":[[2008,12]]},"DOI":"10.1007\/s10617-008-9033-z","type":"journal-article","created":{"date-parts":[[2008,12,2]],"date-time":"2008-12-02T20:31:36Z","timestamp":1228249896000},"page":"377-396","source":"Crossref","is-referenced-by-count":8,"title":["Sequential equivalence checking between system level and RTL descriptions"],"prefix":"10.1007","volume":"12","author":[{"given":"Shobha","family":"Vasudevan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vinod","family":"Viswanath","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jacob A.","family":"Abraham","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"JiaJin","family":"Tu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2008,11,26]]},"reference":[{"key":"9033_CR1","doi-asserted-by":"crossref","unstructured":"Abraham JA, Vedula VM, Saab DG (2002) Verifying properties using sequential ATPG. In: Proceedings of the IEEE international test conference, pp 194\u2013200","DOI":"10.1109\/TEST.2002.1041761"},{"key":"9033_CR2","doi-asserted-by":"crossref","unstructured":"Anastasakis D, Damiano R, Ma H-KT, Stanion T (2002) A practical and efficient method for compare-point matching. In: Proceedings of the 39th design automation conference, pp 305\u2013310","DOI":"10.1109\/DAC.2002.1012640"},{"key":"9033_CR3","volume-title":"SystemC: From the ground up","author":"DC Black","year":"2005","unstructured":"Black DC, Donovan J (2005) SystemC: From the ground up. Springer, Berlin"},{"key":"9033_CR4","doi-asserted-by":"crossref","unstructured":"Burch JR, Singhal V (1998) Robust latch mapping for combinational equivalence checking. In: Proceedings of the IEEE\/ACM international conference on computer-aided design, pp. 563\u2013569","DOI":"10.1145\/288548.289087"},{"key":"9033_CR5","unstructured":"Cai L, Gajski D (2003) Transaction level modeling: an overview. In: Proceedings of the 1st IEEE\/ACM\/IFIP international conference on hardware\/software codesign and system synthesis, pp 19\u201324"},{"key":"9033_CR6","unstructured":"Calypto design systems http:\/\/www.calypto.com"},{"key":"9033_CR7","unstructured":"Clarke E, Kroening D (2003) Hardware verification using ANSI-C programs as a reference. In: Proceedings of the IEEE Asia south pacific\u2014Design automation conference, pp 308\u2013311"},{"key":"9033_CR8","unstructured":"Digital radio mondiale http:\/\/www.drm.org"},{"key":"9033_CR9","volume-title":"Transaction-level modeling with SystemC: TLM concepts and applications for embedded systems","year":"2006","unstructured":"Ghenassia F (ed) (2006) Transaction-level modeling with SystemC: TLM concepts and applications for embedded systems. Springer, Berlin"},{"key":"9033_CR10","unstructured":"Fu Z, Mahajan Y, Malik S, zChaff Solver http:\/\/www.princeton.edu\/~zchaff\/zchaff.html"},{"key":"9033_CR11","doi-asserted-by":"crossref","unstructured":"Huang S-Y, Cheng K-T, Chen K-C (2001) Verifying sequential equivalence using ATPG techniques. In: ACM transactions on design automation of electronic systems, pp 244\u2013275","DOI":"10.1145\/375977.376022"},{"key":"9033_CR12","unstructured":"Kroening D, Clarke E, Yorav K (2003) Behavioral consistency of C and Verilog programs using bounded model checking. In: Proceedings of the 40th IEEE design automation conference, pp 368\u2013371"},{"key":"9033_CR13","doi-asserted-by":"crossref","unstructured":"Lu F, Iyer MK, Parthasarathy G, Wang L-C, Cheng K-T, Chen K-C (2005) An efficient sequential SAT solver with improved search strategies. In: Proceedings of the IEEE design automation and test in Europe, pp 1102\u20131107","DOI":"10.1109\/DATE.2005.55"},{"key":"9033_CR14","doi-asserted-by":"crossref","unstructured":"Matsumoto T, Saito H, Fujita M (2005) An equivalence checking method for C descriptions based on symbolic simulation with textual differences. In: IEICE transactions on fundamentals of electronics, communications and computer sciences, pp 3315\u20133323","DOI":"10.1093\/ietfec\/e88-a.12.3315"},{"key":"9033_CR15","unstructured":"Open SystemC initiative http:\/\/www.systemc.org"},{"key":"9033_CR16","doi-asserted-by":"crossref","unstructured":"Pixley C (1992) A theory and implementation of sequential hardware equivalence. In: IEEE transactions on computer-aided design of integrated circuits and systems","DOI":"10.1109\/43.180261"},{"key":"9033_CR17","doi-asserted-by":"crossref","unstructured":"Pixley C (2001) Formal verification of commercial integrated circuits. In: IEEE design and test of computers","DOI":"10.1109\/MDT.2001.936243"},{"issue":"2","key":"9033_CR18","doi-asserted-by":"crossref","first-page":"156","DOI":"10.1007\/s10009-004-0183-4","volume":"7","author":"MR Prasad","year":"2005","unstructured":"Prasad MR, Biere A, Gupta A (2005) A survey of recent advances in SAT-based formal verification. Softw Test Technol Transf (STTT) 7(2):156\u2013173","journal-title":"Softw Test Technol Transf (STTT)"},{"key":"9033_CR19","doi-asserted-by":"crossref","unstructured":"Smria L, Mehra R, Pangrle B, Ekanayake A, Seawright A, Ng D (2002) RTL C-based methodology for designing and verifying a multi-threaded processor. In: Proceedings of the 39th design automation conference, pp 123\u2013128","DOI":"10.1109\/DAC.2002.1012606"},{"key":"9033_CR20","unstructured":"SystemC reference manual http:\/\/homes.dsi.unimi.it\/~pedersin\/AD\/SystemC_v201_LRM.pdf"},{"key":"9033_CR21","unstructured":"Tu J (2006) Viterbi decoder coprocessor in the DRM application SoC. Masters Report, University of Texas at Austin"},{"key":"9033_CR22","doi-asserted-by":"crossref","unstructured":"van Eijk C (1998) Sequential equivalence checking without state space traversal. In: Proceedings of the IEEE design automation and test in Europe","DOI":"10.1109\/DATE.1998.655922"},{"key":"9033_CR23","unstructured":"van Eijk C, Jess J (1995) Detection of equivalent state variables in finite state machine verification. In: ACM\/IEEE international workshop on logic synthesis, pp 3.35\u20133.44"},{"key":"9033_CR24","doi-asserted-by":"crossref","unstructured":"Vasudevan S, Abraham JA, Viswanath V, Tu J (2006) Automatic decomposition for sequential equivalence checking of system level and RTL descriptions. In: Proceedings of 4th ACM-IEEE international conference on formal methods and models for codesign (MEMOCODE). IEEE, pp 71\u201380","DOI":"10.1109\/MEMCOD.2006.1695903"},{"issue":"10","key":"9033_CR25","doi-asserted-by":"crossref","first-page":"1401","DOI":"10.1109\/TC.2007.1073","volume":"56","author":"S Vasudevan","year":"2007","unstructured":"Vasudevan S, Viswanath V, Sumners RW, Abraham JA (2007) Automatic verification of arithmetic circuits in RTL using stepwise refinement of term rewriting systems. IEEE Trans Comput 56(10):1401\u20131414","journal-title":"IEEE Trans Comput"},{"key":"9033_CR26","doi-asserted-by":"crossref","unstructured":"Viterbi A (1967) Error bounds for convolutional codes and an asymptotically optimum decoding algorithm. In: IEEE transactions on information theory, pp 260\u2013269","DOI":"10.1109\/TIT.1967.1054010"}],"container-title":["Design Automation for Embedded Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10617-008-9033-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10617-008-9033-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10617-008-9033-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,9,24]],"date-time":"2021-09-24T19:02:49Z","timestamp":1632510169000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10617-008-9033-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,11,26]]},"references-count":26,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2008,12]]}},"alternative-id":["9033"],"URL":"https:\/\/doi.org\/10.1007\/s10617-008-9033-z","relation":{},"ISSN":["0929-5585","1572-8080"],"issn-type":[{"value":"0929-5585","type":"print"},{"value":"1572-8080","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,11,26]]}}}