{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:15:53Z","timestamp":1750306553562,"version":"3.41.0"},"reference-count":57,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2014,11,18]],"date-time":"2014-11-18T00:00:00Z","timestamp":1416268800000},"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":[[2014,11,18]]},"abstract":"<jats:p>\n            A system-on-chip (SoC) contains numerous intellectual property blocks, or IPs. Protocol mismatches between IPs may affect the system-level functionality of the SoC. Mismatches are addressed by introducing converters to control inter-IP interactions. Current approaches towards converter generation find limited practical application as they use restrictive models, lack formal rigour, handle a small subset of commonly encountered mismatches, and\/or are not scalable. We propose a formal technique for SoC design using\n            <jats:italic>incremental converter synthesis<\/jats:italic>\n            . The proposed formulation provides precise models for protocols and requirements, and provides a scalable algorithm that allows adding multiple components and requirements to an SoC incrementally. We prove that the technique is sound and complete. Experimental results obtained using real-life AMBA benchmarks show the scalability and wide range of mismatches handled by our approach.\n          <\/jats:p>","DOI":"10.1145\/2663344","type":"journal-article","created":{"date-parts":[[2014,11,24]],"date-time":"2014-11-24T15:29:41Z","timestamp":1416842981000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["A Formal Approach to Incremental Converter Synthesis for System-on-Chip Design"],"prefix":"10.1145","volume":"20","author":[{"given":"Roopak","family":"Sinha","sequence":"first","affiliation":[{"name":"University of Technology, New Zealand"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alain","family":"Girault","sequence":"additional","affiliation":[{"name":"INRIA and Universite Grenoble Alpes, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gregor","family":"Goessler","sequence":"additional","affiliation":[{"name":"INRIA and Universite Grenoble Alpes, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Partha S.","family":"Roop","sequence":"additional","affiliation":[{"name":"University of Auckland, New Zealand"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2014,11,18]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/645460.654222"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1049\/ip-cdt:20041100"},{"key":"e_1_2_1_3_1","unstructured":"ARM. 2011. AMBA 4 specifications. www.arm.com.  ARM. 2011. AMBA 4 specifications. www.arm.com."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1497561.1497562"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/832283.835001"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/1397757.1397993"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2002.805826"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/1083592.1083664"},{"key":"e_1_2_1_9_1","first-page":"477","article-title":"Methods and arrangements for automatic synthesis of systems-on-chip","volume":"6","author":"Bergamashi Reinaldo A.","year":"2002","unstructured":"Reinaldo A. Bergamashi , Subhrajit Bhattacharya , Jean-Marc R. Daveau , and William R. Lee . 2002 . Methods and arrangements for automatic synthesis of systems-on-chip . US Patent 6 , 477 ,691. http:\/\/www.google.com\/patents\/US6477691. Reinaldo A. Bergamashi, Subhrajit Bhattacharya, Jean-Marc R. Daveau, and William R. Lee. 2002. Methods and arrangements for automatic synthesis of systems-on-chip. US Patent 6,477,691. http:\/\/www.google.com\/patents\/US6477691.","journal-title":"US Patent"},{"volume-title":"Proceedings of the International Conference on Computer Aided Design (ICCAD'87)","author":"Borriello Gaetano","key":"e_1_2_1_11_1","unstructured":"Gaetano Borriello and Randy H. Katz . 1987. Synthesis and optimization of interface transducer logic . In Proceedings of the International Conference on Computer Aided Design (ICCAD'87) . 481--494. Gaetano Borriello and Randy H. Katz. 1987. Synthesis and optimization of interface transducer logic. In Proceedings of the International Conference on Computer Aided Design (ICCAD'87). 481--494."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02979-0_30"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/1880999.1881064"},{"key":"e_1_2_1_14_1","unstructured":"Krishnendu Chatterjee Tom Henzinger and Nir Piterman. 2006. Algorithms for buchi games. http:\/\/chess.eecs.berkeley.edu\/pubs\/238.html.  Krishnendu Chatterjee Tom Henzinger and Nir Piterman. 2006. Algorithms for buchi games. http:\/\/chess.eecs.berkeley.edu\/pubs\/238.html."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/92.555993"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/503271.503226"},{"volume-title":"Proceedings of the 10th IEEE International Symposium on Asynchronous Circuits and Systems (ASYNC'04)","author":"Dobkin Rostislav","key":"e_1_2_1_17_1","unstructured":"Rostislav Dobkin , Ran Ginosar , and Christos P. Sotiriou . 2004. Data synchronization issues in gals socs . In Proceedings of the 10th IEEE International Symposium on Asynchronous Circuits and Systems (ASYNC'04) . 170--179. Rostislav Dobkin, Ran Ginosar, and Christos P. Sotiriou. 2004. Data synchronization issues in gals socs. In Proceedings of the 10th IEEE International Symposium on Asynchronous Circuits and Systems (ASYNC'04). 170--179."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/962758.963411"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/968878.969073"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1049\/ip-cdt:20045097"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.3182\/20070613-3-FR-4909.00031"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISQED.2010.5450526"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2007.895794"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSC.2010.57"},{"key":"e_1_2_1_25_1","unstructured":"Paul Glover. 2005. Using and creating interrupt-based systems. http:\/\/www.xilinx.com\/support\/documentation\/application_notes\/xapp778.pdf.  Paul Glover. 2005. Using and creating interrupt-based systems. http:\/\/www.xilinx.com\/support\/documentation\/application_notes\/xapp778.pdf."},{"key":"e_1_2_1_26_1","first-page":"5","article-title":"Synthesis of amba ahb from formal specification: A case study","volume":"15","author":"Godhal Yashdeep","year":"2011","unstructured":"Yashdeep Godhal , Krishnendu Chatterjee , and Thomas A. Henzinger . 2011 . Synthesis of amba ahb from formal specification: A case study . Int. J. Softw. Tools Technol. Transfer 15 , 5 -- 6 , 585--601. Yashdeep Godhal, Krishnendu Chatterjee, and Thomas A. Henzinger. 2011. Synthesis of amba ahb from formal specification: A case study. Int. J. Softw. Tools Technol. Transfer 15, 5--6, 585--601.","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCOM.1986.1096529"},{"key":"e_1_2_1_28_1","volume-title":"Councill","author":"Heineman George T.","year":"2001","unstructured":"George T. Heineman and William T . Councill . 2001 . Component-Based Software Engineering: Putting the Pieces Together. Addison-Wesley Longman . George T. Heineman and William T. Councill. 2001. Component-Based Software Engineering: Putting the Pieces Together. Addison-Wesley Longman."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASIC.2002.1158060"},{"volume-title":"Reuse Methodology Manual: For System-on-a-Chip Designs","author":"Keating Michael","key":"e_1_2_1_30_1","unstructured":"Michael Keating and Pierre Bricaud . 2002. Reuse Methodology Manual: For System-on-a-Chip Designs . Springer . Michael Keating and Pierre Bricaud. 2002. Reuse Methodology Manual: For System-on-a-Chip Designs. Springer."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/CACSD.1996.555193"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008258331497"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2893"},{"key":"e_1_2_1_34_1","unstructured":"Mounir Maaref. 2007. Creating an opb ipif-based ip and using it in edk. http:\/\/www.xilinx.com\/support\/documentation\/application_notes\/xapp967.pdf.  Mounir Maaref. 2007. Creating an opb ipif-based ip and using it in edk. http:\/\/www.xilinx.com\/support\/documentation\/application_notes\/xapp967.pdf."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1176887.1176932"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/TII.2009.2026896"},{"volume-title":"Introduction to VLSI Systems","author":"Mead Carver","key":"e_1_2_1_37_1","unstructured":"Carver Mead and Lynn Conway . 1980. Introduction to VLSI Systems . Addison-Wesley . Carver Mead and Lynn Conway. 1980. Introduction to VLSI Systems. Addison-Wesley."},{"volume-title":"Communication and Concurrency","author":"Milner Robin","key":"e_1_2_1_38_1","unstructured":"Robin Milner . 1989. Communication and Concurrency . Prentice-Hall . Robin Milner. 1989. Communication and Concurrency. Prentice-Hall."},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/217474.217572"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/774572.774592"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/277044.277047"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACSD.2009.25"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2006.873611"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/54.970421"},{"key":"e_1_2_1_45_1","first-page":"8","article-title":"Zynq-7000 epp sets stage for new era of innovations","volume":"75","author":"Santarini Mike","year":"2011","unstructured":"Mike Santarini . 2011 . Zynq-7000 epp sets stage for new era of innovations . Xcell J. 75 , 8 -- 13 . Mike Santarini. 2011. Zynq-7000 epp sets stage for new era of innovations. Xcell J. 75, 8--13.","journal-title":"Xcell J."},{"key":"e_1_2_1_46_1","unstructured":"Roopak Sinha. 2009. Automated techniques for formal verification of socs. http:\/\/homepages.engineering.auckland.ac.nz\/~roop\/pub\/phd\/Roopak.pdf.  Roopak Sinha. 2009. Automated techniques for formal verification of socs. http:\/\/homepages.engineering.auckland.ac.nz\/~roop\/pub\/phd\/Roopak.pdf."},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1155\/2008\/296206"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.5555\/1874620.1874650"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.5555\/2492708.2492871"},{"volume-title":"Handbook of Theoretical Computer Science","author":"Thomas Wolfgang","key":"e_1_2_1_50_1","unstructured":"Wolfgang Thomas . 1990. Automata on infinite objects . In Handbook of Theoretical Computer Science , Vol. B, Jan van Leeuwen, Ed., MIT Press, 133-- 191 . Wolfgang Thomas. 1990. Automata on infinite objects. In Handbook of Theoretical Computer Science, Vol. B, Jan van Leeuwen, Ed., MIT Press, 133--191."},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.5555\/1763507.1763528"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629335.1629346"},{"volume-title":"The Linear Time-Branching Time Spectrum","author":"van Glabbeek Rob J.","key":"e_1_2_1_53_1","unstructured":"Rob J. van Glabbeek . 1990. The Linear Time-Branching Time Spectrum . Springer . Rob J. van Glabbeek. 1990. The Linear Time-Branching Time Spectrum. Springer."},{"key":"e_1_2_1_54_1","volume-title":"Proceedings of the 5th IEEE International Symposium on Requirements Engineering (RE'01)","author":"van Lamsweerde Axel","year":"2001","unstructured":"Axel van Lamsweerde . 2001 . Goal-oriented requirements engineering: A guided tour . In Proceedings of the 5th IEEE International Symposium on Requirements Engineering (RE'01) . 249--262. Axel van Lamsweerde. 2001. Goal-oriented requirements engineering: A guided tour. In Proceedings of the 5th IEEE International Symposium on Requirements Engineering (RE'01). 249--262."},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1109\/TII.2005.843829"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASPDAC.2007.357999"},{"volume-title":"Support: IP documentation","year":"2013","key":"e_1_2_1_57_1","unstructured":"Xilinx. 2013 . Support: IP documentation . http:\/\/www.xilinx.com\/support\/index.html\/content\/xilinx\/en\/supportNav\/ip_documentation.html. Xilinx. 2013. Support: IP documentation. http:\/\/www.xilinx.com\/support\/index.html\/content\/xilinx\/en\/supportNav\/ip_documentation.html."},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCOM.1980.1094702"}],"container-title":["ACM Transactions on Design Automation of Electronic Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2663344","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2663344","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T06:12:47Z","timestamp":1750227167000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2663344"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,11,18]]},"references-count":57,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2014,11,18]]}},"alternative-id":["10.1145\/2663344"],"URL":"https:\/\/doi.org\/10.1145\/2663344","relation":{},"ISSN":["1084-4309","1557-7309"],"issn-type":[{"type":"print","value":"1084-4309"},{"type":"electronic","value":"1557-7309"}],"subject":[],"published":{"date-parts":[[2014,11,18]]},"assertion":[{"value":"2013-03-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-08-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-11-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}