{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:33:33Z","timestamp":1750307613568,"version":"3.41.0"},"reference-count":23,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2009,3,1]],"date-time":"2009-03-01T00:00:00Z","timestamp":1235865600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000923","name":"Australian Research Council","doi-asserted-by":"publisher","award":["2005-2008"],"award-info":[{"award-number":["2005-2008"]}],"id":[{"id":"10.13039\/501100000923","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":[[2009,3]]},"abstract":"<jats:p>Hardware module reuse is a standard solution to the problems of increasing complexity of chip architectures and pressure to reduce time to market. In the absence of a single module interface standard, predesigned modules for \u201cplug-and-play\u201d usually require a converter between incompatible interface protocols. Current approaches to automatic synthesis of protocol converters mostly lack formal foundations and either employ abstractions far removed from the HDL implementation level or grossly simplify the structure of the protocols considered. This work presents a state-machine-based formalism for modeling bus-based communication protocols and a notion of protocol compatibility and of correct conversion between incompatible protocols. This formalism is used to derive algorithms for checking protocol compatibility and for provably correct, automatic converter synthesis. Experiments with automatic converter synthesis between different configurations of widely used commercial bus protocols, such as AMBA AHB, ASB APB, and the Open Core Protocol (OCP) are discussed. The work here is unique in its combination of a completely formal approach and the use of a low abstraction level that enables precise modeling of protocol characteristics that is also close to HDL.<\/jats:p>","DOI":"10.1145\/1497561.1497562","type":"journal-article","created":{"date-parts":[[2009,4,6]],"date-time":"2009-04-06T16:34:22Z","timestamp":1239035662000},"page":"1-41","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["Provably correct on-chip communication"],"prefix":"10.1145","volume":"14","author":[{"given":"K.","family":"Avnit","sequence":"first","affiliation":[{"name":"University of New South Wales"}]},{"given":"V.","family":"D'silva","sequence":"additional","affiliation":[{"name":"Oxford University"}]},{"given":"A.","family":"Sowmya","sequence":"additional","affiliation":[{"name":"University of New South Wales"}]},{"given":"S.","family":"Ramesh","sequence":"additional","affiliation":[{"name":"GM India Science Lab"}]},{"given":"S.","family":"Parameswaran","sequence":"additional","affiliation":[{"name":"University of New South Wales"}]}],"member":"320","published-online":{"date-parts":[[2009,4,7]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Proceedings of the Canadian Conference on Electrical and Computer Engineering.","volume":"4","author":"Abdel-Hamid A.","year":"1907","unstructured":"Abdel-Hamid , A. , Zaki , M. , and Tahar , S . 2004. A tool converting finite state machine to VHDL . In Proceedings of the Canadian Conference on Electrical and Computer Engineering. Vol. 4 , 1907 --1910. Abdel-Hamid, A., Zaki, M., and Tahar, S. 2004. A tool converting finite state machine to VHDL. In Proceedings of the Canadian Conference on Electrical and Computer Engineering. Vol. 4, 1907--1910."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/645460.654222"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1049\/ip-cdt:20041100"},{"key":"e_1_2_1_4_1","unstructured":"ARM. 1999. AMBA specification. http:\/\/www.arm.com\/.  ARM. 1999. AMBA specification. http:\/\/www.arm.com\/."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1403375.1403447"},{"key":"e_1_2_1_6_1","doi-asserted-by":"crossref","unstructured":"Davey B. and Priestley H. 2002. Introduction to Lattices and Order. Cambridge University Press.  Davey B. and Priestley H. 2002. Introduction to Lattices and Order. Cambridge University Press.","DOI":"10.1017\/CBO9780511809088"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2003.819385"},{"volume-title":"Proceedings of the 17th International Conference on VLSI Design. 189--194","author":"D'Silva V.","key":"e_1_2_1_8_1","unstructured":"D'Silva , V. , Ramesh , S. , and Sowmya , A . 2004. Bridge over troubled wrappers: Automated interface synthesis . In Proceedings of the 17th International Conference on VLSI Design. 189--194 . D'Silva, V., Ramesh, S., and Sowmya, A. 2004. Bridge over troubled wrappers: Automated interface synthesis. In Proceedings of the 17th International Conference on VLSI Design. 189--194."},{"volume-title":"Proceedings of the Computers and Digital Techniques. 390--395","author":"D'Silva V.","key":"e_1_2_1_9_1","unstructured":"D'Silva , V. , Ramesh , S. , and Sowmya , A . 2005. Synchronous protocol automata: A framework for modeling and verification of SoC communication architectures . In Proceedings of the Computers and Digital Techniques. 390--395 . D'Silva, V., Ramesh, S., and Sowmya, A. 2005. Synchronous protocol automata: A framework for modeling and verification of SoC communication architectures. In Proceedings of the Computers and Digital Techniques. 390--395."},{"key":"e_1_2_1_10_1","unstructured":"Gansner E. K. and North S. C. 2002. Drawing graphs with dot. Tech. rep. AT&T Bell Laboratories Murray Hill NJ.  Gansner E. K. and North S. C. 2002. Drawing graphs with dot. Tech. rep. AT&T Bell Laboratories Murray Hill NJ."},{"key":"e_1_2_1_11_1","unstructured":"Gajski D. Cho H. and Abdi S. 2005. General transducer architecture. Tech. rep. TR 05-08 CECS Center for Embedded Computer Systems University of California Irvine.  Gajski D. Cho H. and Abdi S. 2005. General transducer architecture. Tech. rep. TR 05-08 CECS Center for Embedded Computer Systems University of California Irvine."},{"key":"e_1_2_1_12_1","unstructured":"Lee E. A. The Ptolemy project. http:\/\/ptolemy.eecs.berkeley.edu\/.  Lee E. A. The Ptolemy project. http:\/\/ptolemy.eecs.berkeley.edu\/."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1255456.1255470"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/TVLSI.2008.2000344"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/217474.217572"},{"key":"e_1_2_1_16_1","unstructured":"OCPIP. 2005. Open Core Protocol International Partnership. http:\/\/www.ocpip.org.  OCPIP. 2005. Open Core Protocol International Partnership. http:\/\/www.ocpip.org."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/774572.774592"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/277044.277047"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2003.819898"},{"key":"e_1_2_1_20_1","unstructured":"Shin D. and Gajski D. 2002. Interface synthesis from protocol specification. Tech. rep. CECS-02-13 Center for Embedded Computer Systems University of California Irvine. dongwans gajski@cecs.uci.edu.  Shin D. and Gajski D. 2002. Interface synthesis from protocol specification. Tech. rep. CECS-02-13 Center for Embedded Computer Systems University of California Irvine. dongwans gajski@cecs.uci.edu."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/277044.277048"},{"key":"e_1_2_1_22_1","unstructured":"Sonics. Smart interconnects. http:\/\/www.sonicsinc.com\/.  Sonics. Smart interconnects. http:\/\/www.sonicsinc.com\/."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASPDAC.2007.357999"}],"container-title":["ACM Transactions on Design Automation of Electronic Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1497561.1497562","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1497561.1497562","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T12:45:43Z","timestamp":1750250743000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1497561.1497562"}},"subtitle":["A formal approach to automatic protocol converter synthesis"],"short-title":[],"issued":{"date-parts":[[2009,3]]},"references-count":23,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2009,3]]}},"alternative-id":["10.1145\/1497561.1497562"],"URL":"https:\/\/doi.org\/10.1145\/1497561.1497562","relation":{},"ISSN":["1084-4309","1557-7309"],"issn-type":[{"type":"print","value":"1084-4309"},{"type":"electronic","value":"1557-7309"}],"subject":[],"published":{"date-parts":[[2009,3]]},"assertion":[{"value":"2008-05-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2008-10-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2009-04-07","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}