{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:25:21Z","timestamp":1750307121074,"version":"3.41.0"},"reference-count":36,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100003246","name":"Nederlandse Organisatie voor Wetenschappelijk Onderzoek","doi-asserted-by":"publisher","award":["612.064.811"],"award-info":[{"award-number":["612.064.811"]}],"id":[{"id":"10.13039\/501100003246","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":[[2012,1]]},"abstract":"<jats:p>This article presents a formal specification and validation environment to prove safety and liveness properties of parametric -- unbounded -- NoCs architectures described at a high-level of abstraction. The environment improves the GeNoC approach with two new theorems, proving evacuation and starvation freedom. The application of the validation methodology is illustrated on a HERMES NoC with adaptive west-first routing and wormhole switching. This case study illustrates the strong compositional aspect of the GeNoC environment. The complete specification of this HERMES instance, together with the proof that the specification is deadlock-free, starvation free, and all messages eventually leave the network at their correct destination, could be achieved in about a week. Approximately 86% of this proof is automatically derived from the GeNoC model.<\/jats:p>","DOI":"10.1145\/2071356.2071357","type":"journal-article","created":{"date-parts":[[2012,1,31]],"date-time":"2012-01-31T14:49:20Z","timestamp":1328021360000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["Easy Formal Specification and Validation of Unbounded Networks-on-Chips Architectures"],"prefix":"10.1145","volume":"17","author":[{"given":"Freek","family":"Verbeek","sequence":"first","affiliation":[{"name":"Radboud University Nijmegen"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Julien","family":"Schmaltz","sequence":"additional","affiliation":[{"name":"Open University of The Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2012,1]]},"reference":[{"volume-title":"Computer Laboratory","author":"Amjad H.","key":"e_1_2_1_1_1","unstructured":"Amjad , H. 2004. Model checking the AMBA protocol in HOL. Tech. rep ., Computer Laboratory , University of Cambridge . Amjad, H. 2004. Model checking the AMBA protocol in HOL. Tech. rep., Computer Laboratory, University of Cambridge."},{"key":"e_1_2_1_2_1","volume-title":"-P","author":"Baier C.","year":"2008","unstructured":"Baier , C. and Katoen , J . -P . 2008 . Principles of Model Checking. MIT Press . Cambridge, MA. Baier, C. and Katoen, J.-P. 2008. Principles of Model Checking. MIT Press. Cambridge, MA."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.976921"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/NOCS.2007.1"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1404371.1404421"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1155\/2009\/548324"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_29"},{"volume-title":"Proceedings of the High Level Design Validation and Test Workshop (HLDVT\u201910)","author":"Chatterjee S.","key":"e_1_2_1_8_1","unstructured":"Chatterjee , S. , Kishinevsky , M. , and Ogras , U . 2010. Quick formal modeling of communication fabrics to enable verification . In Proceedings of the High Level Design Validation and Test Workshop (HLDVT\u201910) . 42--49. Chatterjee, S., Kishinevsky, M., and Ogras, U. 2010. Quick formal modeling of communication fabrics to enable verification. In Proceedings of the High Level Design Validation and Test Workshop (HLDVT\u201910). 42--49."},{"key":"e_1_2_1_9_1","unstructured":"Cormen T. Leiserson C. and Rivest R. 1990. Introduction to Algorithms. MIT Press and McGraw Hill. Cormen T. Leiserson C. and Rivest R. 1990. Introduction to Algorithms . MIT Press and McGraw Hill."},{"key":"e_1_2_1_10_1","volume-title":"Proceedings of the Design Automation Conference (DAC\u201909)","author":"Dally W.","year":"2009","unstructured":"Dally , W. 2009 . The end of denial architecture . In Proceedings of the Design Automation Conference (DAC\u201909) . Dally, W. 2009. The end of denial architecture. In Proceedings of the Design Automation Conference (DAC\u201909)."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1987.1676939"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/378239.379048"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/71.473515"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/71.532115"},{"key":"e_1_2_1_15_1","unstructured":"Duato J. Yalamanchili S. and Ni L. 2003. Interconnection Networks An Engineering Approach. Morgan Kaufmann. Duato J. Yalamanchili S. and Ni L. 2003. Interconnection Networks An Engineering Approach . Morgan Kaufmann."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/71.707539"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/11560548_28"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/185675.185682"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02311228"},{"volume-title":"Proceedings of the IEEE Symposium on Design and Diagnostics of Electronic System (DDECS\u201910)","author":"Helmy A.","key":"e_1_2_1_20_1","unstructured":"Helmy , A. , Pierre , L. , and Jantsch , A . 2010. Theorem proving techniques for the formal verification of NoC communications with non-minimal adaptive routing . In Proceedings of the IEEE Symposium on Design and Diagnostics of Electronic System (DDECS\u201910) . Helmy, A., Pierre, L., and Jantsch, A. 2010. Theorem proving techniques for the formal verification of NoC communications with non-minimal adaptive routing. In Proceedings of the IEEE Symposium on Design and Diagnostics of Electronic System (DDECS\u201910)."},{"key":"e_1_2_1_21_1","doi-asserted-by":"crossref","unstructured":"Kaufmann M. Manolios P. and Moore J. S. 2000. ACL2 Computer-Aided Reasoning: An Approach. Kluwer Academic Press. Kaufmann M. Manolios P. and Moore J. S. 2000. ACL2 Computer-Aided Reasoning: An Approach. Kluwer Academic Press.","DOI":"10.1007\/978-1-4757-3188-0"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/43.898830"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.vlsi.2004.03.003"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.191995"},{"volume-title":"Proceedings of the Design Automation and Test Europe Conference (DATE\u201903)","author":"Roychoudhury A.","key":"e_1_2_1_25_1","unstructured":"Roychoudhury , A. , Mitra , T. , and Karri , S . 2003. Using formal techniques to debug the AMBA System-on-Chip bus protocol . In Proceedings of the Design Automation and Test Europe Conference (DATE\u201903) . 828--833. Roychoudhury, A., Mitra, T., and Karri, S. 2003. Using formal techniques to debug the AMBA System-on-Chip bus protocol. In Proceedings of the Design Automation and Test Europe Conference (DATE\u201903). 828--833."},{"key":"e_1_2_1_27_1","volume-title":"Proceedings of Formal Methods in Computer-Aided Design (FMCAD\u201904)","volume":"3312","author":"Schmaltz J.","unstructured":"Schmaltz , J. and Borrione , D . 2004. A functional approach to the formal specification of networks on chip . In Proceedings of Formal Methods in Computer-Aided Design (FMCAD\u201904) . Lecture Notes in Computer Science , vol. 3312 , A. Hu and A. Martin Eds., Springer, Berlin, 52--66. Schmaltz, J. and Borrione, D. 2004. A functional approach to the formal specification of networks on chip. In Proceedings of Formal Methods in Computer-Aided Design (FMCAD\u201904). Lecture Notes in Computer Science, vol. 3312, A. Hu and A. Martin Eds., Springer, Berlin, 52--66."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1217975.1217985"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-007-0049-0"},{"volume-title":"Proceedings of the 1st International Workshop on Communication and Architectural Support for Network-Based Parallel Computing (CANPC\u201997)","author":"Silla F.","key":"e_1_2_1_30_1","unstructured":"Silla , F. , Malumbres , M. P. , Robles , A. , Lopez , P. , and Duato , J . 1997. Efficient adaptive routing in networks of workstations with irregular topology . In Proceedings of the 1st International Workshop on Communication and Architectural Support for Network-Based Parallel Computing (CANPC\u201997) . Springer, Berlin, 46--60. Silla, F., Malumbres, M. P., Robles, A., Lopez, P., and Duato, J. 1997. Efficient adaptive routing in networks of workstations with irregular topology. In Proceedings of the 1st International Workshop on Communication and Architectural Support for Network-Based Parallel Computing (CANPC\u201997). Springer, Berlin, 46--60."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/PDP.2010.19"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14052-5_7"},{"volume-title":"Proceedings of the Design, Automation and Test in Europe Conference (DATE). 1701--1706","author":"Verbeek F.","key":"e_1_2_1_33_1","unstructured":"Verbeek , F. and Schmaltz , J . 2010b. Formal specification of networks-on-chips: Deadlock and evacuation . In Proceedings of the Design, Automation and Test in Europe Conference (DATE). 1701--1706 . Verbeek, F. and Schmaltz, J. 2010b. Formal specification of networks-on-chips: Deadlock and evacuation. In Proceedings of the Design, Automation and Test in Europe Conference (DATE). 1701--1706."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-010-9206-x"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/TPDS.2011.16"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/PDP.2011.23"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/TPDS.2011.60"}],"container-title":["ACM Transactions on Design Automation of Electronic Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2071356.2071357","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2071356.2071357","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T09:48:24Z","timestamp":1750240104000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2071356.2071357"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,1]]},"references-count":36,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2012,1]]}},"alternative-id":["10.1145\/2071356.2071357"],"URL":"https:\/\/doi.org\/10.1145\/2071356.2071357","relation":{},"ISSN":["1084-4309","1557-7309"],"issn-type":[{"type":"print","value":"1084-4309"},{"type":"electronic","value":"1557-7309"}],"subject":[],"published":{"date-parts":[[2012,1]]},"assertion":[{"value":"2010-12-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2011-07-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2012-01-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}