{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:24:15Z","timestamp":1750307055842,"version":"3.41.0"},"reference-count":30,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2012,6,1]],"date-time":"2012-06-01T00:00:00Z","timestamp":1338508800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100002418","name":"Intel Corporation","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100002418","id-type":"DOI","asserted-by":"publisher"}]},{"name":"NOW\/EW project Formal Validation of Deadlock Avoidance Mechanisms","award":["612.064.811"],"award-info":[{"award-number":["612.064.811"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Des. Autom. Electron. Syst."],"published-print":{"date-parts":[[2012,6]]},"abstract":"<jats:p>Cache coherency is one of the major issues in multicore systems. Formal methods, in particular model-checking, have been successful at verifying high-level protocols, but, to the best of our knowledge, the verification of cache coherency at the architectural level is still an open issue. All existing verification efforts assume a reliable interconnect, that is, messages eventually reach their destination. We discuss the challenge of discharging this assumption at the architectural level where implementation details of the interconnect are mixed with a cache coherency protocol. Our automatic approach is based on a well-defined set of primitives to express architectural models, a generic model of communication fabrics expressed in an automated theorem proving system, and a dedicated algorithm for deadlock and livelock detection. We argue that reliability depends on the interaction between the interconnect and the cache coherency protocol. They must be verified altogether as their combination creates intricate message dependencies. We sketch our verification approach and apply it to a simple write-invalidate protocol on the Spidergon network-on-chip from STMicroelectronics. Our approach is promising. For this simple protocol, networks with tens of agents and hundreds of components can be analyzed within seconds.<\/jats:p>","DOI":"10.1145\/2209291.2209293","type":"journal-article","created":{"date-parts":[[2012,8,1]],"date-time":"2012-08-01T17:35:16Z","timestamp":1343842516000},"page":"1-16","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Towards the formal verification of cache coherency at the architectural level"],"prefix":"10.1145","volume":"17","author":[{"given":"Freek","family":"Verbeek","sequence":"first","affiliation":[{"name":"Radboud University Nijmegen, The Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Julien","family":"Schmaltz","sequence":"additional","affiliation":[{"name":"Open University of The Netherlands, The Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2012,7,5]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"Baier C. and Katoen J.-P. 2008. Principles of Model Checking. The MIT Press Cambridge MA.   Baier C. and Katoen J.-P. 2008. Principles of Model Checking. The MIT Press Cambridge MA."},{"key":"e_1_2_1_2_1","doi-asserted-by":"crossref","unstructured":"Baukus K. Lakhnech Y. and Stahl K. 2002. Parameterized verification of a cache coherence protocol: Safety and liveness. In Revised Papers from the 3rd International Workshop on Verification Model Checking and Abstract Interpretation (VMCAI'02). Springer 317--330.   Baukus K. Lakhnech Y. and Stahl K. 2002. Parameterized verification of a cache coherence protocol: Safety and liveness. In Revised Papers from the 3rd International Workshop on Verification Model Checking and Abstract Interpretation (VMCAI'02). Springer 317--330.","DOI":"10.1007\/3-540-47813-2_22"},{"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.1007\/978-3-642-14295-6_29"},{"volume-title":"Proceedings of the High Level Design Validation and Test Workshop (HLDVT'10)","author":"Chatterjee S.","key":"e_1_2_1_5_1"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-010-0092-y"},{"volume-title":"Proceedings of the Conference on Formal Methods in Computer Aided Design (FMCAD'04)","author":"Chou C.","key":"e_1_2_1_7_1"},{"key":"e_1_2_1_8_1","doi-asserted-by":"crossref","unstructured":"Coppola M. Grammatikakis M. Locatelli R. Mariuccia G. and Pieralisi L. 2009. Design of Interconnect Processing Units Spidergon STNoC. CRC Press.   Coppola M. Grammatikakis M. Locatelli R. Mariuccia G. and Pieralisi L. 2009. Design of Interconnect Processing Units Spidergon STNoC. CRC Press.","DOI":"10.1201\/9781420044720"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1987.1676939"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/378239.379048"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/647769.734088"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1026276129010"},{"key":"e_1_2_1_13_1","doi-asserted-by":"crossref","unstructured":"Emerson E.\n     and \n      \n      \n      Kahlon V\n      \n  \n  . \n  2003\n  a. Exact and efficient verification of parameterized cache coherence protocols. In Correct Hardware Design and Verification Methods Lecture Notes in Computer Science vol. \n  2860 Springer Berlin 247--262.  Emerson E. and Kahlon V. 2003a. Exact and efficient verification of parameterized cache coherence protocols. In Correct Hardware Design and Verification Methods Lecture Notes in Computer Science vol. 2860 Springer Berlin 247--262.","DOI":"10.1007\/978-3-540-39724-3_22"},{"key":"e_1_2_1_14_1","doi-asserted-by":"crossref","unstructured":"Emerson E.\n     and \n      \n      \n      Kahlon V\n      \n  \n  . \n  2003\n  b. Rapid parameterized model checking of snoopy cache coherence protocols. In Tools and Algorithms for the Construction and Analysis of Systems H. Garavel and J. Hatcliff Eds. Lecture Notes in Computer Science vol. \n  2619 Springer Berlin 144--159.   Emerson E. and Kahlon V. 2003b. Rapid parameterized model checking of snoopy cache coherence protocols. In Tools and Algorithms for the Construction and Analysis of Systems H. Garavel and J. Hatcliff Eds. Lecture Notes in Computer Science vol. 2619 Springer Berlin 144--159.","DOI":"10.1007\/3-540-36577-X_11"},{"volume-title":"Proceedings of the 12th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'11)","author":"Gotmanov A.","key":"e_1_2_1_15_1"},{"key":"e_1_2_1_16_1","doi-asserted-by":"crossref","unstructured":"Hansson A. Goossens K. and R\u0103dulescu A. 2007. Avoiding message-dependent deadlock in network-based systems on chip. VLSI Des. 07. Article ID 95859.  Hansson A. Goossens K. and R\u0103dulescu A. 2007. Avoiding message-dependent deadlock in network-based systems on chip. VLSI Des. 07. Article ID 95859.","DOI":"10.1155\/2007\/95859"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCD.2005.58"},{"key":"e_1_2_1_18_1","volume-title":"Lecture Notes in Computer Science","volume":"2144","author":"McMillan K.","year":"2001"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/647767.733778"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.191995"},{"volume-title":"Proceedings of the International Conference on Formal Methods in Computer-Aided Design (FMCAD). 172--179","author":"O'Leary J. W.","key":"e_1_2_1_21_1"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/11560548_24"},{"volume-title":"Proceedings of the SIGCHI Conference on Human Factors in Computing Systems (CHI'06)","author":"Park S.","key":"e_1_2_1_23_1"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/277651.277672"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/248621.248624"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/71.879780"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/MDT.2007.38"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2071356.2071357"},{"volume-title":"Proceedings of the Conference on Formal Methods in Computer Aided Design (FMCAD'11)","author":"Verbeek F.","key":"e_1_2_1_29_1"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/MICRO.2010.11"}],"container-title":["ACM Transactions on Design Automation of Electronic Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2209291.2209293","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2209291.2209293","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T09:21:11Z","timestamp":1750238471000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2209291.2209293"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,6]]},"references-count":30,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2012,6]]}},"alternative-id":["10.1145\/2209291.2209293"],"URL":"https:\/\/doi.org\/10.1145\/2209291.2209293","relation":{},"ISSN":["1084-4309","1557-7309"],"issn-type":[{"type":"print","value":"1084-4309"},{"type":"electronic","value":"1557-7309"}],"subject":[],"published":{"date-parts":[[2012,6]]},"assertion":[{"value":"2011-05-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2012-01-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2012-07-05","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}