{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:12:30Z","timestamp":1750219950785,"version":"3.41.0"},"reference-count":59,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2023,10,16]],"date-time":"2023-10-16T00:00:00Z","timestamp":1697414400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"NSF","award":["1628926"],"award-info":[{"award-number":["1628926"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Des. Autom. Electron. Syst."],"published-print":{"date-parts":[[2023,11,30]]},"abstract":"<jats:p>\n            In modern systems-on-chips, several hardware protocols are used for communication and interaction among different modules. These protocols are complex and need to be implemented correctly for correct operation of the system-on-chip. Therefore, protocol verification has received significant attention. However, this verification is often limited to checking high-level properties on a protocol specification or an implementation. Verifying these properties directly on an implementation faces scalability challenges due to its size and design complexity. Further, even after some high-level properties are verified, there is no guarantee that an implementation fully complies with a given specification, even if the same properties have also been checked on the specification. We address these challenges and gaps by adding a layer of component specifications, one for each component in the protocol implementation, and specifying and verifying the interactions at the interfaces between each pair of communicating components. We use the recently proposed formal model termed\n            <jats:italic>Instruction-Level Abstraction<\/jats:italic>\n            (ILA) as a component specification, which includes an interface specification for the interactions in composing different components. The use of ILA models as component specifications allows us to decompose the complete verification task into two sub-tasks: checking that the composition of ILAs is sequentially equivalent to a verified formal protocol specification, and checking that the protocol implementation is a refinement of the ILA composition. This check requires that each component implementation is a refinement of its ILA specification and includes interface checks guaranteeing that components interact with each other as specified. We have applied the proposed ILA-based methodology for protocol verification to several third-party design case studies. These include an AXI on-chip communication protocol, an off-chip communication protocol, and a cache coherence protocol. For each system, we successfully detected bugs in the implementation, and show that the full formal verification can be completed in reasonable time and effort.\n          <\/jats:p>","DOI":"10.1145\/3610292","type":"journal-article","created":{"date-parts":[[2023,7,24]],"date-time":"2023-07-24T12:15:22Z","timestamp":1690200922000},"page":"1-24","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["SoC Protocol Implementation Verification Using Instruction-Level Abstraction Specifications"],"prefix":"10.1145","volume":"28","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3875-1761","authenticated-orcid":false,"given":"Huaixi","family":"Lu","sequence":"first","affiliation":[{"name":"Princeton University, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7422-3352","authenticated-orcid":false,"given":"Yue","family":"Xing","sequence":"additional","affiliation":[{"name":"Princeton University, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6676-9400","authenticated-orcid":false,"given":"Aarti","family":"Gupta","sequence":"additional","affiliation":[{"name":"Princeton University, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0837-5443","authenticated-orcid":false,"given":"Sharad","family":"Malik","sequence":"additional","affiliation":[{"name":"Princeton University, USA"}]}],"member":"320","published-online":{"date-parts":[[2023,10,16]]},"reference":[{"key":"e_1_3_2_2_2","volume-title":"Proceedings of the International Workshop on Foundations of Computer Security (FCS\u201905)","author":"Agha Gul","year":"2005","unstructured":"Gul Agha, C. Gunter, Michael Greenwald, Sanjeev Khanna, Jose Meseguer, Koushik Sen, and Prasannaa Thati. 2005. Formal modeling and analysis of DoS using probabilistic rewrite theories. In Proceedings of the International Workshop on Foundations of Computer Security (FCS\u201905)."},{"key":"e_1_3_2_3_2","doi-asserted-by":"crossref","unstructured":"Rajeev Alur Thomas A. Henzinger Freddy Y. C. Mang Shaz Qadeer Sriram K. Rajamani and Serdar Tasiran. 1998. MOCHA: Modularity in model checking. In Computer Aided Verification . Lecture Notes in Computer Science Vol. 1427. Springer 521\u2013525.","DOI":"10.1007\/BFb0028774"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/2872362.2872414"},{"key":"e_1_3_2_5_2","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/978-3-642-28641-4_2","volume-title":"Proceedings of the International Conference on Principles of Security and Trust","author":"Blanchet Bruno","year":"2012","unstructured":"Bruno Blanchet. 2012. Security protocol verification: Symbolic and computational models. In Proceedings of the International Conference on Principles of Security and Trust. 3\u201329."},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/1297666.1297670"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/196244.196577"},{"key":"e_1_3_2_8_2","unstructured":"Cadence Design Systems Inc.2018. JasperGold: Formal Property Verification App.Retrieved November 26 2019 from http:\/\/www.jasper-da.com\/products\/jaspergold-apps\/"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.5555\/2677118"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICGCS.2010.5543050"},{"key":"e_1_3_2_11_2","doi-asserted-by":"crossref","unstructured":"Joonwon Choi Muralidaran Vijayaraghavan Benjamin Sherman Adam Chlipala and Arvind. 2017. Kami: A platform for high-level parametric hardware specification and its modular verification. Proceedings of the ACM on Programming Languages 1 ICFP (2017) Article 24 30 pages.","DOI":"10.1145\/3110268"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30494-4_27"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454037"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICCD.1992.276232"},{"key":"e_1_3_2_15_2","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1007\/978-0-387-75462-8_14","volume-title":"Proceedings of the International Conference on Critical Infrastructure Protection","author":"Dutertre Bruno","year":"2007","unstructured":"Bruno Dutertre. 2007. Formal modeling and analysis of the Modbus protocol. In Proceedings of the International Conference on Critical Infrastructure Protection. 189\u2013204."},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/337292.337757"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.4204\/eptcs.316.2"},{"key":"e_1_3_2_18_2","unstructured":"J. Holzmann Gerard. 2003. The Spin Model Checker: Primer and Reference Manual . Addison-Wesley Professional."},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_12"},{"key":"e_1_3_2_20_2","first-page":"310","volume-title":"Proceedings of the 2019 1st International Conference on Advanced Technologies in Intelligent Control, Environment, Computing, and Communication Engineering (ICATIECE\u201919)","author":"Giridhar Perumalla","year":"2019","unstructured":"Perumalla Giridhar and Priyanka Choudhury. 2019. Design and verification of AMBA AHB. In Proceedings of the 2019 1st International Conference on Advanced Technologies in Intelligent Control, Environment, Computing, and Communication Engineering (ICATIECE\u201919). IEEE, Los Alamitos, CA, 310\u2013315."},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.23919\/DATE.2018.8342253"},{"key":"e_1_3_2_22_2","first-page":"1","volume-title":"Proceedings of the 29th International Workshop on Principles of Diagnosis","author":"Hofer Birgit","year":"2018","unstructured":"Birgit Hofer, Radu Mateescu, Wendelin Serwe, and Franz Wotawa. 2018. Using LNT formal descriptions for model-based diagnosis. In Proceedings of the 29th International Workshop on Principles of Diagnosis. 1\u20138."},{"key":"e_1_3_2_23_2","doi-asserted-by":"crossref","unstructured":"Bo Yuan Huang Hongce Zhang Aarti Gupta and Sharad Malik. 2019. ILAng: A modeling and verification platform for SoCs using instruction-level abstractions. In Tools and Algorithms for the Construction and Analysis of Systems . Lecture Notes in Computer Science Vol. 11427. Springer 351\u2013357.","DOI":"10.1007\/978-3-030-17462-0_21"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/3282444"},{"key":"e_1_3_2_25_2","unstructured":"IEEE. 2005. IEEE Standard for Property Specification Language (PSL) . IEEE Standard 1850-2005. IEEE."},{"key":"e_1_3_2_26_2","doi-asserted-by":"crossref","first-page":"396","DOI":"10.1007\/3-540-44585-4_40","volume-title":"Computer Aided Verification","author":"Jhala Ranjit","year":"2001","unstructured":"Ranjit Jhala and Kenneth L. McMillan. 2001. Microarchitecture verification by compositional model checking. In Computer Aided Verification. Lecture Notes in Computer Science, Vol. 2102. Springer, 396\u2013410."},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1022969405325"},{"key":"e_1_3_2_28_2","first-page":"58","volume-title":"Proceedings of the IEEE\/ACM International Conference on Computer Aided Design (ICCAD\u201904).","author":"Khasidashvili Zurab","year":"2004","unstructured":"Zurab Khasidashvili, Marcelo Skaba, Daher Kaiss, and Ziyad Hanna. 2004. Theoretical framework for compositional sequential hardware equivalence verification in presence of design constraints. In Proceedings of the IEEE\/ACM International Conference on Computer Aided Design (ICCAD\u201904). IEEE, Los Alamitos, CA, 58\u201365."},{"key":"e_1_3_2_29_2","unstructured":"Mallory Knodel and Niels ten Oever. 2020. Terminology Power and Inclusive Language. [Online]. Available: https:\/\/datatracker.ietf.org\/doc\/html\/draft-knodel-terminology-02 accessed on: 2023-07."},{"key":"e_1_3_2_30_2","unstructured":"Leslie Lamport. 2002. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers . Addison-Wesley Professional."},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICCD.2016.7753341"},{"key":"e_1_3_2_32_2","first-page":"494","volume-title":"Proceedings of the 1999 IEEE\/ACM International Conference on Computer-Aided Design: Digest of Technical Papers (ICCAD\u201999)","author":"Liu Xiaojun","year":"1999","unstructured":"Xiaojun Liu. 1999. Formal specification and verification of a dataflow processor array. In Proceedings of the 1999 IEEE\/ACM International Conference on Computer-Aided Design: Digest of Technical Papers (ICCAD\u201999). IEEE, Los Alamitos, CA, 494\u2013499."},{"key":"e_1_3_2_33_2","unstructured":"Makai Mann. 2019. AXI Protocol Checker for the OH! Implementation of the AXI Protocol. Retrieved November 26 2019 from https:\/\/github.com\/upscale-project\/case-studies\/tree\/master\/axi"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1109\/TVLSI.2008.918120"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2005.1560183"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2018.8603014"},{"key":"e_1_3_2_37_2","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1007\/3-540-63166-6_6","volume-title":"Computer Aided Verification","author":"McMillan Kenneth L.","year":"1997","unstructured":"Kenneth L. McMillan. 1997. A compositional rule for hardware design refinement. In Computer Aided Verification. Lecture Notes in Computer Science, Vol. 1254. Springer, 24\u201335."},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1109\/MDT.2005.68"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_39"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2008.2006092"},{"key":"e_1_3_2_41_2","first-page":"1","volume-title":"Proceedings of the 2009 Forum on Specification and Design Languages (FDL\u201909)","author":"Nguyen Minh D.","year":"2009","unstructured":"Minh D. Nguyen, Max Thalmaier, Markus Wedler, Dominik Stoffel, Wolfgang Kunz, and J\u00f6rg Bormann. 2009. A re-use methodology for formal SoC protocol compliance verification. In Proceedings of the 2009 Forum on Specification and Design Languages (FDL\u201909). IEEE, Los Alamitos, CA, 1\u20136."},{"key":"e_1_3_2_42_2","first-page":"1","volume-title":"Proceedings of the 2009 Forum on Specification and Design Languages (FDL\u201909)","author":"Nguyen Minh D.","year":"2009","unstructured":"Minh D. Nguyen, Max Thalmaier, Markus Wedler, Dominik Stoffel, Wolfgang Kunz, and J\u00f6rg Bormann. 2009. A re-use methodology for formal SoC protocol compliance verification. In Proceedings of the 2009 Forum on Specification and Design Languages (FDL\u201909). IEEE, Los Alamitos, CA, 1\u20136."},{"key":"e_1_3_2_43_2","first-page":"69","volume-title":"Proceedings of the 2nd ACM\/IEEE International Conference on Formal Methods and Models for Co-Design (MEMCODE\u201904).","author":"Nikhil Rishiyur","year":"2004","unstructured":"Rishiyur Nikhil. 2004. Bluespec System Verilog: Efficient, correct RTL from high level specifications. In Proceedings of the 2nd ACM\/IEEE International Conference on Formal Methods and Models for Co-Design (MEMCODE\u201904). IEEE, Los Alamitos, CA, 69\u201370."},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2009.5351126"},{"key":"e_1_3_2_45_2","unstructured":"Andreas Olofsson Roman Trogan Fred Huettig Ola Jeppsson and Peter Saunderson. 2016. Epiphany eLink AXI. Retrieved November 26 2019 from https:\/\/github.com\/aolofsson\/oh\/tree\/master\/axi"},{"key":"e_1_3_2_46_2","first-page":"75","volume-title":"Proceedings of the 14th International Symposium on Systems Synthesis","author":"Panda Preeti Ranjan","year":"2001","unstructured":"Preeti Ranjan Panda. 2001. SystemC: A modeling platform supporting multiple design abstractions. In Proceedings of the 14th International Symposium on Systems Synthesis. 75\u201380."},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.vlsi.2020.06.003"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.05.054"},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2008.4484908"},{"key":"e_1_3_2_50_2","article-title":"Transaction level modeling in SystemC","author":"Rose Adam","year":"2005","unstructured":"Adam Rose, Stuart Swan, John Pierce, and Jean-Michel Fernandez. 2005. Transaction level modeling in SystemC. Open SystemC Initiative 1 (2005), 1\u201317.","journal-title":"Open SystemC Initiative"},{"key":"e_1_3_2_51_2","doi-asserted-by":"crossref","first-page":"828","DOI":"10.1109\/DATE.2003.1253709","volume-title":"Proceedings of the 2003 Design, Automation, and Test in Europe Conference and Exhibition (DATE\u201903)","author":"Roychoudhury Abhik","year":"2003","unstructured":"Abhik Roychoudhury, Tulika Mitra, and Satyanarayana R. Karri. 2003. Using formal techniques to debug the AMBA system-on-chip bus protocol. In Proceedings of the 2003 Design, Automation, and Test in Europe Conference and Exhibition (DATE\u201903). IEEE, Los Alamitos, CA, 828\u2013833."},{"key":"e_1_3_2_52_2","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2008.ECP.14"},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.2018.8465909"},{"issue":"7","key":"e_1_3_2_54_2","doi-asserted-by":"crossref","first-page":"814","DOI":"10.1109\/43.851997","article-title":"Sequential equivalence checking based on structural similarities","volume":"19","author":"Eijk C. A. J. Van","year":"2000","unstructured":"C. A. J. Van Eijk. 2000. Sequential equivalence checking based on structural similarities. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 19, 7 (2000), 814\u2013819.","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"},{"key":"e_1_3_2_55_2","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2010.5457129"},{"key":"e_1_3_2_56_2","doi-asserted-by":"crossref","unstructured":"Muralidaran Vijayaraghavan Adam Chlipala and Nirav Dave. 2015. Modular deductive verification of multiprocessor hardware designs. In Computer Aided Verification . Lecture Notes in Computer Science Vol. 9207. Springer 109\u2013127.","DOI":"10.1007\/978-3-319-21668-3_7"},{"key":"e_1_3_2_57_2","first-page":"413","volume-title":"Proceedings of the International Conference on Algebraic Methodology and Software Technology","author":"Vu Thuy Duong","year":"2008","unstructured":"Thuy Duong Vu, Li Zhang, and Chris Jesshope. 2008. The verification of the on-chip COMA cache coherence protocol. In Proceedings of the International Conference on Algebraic Methodology and Software Technology. 413\u2013429."},{"key":"e_1_3_2_58_2","doi-asserted-by":"publisher","DOI":"10.1109\/12.368009"},{"key":"e_1_3_2_59_2","first-page":"1","volume-title":"Proceedings of the 2021 Design, Automation, and Test in Europe Conference and Exhibition (DATE\u201921)","author":"Xing Yue","year":"2021","unstructured":"Yue Xing, Huaixi Lu, Aarti Gupta, and Sharad Malik. 2021. Leveraging processor modeling and verification for general hardware modules. In Proceedings of the 2021 Design, Automation, and Test in Europe Conference and Exhibition (DATE\u201921). 1\u20136."},{"key":"e_1_3_2_60_2","volume-title":"Proceedings of the 2022 IEEE\/ACM International Conference on Computer Aided Design (ICCAD\u201922)","author":"Xing Yue","year":"2022","unstructured":"Yue Xing, Huaixi Lu, Aarti Gupta, and Sharad Malik. 2022. Compositional verification using a formal component and interface specification. In Proceedings of the 2022 IEEE\/ACM International Conference on Computer Aided Design (ICCAD\u201922)."}],"container-title":["ACM Transactions on Design Automation of Electronic Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3610292","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3610292","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T17:49:02Z","timestamp":1750182542000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3610292"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,10,16]]},"references-count":59,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2023,11,30]]}},"alternative-id":["10.1145\/3610292"],"URL":"https:\/\/doi.org\/10.1145\/3610292","relation":{},"ISSN":["1084-4309","1557-7309"],"issn-type":[{"type":"print","value":"1084-4309"},{"type":"electronic","value":"1557-7309"}],"subject":[],"published":{"date-parts":[[2023,10,16]]},"assertion":[{"value":"2023-01-26","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-07-08","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-10-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}