{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:36:39Z","timestamp":1750307799424,"version":"3.41.0"},"reference-count":36,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2008,7,1]],"date-time":"2008-07-01T00:00:00Z","timestamp":1214870400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100004965","name":"Sixth Framework Programme","doi-asserted-by":"publisher","award":["FP6-2005-IST-5-033709"],"award-info":[{"award-number":["FP6-2005-IST-5-033709"]}],"id":[{"id":"10.13039\/501100004965","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Des. Autom. Electron. Syst."],"published-print":{"date-parts":[[2008,7]]},"abstract":"<jats:p>In transaction-level modeling (TLM), verification methodologies based on transactions allow testbenches, properties, and IP cores in mixed TL-RTL designs to be reused. However, no papers in the literature analyze the effectiveness of transaction-based verification (TBV) in comparison to the more traditional RTL approach. The first contribution of this article is the introduction of a functional-fault-model-based methodology for demonstrating the effectiveness of reuse through TBV. A second contribution is the introduction of a similar methodology for efficient property checking which identifies and removes redundant properties prior to assertion-based verification or model checking.<\/jats:p>","DOI":"10.1145\/1367045.1367056","type":"journal-article","created":{"date-parts":[[2008,7,29]],"date-time":"2008-07-29T13:22:19Z","timestamp":1217337739000},"page":"1-22","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Reuse and optimization of testbenches and properties in a TLM-to-RTL design flow"],"prefix":"10.1145","volume":"13","author":[{"given":"Nicola","family":"Bombieri","sequence":"first","affiliation":[{"name":"Universit\u00e0 di Verona, Verona, Italy"}]},{"given":"Franco","family":"Fummi","sequence":"additional","affiliation":[{"name":"Universit\u00e0 di Verona, Verona, Italy"}]},{"given":"Graziano","family":"Pravadelli","sequence":"additional","affiliation":[{"name":"Universit\u00e0 di Verona, Verona, Italy"}]}],"member":"320","published-online":{"date-parts":[[2008,7,25]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Proceedings of the International Conference on Computer-Aided Verification (CAV). Lecture Notes in Computer Science","volume":"1855","author":"Abarbanel Y.","unstructured":"Abarbanel , Y. , Beer , I. , Gluhovsky , L. , Keidar , S. , and Wolfsthal , Y . 2000. Focs\u2014automatic generation of simulation checkers from formal specifications . In Proceedings of the International Conference on Computer-Aided Verification (CAV). Lecture Notes in Computer Science , vol. 1855 . Springer, 538--542.]] Abarbanel, Y., Beer, I., Gluhovsky, L., Keidar, S., and Wolfsthal, Y. 2000. Focs\u2014automatic generation of simulation checkers from formal specifications. In Proceedings of the International Conference on Computer-Aided Verification (CAV). Lecture Notes in Computer Science, vol. 1855. Springer, 538--542.]]"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/996566.996579"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/240518.240642"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/MTV.2005.15"},{"key":"e_1_2_1_5_1","volume-title":"Tech. Rep. CDNL-TR-2000-0825, Cadence Berkeley Labs.]]","author":"Brahme D.","year":"2000","unstructured":"Brahme , D. , Cox , S. , Gallo , J. , Glasser , M. , Grundmann , W. , Norris Ip , C. , Paulsen , W. , Pierce , J. , Rose , J. , Shea , D. , and Whiting , K . 2000 . The transaction-based verification methodology. Tech. Rep. CDNL-TR-2000-0825, Cadence Berkeley Labs.]] Brahme, D., Cox, S., Gallo, J., Glasser, M., Grundmann, W., Norris Ip, C., Paulsen, W., Pierce, J., Rose, J., Shea, D., and Whiting, K. 2000. The transaction-based verification methodology. Tech. Rep. CDNL-TR-2000-0825, Cadence Berkeley Labs.]]"},{"volume-title":"Digital Systems Testing and Testable Design","author":"Breuer M.","key":"e_1_2_1_6_1","unstructured":"Breuer , M. , Abramovici , M. , and Friedman ., A. 1990. Digital Systems Testing and Testable Design . IEEE Press .]] Breuer, M., Abramovici, M., and Friedman., A. 1990. Digital Systems Testing and Testable Design. IEEE Press.]]"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/944645.944651"},{"volume-title":"Proceedings of the IEEE International Conference on Computer-Aided Design (ICCAD), 226--229","author":"Cheng K.-T.","key":"e_1_2_1_8_1","unstructured":"Cheng , K.-T. and Jou , J . -Y. 1990. A single-state-transition fault model for sequential machines . In Proceedings of the IEEE International Conference on Computer-Aided Design (ICCAD), 226--229 .]] Cheng, K.-T. and Jou, J.-Y. 1990. A single-state-transition fault model for sequential machines. In Proceedings of the IEEE International Conference on Computer-Aided Design (ICCAD), 226--229.]]"},{"volume-title":"Proceedigs of the International Conference on Computer-Aided Verification (CAV), 66--78","author":"Chockler H.","key":"e_1_2_1_9_1","unstructured":"Chockler , H. , Kupferman , O. , Kurshan , R. P. , and Vardi , M. Y . 2001. A practical approach to coverage in model checking . In Proceedigs of the International Conference on Computer-Aided Verification (CAV), 66--78 .]] Chockler, H., Kupferman, O., Kurshan, R. P., and Vardi, M. Y. 2001. A practical approach to coverage in model checking. In Proceedigs of the International Conference on Computer-Aided Verification (CAV), 66--78.]]"},{"key":"e_1_2_1_10_1","unstructured":"Clarke E. Grumberg D. and Peled D. 2000. Model Checking. MIT Press.]]  Clarke E. Grumberg D. and Peled D. 2000. Model Checking. MIT Press.]]"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/217474.217565"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(85)90001-7"},{"volume-title":"Proceedings of the ACM\/IEEE International Conference on Formal Methods and Models for Codesign, (MEMOCODE). 145--152","author":"Fedeli A.","key":"e_1_2_1_13_1","unstructured":"Fedeli , A. , Fummi , F. , Pravadelli , G. , Rossi , U. , and Toto , F . 2003. On the use of a high-level fault model to check properties incompleteness . In Proceedings of the ACM\/IEEE International Conference on Formal Methods and Models for Codesign, (MEMOCODE). 145--152 .]] Fedeli, A., Fummi, F., Pravadelli, G., Rossi, U., and Toto, F. 2003. On the use of a high-level fault model to check properties incompleteness. In Proceedings of the ACM\/IEEE International Conference on Formal Methods and Models for Codesign, (MEMOCODE). 145--152.]]"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/307418.307541"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/TR.2003.821926"},{"key":"e_1_2_1_16_1","doi-asserted-by":"crossref","unstructured":"Foster H. D. Krolnik A. C. and Lacey D. J. 2004. Assertion-Based Design. Springer Academic The Netherlands.]]   Foster H. D. Krolnik A. C. and Lacey D. J. 2004. Assertion-Based Design. Springer Academic The Netherlands.]]","DOI":"10.1007\/b117047"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/ETS.2005.12"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00133499"},{"key":"e_1_2_1_19_1","unstructured":"Hachtel G. D. and Somenzi F. 1996. Logic Synthesis and Verification Algorithms. Kluwer Academic.]]   Hachtel G. D. and Somenzi F. 1996. Logic Synthesis and Verification Algorithms. Kluwer Academic.]]"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/309847.309936"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/775832.775908"},{"volume-title":"Proceedings of the IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE). 199--203","author":"Jindal R.","key":"e_1_2_1_22_1","unstructured":"Jindal , R. and Jain , K . 2003. Verification of transaction-level systemc models using RTL testbenches . In Proceedings of the IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE). 199--203 .]] Jindal, R. and Jain, K. 2003. Verification of transaction-level systemc models using RTL testbenches. In Proceedings of the IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE). 199--203.]]"},{"volume-title":"Proceedings of the IFIP Correct Hardware Design and Verification Methods (CHARME). 280--297","author":"Katz S.","key":"e_1_2_1_23_1","unstructured":"Katz , S. , Grumberg , O. , and Geist , D . 1999. Have I written enough properties&quest; A method of comparison between specification and implementation . In Proceedings of the IFIP Correct Hardware Design and Verification Methods (CHARME). 280--297 .]] Katz, S., Grumberg, O., and Geist, D. 1999. Have I written enough properties&quest; A method of comparison between specification and implementation. In Proceedings of the IFIP Correct Hardware Design and Verification Methods (CHARME). 280--297.]]"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/996566.996580"},{"key":"e_1_2_1_25_1","volume-title":"-A","author":"Lee T.-C.","year":"2004","unstructured":"Lee , T.-C. and Hsiung , P . -A . 2004 . Mutation coverage estimation for model checking. In Proceedings of the International Symposium on Automated Technology for Verification and Analysis. Lecture Notes in Computer Science, vol. 3299 . Springer , 534--368.]] Lee, T.-C. and Hsiung, P.-A. 2004. Mutation coverage estimation for model checking. In Proceedings of the International Symposium on Automated Technology for Verification and Analysis. Lecture Notes in Computer Science, vol. 3299. Springer, 534--368.]]"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/8.1.55"},{"volume-title":"Symbolic Model Checking","author":"McMillan K. L.","key":"e_1_2_1_27_1","unstructured":"McMillan , K. L. 1993. Symbolic Model Checking . Kluwer Academic , Norwell, MA .]] McMillan, K. L. 1993. Symbolic Model Checking. Kluwer Academic, Norwell, MA.]]"},{"volume-title":"The Art of Software Testing","author":"Myers G.","key":"e_1_2_1_28_1","unstructured":"Myers , G. 1979. The Art of Software Testing . Wiley Interscience , New York .]] Myers, G. 1979. The Art of Software Testing. Wiley Interscience, New York.]]"},{"key":"e_1_2_1_29_1","unstructured":"Norris Ip C. and Swan S. 2003. A tutorial introduction on the new systemc verification standard. White paper. www.systemc.org.]]  Norris Ip C. and Swan S. 2003. A tutorial introduction on the new systemc verification standard. White paper. www.systemc.org.]]"},{"key":"e_1_2_1_30_1","unstructured":"Politecnico di Torino. 1999. ITC-99 benchmarks. In http:\/\/www.cad.polito.it\/tools\/itc99.html.]]  Politecnico di Torino. 1999. ITC-99 benchmarks. In http:\/\/www.cad.polito.it\/tools\/itc99.html.]]"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.2307\/2695091"},{"key":"e_1_2_1_32_1","volume-title":"-M","author":"Rose A.","year":"2004","unstructured":"Rose , A. , Swan , S. , Pierce , J. , and Fernandez , J . -M . 2004 . Transaction level modeling in systemC. White paper. www.systemc.org.]] Rose, A., Swan, S., Pierce, J., and Fernandez, J.-M. 2004. Transaction level modeling in systemC. White paper. www.systemc.org.]]"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/787267.787958"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1118299.1118411"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1118299.1118303"},{"volume-title":"Proceedings of the IEEE International Symposium on Circuits and Systems (ISCAS). 5850--5853","author":"Zhong","key":"e_1_2_1_36_1","unstructured":"Zhong -hai, W. and Yi -zheng, Y . 2005. The improvement for transaction level verification functional coverage . In Proceedings of the IEEE International Symposium on Circuits and Systems (ISCAS). 5850--5853 .]] Zhong-hai, W. and Yi-zheng, Y. 2005. The improvement for transaction level verification functional coverage. In Proceedings of the IEEE International Symposium on Circuits and Systems (ISCAS). 5850--5853.]]"}],"container-title":["ACM Transactions on Design Automation of Electronic Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1367045.1367056","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1367045.1367056","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:56:30Z","timestamp":1750254990000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1367045.1367056"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,7]]},"references-count":36,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2008,7]]}},"alternative-id":["10.1145\/1367045.1367056"],"URL":"https:\/\/doi.org\/10.1145\/1367045.1367056","relation":{},"ISSN":["1084-4309","1557-7309"],"issn-type":[{"type":"print","value":"1084-4309"},{"type":"electronic","value":"1557-7309"}],"subject":[],"published":{"date-parts":[[2008,7]]},"assertion":[{"value":"2005-11-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2007-11-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2008-07-25","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}