{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:42:26Z","timestamp":1750308146665,"version":"3.41.0"},"reference-count":21,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2005,10,1]],"date-time":"2005-10-01T00:00:00Z","timestamp":1128124800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Des. Autom. Electron. Syst."],"published-print":{"date-parts":[[2005,10]]},"abstract":"<jats:p>In this article, we present techniques for comparison between behavioral level and register transfer level (RTL) design descriptions by mapping the designs into virtual controllers and virtual datapaths. We also discuss about how the equivalence between behavioral level and RTL designs can be defined precisely using the proposed \u201cattribute statements\u201d in an interactive fashion. Implementation issues as well as considerations on real life industrial design examples are also presented.<\/jats:p>","DOI":"10.1145\/1109118.1109121","type":"journal-article","created":{"date-parts":[[2006,2,6]],"date-time":"2006-02-06T15:07:09Z","timestamp":1139238429000},"page":"610-626","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":19,"title":["Equivalence checking between behavioral and RTL descriptions with virtual controllers and datapaths"],"prefix":"10.1145","volume":"10","author":[{"given":"Masahiro","family":"Fujita","sequence":"first","affiliation":[{"name":"University of Tokyo, Tokyo, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2005,10]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Tech. Rep. CECS-TR-03-41. University of California, Irvine","author":"Abdi S.","year":"2003","unstructured":"Abdi , S. , Peng , J. , Yu , H. , Shin , D. , Gerstlauer , A. , Domer , R. , and Gajski , D . 2003 . System-on-Chip Enviornment : Tutorial . Tech. Rep. CECS-TR-03-41. University of California, Irvine , Irvine, CA .]] Abdi, S., Peng, J., Yu, H., Shin, D.,Gerstlauer, A., Domer, R., and Gajski, D. 2003. System-on-Chip Enviornment: Tutorial. Tech. Rep. CECS-TR-03-41. University of California, Irvine, Irvine, CA.]]"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2003.1207453"},{"volume-title":"Proceedings of the Workshop on Advances in Verification.]]","author":"Ball T.","key":"e_1_2_1_3_1","unstructured":"Ball , T. and Rajamani , S. K . 2000. Boolean programs: A model and process for software analysis . In Proceedings of the Workshop on Advances in Verification.]] Ball, T. and Rajamani, S. K. 2000. Boolean programs: A model and process for software analysis. In Proceedings of the Workshop on Advances in Verification.]]"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"e_1_2_1_5_1","first-page":"298","volume-title":"Proceedings of the Conference on Correct Hardware Design and Verification Methods. Lecture Notes in Computer Science","volume":"1703","author":"Clarke E. M.","unstructured":"Clarke , E. M. , Fujita , M. , Rajan , S. P. , Reps , T. , Shankar , S. , and Teitelbaum , T . 1999. Program slicing for VHDL . In Proceedings of the Conference on Correct Hardware Design and Verification Methods. Lecture Notes in Computer Science , vol. 1703 . Springer-Verlag, Berlin, Germany , pp. 298 -- 312 .]] Clarke, E. M., Fujita, M., Rajan, S. P., Reps, T., Shankar, S., and Teitelbaum, T. 1999. Program slicing for VHDL. In Proceedings of the Conference on Correct Hardware Design and Verification Methods. Lecture Notes in Computer Science, vol. 1703. Springer-Verlag, Berlin, Germany, pp. 298--312.]]"},{"key":"e_1_2_1_6_1","first-page":"368","volume-title":"Proceedings of the Design Automation Conference. ACM","author":"Clarke E.","unstructured":"Clarke , E. , Kroening , D. , and Yorav , K . 2003. Behavioral consistency of C and Verilog programs using bounded model checking . In Proceedings of the Design Automation Conference. ACM , New York , pp. 368 -- 371 .]] 10.1145\/775832.775928 Clarke, E., Kroening, D., and Yorav, K. 2003. Behavioral consistency of C and Verilog programs using bounded model checking. In Proceedings of the Design Automation Conference. ACM, New York, pp. 368--371.]] 10.1145\/775832.775928"},{"key":"e_1_2_1_7_1","unstructured":"CodeSurfer. http:\/\/www.grammatech.com\/products\/codesurfer\/.]]  CodeSurfer. http:\/\/www.grammatech.com\/products\/codesurfer\/.]]"},{"key":"e_1_2_1_8_1","first-page":"130","volume-title":"Proceedings of the Design Automation Conference. ACM","author":"Currie D. W.","unstructured":"Currie , D. W. , Hu , A. J. , Rajan , S. , and Fujita , M . 2000. Automatic formal verification of DSP software . In Proceedings of the Design Automation Conference. ACM , New York , pp. 130 -- 135 .]] 10.1145\/337292.337339 Currie, D. W., Hu, A. J., Rajan, S., and Fujita, M. 2000. Automatic formal verification of DSP software. In Proceedings of the Design Automation Conference. ACM, New York, pp. 130--135.]] 10.1145\/337292.337339"},{"key":"e_1_2_1_9_1","first-page":"81","volume-title":"Proceedings of the International Symposium on System Synthesis. ACM","author":"Fujita M.","unstructured":"Fujita , M. and Nakamura , H . 2001. The standard SpecC language . In Proceedings of the International Symposium on System Synthesis. ACM , New York , pp. 81 -- 86 .]] 10.1145\/500001.500019 Fujita, M. and Nakamura, H. 2001. The standard SpecC language. In Proceedings of the International Symposium on System Synthesis. ACM, New York, pp. 81--86.]] 10.1145\/500001.500019"},{"key":"e_1_2_1_10_1","unstructured":"Gajski D. Zhu J. Domer R. Gerstlauer A. and Zhao S. 2000. SpecC: Specification language and Methodology. Kluwer Academic Publishers 336 p. ISBN: 0-7923-7822-9.]]  Gajski D. Zhu J. Domer R. Gerstlauer A. and Zhao S. 2000. SpecC: Specification language and Methodology. Kluwer Academic Publishers 336 p. ISBN: 0-7923-7822-9.]]"},{"key":"e_1_2_1_11_1","first-page":"420","volume-title":"Proceedings of the Automation Conference. ACM","author":"Jain J.","unstructured":"Jain , J. , Mukherjee , R. , and Fujita , M . 1995. Advanced verification technique based on learning . In Proceedings of the Automation Conference. ACM , New York , pp. 420 -- 426 .]] 10.1145\/217474.217564 Jain, J., Mukherjee, R., and Fujita, M. 1995. Advanced verification technique based on learning. In Proceedings of the Automation Conference. ACM, New York, pp. 420--426.]] 10.1145\/217474.217564"},{"key":"e_1_2_1_12_1","first-page":"263","volume-title":"Proceedings of the Design Automation Conference. ACM","author":"Kuehlmann A.","unstructured":"Kuehlmann , A. and Krohm , F . 1995. Equivalence checking using cuts and heaps . In Proceedings of the Design Automation Conference. ACM , New York , pp. 263 -- 268 .]] 10.1145\/266021.266090 Kuehlmann, A. and Krohm, F. 1995. Equivalence checking using cuts and heaps. In Proceedings of the Design Automation Conference. ACM, New York, pp. 263--268.]] 10.1145\/266021.266090"},{"volume-title":"Proceedings of the IASTED International Conference on Advances in Computer Science and Technology. ACTA Press","author":"Matsumoto T.","key":"e_1_2_1_13_1","unstructured":"Matsumoto , T. , Saito , H. , and Fujita , M . 2004. An equivalence checking methods for C descriptions based on symbolic simulation with textual difference . In Proceedings of the IASTED International Conference on Advances in Computer Science and Technology. ACTA Press , Calgary, Canada.]] Matsumoto, T., Saito, H., and Fujita, M. 2004. An equivalence checking methods for C descriptions based on symbolic simulation with textual difference. In Proceedings of the IASTED International Conference on Advances in Computer Science and Technology. ACTA Press, Calgary, Canada.]]"},{"volume-title":"Proceedings of the Design Automation Conference. ACM","author":"Moskewicz M. W.","key":"e_1_2_1_14_1","unstructured":"Moskewicz , M. W. , Madigan , C. F. , Zhao , Y. Zhang , L. and Malik , S . 2001. Chaff: Engineering an efficient SAT solver . In Proceedings of the Design Automation Conference. ACM , New York.]] 10.1145\/378239.379017 Moskewicz, M. W., Madigan, C. F., Zhao, Y. Zhang, L. and Malik, S. 2001. Chaff: Engineering an efficient SAT solver. In Proceedings of the Design Automation Conference. ACM, New York.]] 10.1145\/378239.379017"},{"key":"e_1_2_1_16_1","first-page":"234","volume-title":"Proceedings of the Conference on Correct Hardware Design and Verification Methods. Lecture Notes in Computer Science","volume":"1703","author":"Ritter G.","unstructured":"Ritter , G. , Eveking , H. , and Hinrichsen , H . 1999. Formal verification of designs with complex control by symbolic simulation . In Proceedings of the Conference on Correct Hardware Design and Verification Methods. Lecture Notes in Computer Science , vol. 1703 , Springer-Verlag, Berlin, Germany , pp. 234 -- 249 .]] Ritter, G., Eveking, H., and Hinrichsen, H. 1999. Formal verification of designs with complex control by symbolic simulation. In Proceedings of the Conference on Correct Hardware Design and Verification Methods. Lecture Notes in Computer Science, vol. 1703, Springer-Verlag, Berlin, Germany, pp. 234--249.]]"},{"key":"e_1_2_1_17_1","first-page":"123","volume-title":"Proceedings of the Design Automation Conference. ACM","author":"Semeria L.","unstructured":"Semeria , L. , Seawright , A. , Mehra , R. , Ng , D. , Ekanayake , A. , and Pangrle , B . 2002. C-based RTL methodology for designing and verifying a multi-threaded processor . In Proceedings of the Design Automation Conference. ACM , New York , pp. 123 -- 128 .]] 10.1145\/513918.513951 Semeria, L., Seawright, A., Mehra, R., Ng, D., Ekanayake, A., and Pangrle, B. 2002. C-based RTL methodology for designing and verifying a multi-threaded processor. In Proceedings of the Design Automation Conference. ACM, New York, pp. 123--128.]] 10.1145\/513918.513951"},{"key":"e_1_2_1_18_1","unstructured":"SpecC. http:\/\/www.cecs.uci.edu\/~specc\/.]]  SpecC. http:\/\/www.cecs.uci.edu\/~specc\/.]]"},{"volume-title":"University of California","author":"So C","key":"e_1_2_1_19_1","unstructured":"So C Environment . University of California , Irvine , Irvine, CA . http:\/\/www.cecs.uci.edu\/~cad\/sce.html.]] SoC Environment. University of California, Irvine, Irvine, CA. http:\/\/www.cecs.uci.edu\/~cad\/sce.html.]]"},{"key":"e_1_2_1_20_1","series-title":"Lecture Notes in Computer Science","volume-title":"CVC: A Cooperating Validity Checker. In Proceedings of the of International Conference on Computer-Aided Verification","author":"Stump A.","year":"2002","unstructured":"Stump , A. , Barret , C. , and Dill , D . 2002 . CVC: A Cooperating Validity Checker. In Proceedings of the of International Conference on Computer-Aided Verification . Lecture Notes in Computer Science , vol. 2404 , Springer-Verlag , Berlin, Germany .]] Stump, A., Barret, C., and Dill, D. 2002. CVC: A Cooperating Validity Checker. In Proceedings of the of International Conference on Computer-Aided Verification. Lecture Notes in Computer Science, vol. 2404, Springer-Verlag, Berlin, Germany.]]"},{"volume-title":"Proceedings of the IASTED International Conference on Advances in Computer Science and Technology. ACTA Press","author":"Tanabe K.","key":"e_1_2_1_21_1","unstructured":"Tanabe , K. , Sasaki , S. , and Fujita , M . 2004. Program slicing for system level designs in SpecC . In Proceedings of the IASTED International Conference on Advances in Computer Science and Technology. ACTA Press , Calgary, Canada.]] Tanabe, K., Sasaki, S., and Fujita, M. 2004. Program slicing for system level designs in SpecC. In Proceedings of the IASTED International Conference on Advances in Computer Science and Technology. ACTA Press, Calgary, Canada.]]"},{"key":"e_1_2_1_22_1","volume-title":"Program Slices: Formal, Psychological, and Practical Investigations of an Automatic Program Abstraction","author":"Weiser M.","year":"1979","unstructured":"Weiser , M. 1979 . Program Slices: Formal, Psychological, and Practical Investigations of an Automatic Program Abstraction . ACM , New York .]] Weiser, M. 1979. Program Slices: Formal, Psychological, and Practical Investigations of an Automatic Program Abstraction. ACM, New York.]]"}],"container-title":["ACM Transactions on Design Automation of Electronic Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1109118.1109121","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1109118.1109121","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T16:18:38Z","timestamp":1750263518000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1109118.1109121"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,10]]},"references-count":21,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2005,10]]}},"alternative-id":["10.1145\/1109118.1109121"],"URL":"https:\/\/doi.org\/10.1145\/1109118.1109121","relation":{},"ISSN":["1084-4309","1557-7309"],"issn-type":[{"type":"print","value":"1084-4309"},{"type":"electronic","value":"1557-7309"}],"subject":[],"published":{"date-parts":[[2005,10]]},"assertion":[{"value":"2005-10-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}