{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,5]],"date-time":"2026-06-05T15:53:31Z","timestamp":1780674811451,"version":"3.54.1"},"publisher-location":"New York, NY, USA","reference-count":36,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,10,30]],"date-time":"2022-10-30T00:00:00Z","timestamp":1667088000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"DARPA"},{"name":"SRC"},{"name":"NSF","award":["1628926"],"award-info":[{"award-number":["1628926"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2022,10,30]]},"DOI":"10.1145\/3508352.3549341","type":"proceedings-article","created":{"date-parts":[[2022,12,22]],"date-time":"2022-12-22T12:10:54Z","timestamp":1671711054000},"page":"1-9","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Compositional Verification Using a Formal Component and Interface Specification"],"prefix":"10.1145","author":[{"given":"Yue","family":"Xing","sequence":"first","affiliation":[{"name":"Princeton University"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Huaixi","family":"Lu","sequence":"additional","affiliation":[{"name":"Princeton University"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Aarti","family":"Gupta","sequence":"additional","affiliation":[{"name":"Princeton University"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sharad","family":"Malik","sequence":"additional","affiliation":[{"name":"Princeton University"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,12,22]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/2677118"},{"key":"e_1_3_2_1_2_1","first-page":"1850","article-title":"IEEE standard for Property Specification Language (PSL)","author":"IEEE-Commission","year":"2005","unstructured":"IEEE-Commission, \"IEEE standard for Property Specification Language (PSL),\" IEEE Std 1850-2005, 2005.","journal-title":"IEEE Std"},{"key":"e_1_3_2_1_3_1","first-page":"46","volume-title":"ieee","author":"Pnueli A.","year":"1977","unstructured":"A. Pnueli, \"The temporal logic of programs,\" in 18th Annual Symposium on Foundations of Computer Science (sfcs 1977). ieee, 1977, pp. 46--57."},{"key":"e_1_3_2_1_4_1","volume-title":"Model checking","author":"Clarke E. M.","year":"2018","unstructured":"E. M. Clarke Jr, O. Grumberg, D. Kroening, D. Peled, and H. Veith, Model checking. MIT press, 2018."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3282444"},{"key":"e_1_3_2_1_6_1","volume-title":"Automation & Test in Europe Conference & Exhibition (DATE)","author":"Xing Y.","year":"2021","unstructured":"Y. Xing, H. Lu, A. Gupta, and S. Malik, \"Leveraging processor modeling and verification for general hardware modules,\" in Design, Automation & Test in Europe Conference & Exhibition (DATE), 2021."},{"key":"e_1_3_2_1_7_1","first-page":"123","article-title":"In transition from global to modular temporal reasoning about programs,\" in Logics and models of concurrent systems","author":"Pnueli A.","year":"1985","unstructured":"A. Pnueli, \"In transition from global to modular temporal reasoning about programs,\" in Logics and models of concurrent systems. Springer, 1985, pp. 123--144.","journal-title":"Springer"},{"key":"e_1_3_2_1_8_1","volume-title":"8051 micro controller","author":"Teran S.","year":"2016","unstructured":"S. Teran and S. Jaka, \"8051 micro controller,\" 2016, [Online]. Available: http:\/\/opencores.org\/project,8051, accessed on: 2022-04."},{"key":"e_1_3_2_1_9_1","first-page":"160","article-title":"Template-based synthesis of instruction-level abstractions for SoC verification,\" in Formal Methods in Computer-Aided Design (FMCAD)","author":"Subramanyan P.","year":"2015","unstructured":"P. Subramanyan, Y. Vizel, S. Ray, and S. Malik, \"Template-based synthesis of instruction-level abstractions for SoC verification,\" in Formal Methods in Computer-Aided Design (FMCAD). IEEE, 2015, pp. 160--167.","journal-title":"IEEE"},{"key":"e_1_3_2_1_10_1","first-page":"158","article-title":"A 25mm2 SOC for IOT devices with 18ms noise-robust speech-to-text latency via Bayesian speech denoising and attention-based sequence-to-sequence DNN speech recognition in 16nm FinFET,\" in 2021 IEEE International Solid-State Circuits Conference (ISSCC), vol. 64","author":"Tambe T.","year":"2021","unstructured":"T. Tambe, E.-Y. Yang, G. G. Ko, Y. Chai, C. Hooper, M. Donato, P. N. Whatmough, A. M. Rush, D. Brooks, and G.-Y. Wei, \"A 25mm2 SOC for IOT devices with 18ms noise-robust speech-to-text latency via Bayesian speech denoising and attention-based sequence-to-sequence DNN speech recognition in 16nm FinFET,\" in 2021 IEEE International Solid-State Circuits Conference (ISSCC), vol. 64. IEEE, 2021, pp. 158--160.","journal-title":"IEEE"},{"key":"e_1_3_2_1_11_1","unstructured":"NVIDIA \"NVIDIA Deep Learning Accelerator \" 2018 [Online]. Available:www.nvdla.org accessed on: 2022-04."},{"key":"e_1_3_2_1_12_1","first-page":"1","article-title":"INVITED: BaseJump STL: SystemVerilog Needs a Standard Template Library for Hardware Design","author":"Taylor M. B.","year":"2018","unstructured":"M. B. Taylor, \"INVITED: BaseJump STL: SystemVerilog Needs a Standard Template Library for Hardware Design,\" in DAC, 2018, pp. 1--6.","journal-title":"DAC"},{"key":"e_1_3_2_1_13_1","volume-title":"Epiphany eLink AXI","author":"Olofsson A.","year":"2016","unstructured":"A. Olofsson, R. Trogan, F. Huettig, O. Jeppsson, and P. Saunderson, \"Epiphany eLink AXI,\" 2016, [Online]. Available:https:\/\/github.com\/aolofsson\/oh\/tree\/master\/axi, accessed on: 2022-04."},{"key":"e_1_3_2_1_14_1","first-page":"353","article-title":"A refinement-based compositional reasoning framework for pipelined machine verification","volume":"16","author":"Manolios P.","year":"2008","unstructured":"P. Manolios and S. Srinivasan, \"A refinement-based compositional reasoning framework for pipelined machine verification,\" TVLSI, vol. 16, pp. 353 -- 364, 05 2008.","journal-title":"TVLSI"},{"key":"e_1_3_2_1_15_1","volume-title":"Automatic verification of pipelined microprocessor control,\" in CAV","author":"Burch J. R.","year":"1994","unstructured":"J. R. Burch and D. L. Dill, \"Automatic verification of pipelined microprocessor control,\" in CAV, 1994."},{"key":"e_1_3_2_1_16_1","volume-title":"A complete compositional reasoning framework for the efficient verification of pipelined machines,\" in ICCAD","author":"Manolios P.","year":"2005","unstructured":"P. Manolios and S. K. Srinivasan, \"A complete compositional reasoning framework for the efficient verification of pipelined machines,\" in ICCAD, 2005."},{"key":"e_1_3_2_1_17_1","first-page":"42","volume-title":"End-to-end verification of processors with isa-formal,\" in International Conference on Computer Aided Verification","author":"Reid A.","year":"2016","unstructured":"A. Reid, R. Chen, A. Deligiannis, D. Gilday, D. Hoyes, W. Keen, A. Pathirane, O. Shepherd, P. Vrabel, and A. Zaidi, \"End-to-end verification of processors with isa-formal,\" in International Conference on Computer Aided Verification. Springer, 2016, pp. 42--58."},{"key":"e_1_3_2_1_18_1","first-page":"1","article-title":"CoSA: Integrated verification for agile hardware design","author":"Mattarei C.","year":"2018","unstructured":"C. Mattarei, M. Mann, C. Barrett, R. G. Daly, D. Huff, and P. Hanrahan, \"CoSA: Integrated verification for agile hardware design,\" in FMCAD, 2018, pp. 1--5.","journal-title":"FMCAD"},{"key":"e_1_3_2_1_19_1","unstructured":"Cadence Design Systems Inc. \"JasperGold: Formal Property Verification App.\" 2018 [Online]. Available:http:\/\/www.jasperda.com\/products\/jaspergold-apps\/ accessed on: 2022-04."},{"key":"e_1_3_2_1_20_1","unstructured":"Xilinx \"Vivado Design Suite User Guide \" 2021 [Online]. Available:https:\/\/docs.xilinx.com\/v\/u\/en-US\/ug902-vivado-high-level-synthesis accessed on: 2022-04."},{"key":"e_1_3_2_1_21_1","first-page":"351","volume-title":"TACAS 2019 held as part of the 22nd European Joint Conferences on Theory and Practice of Software, ETAPS","author":"Huang B. Y.","year":"2019","unstructured":"B. Y. Huang, H. Zhang, A. Gupta, and S. Malik, \"ILAng: A modeling and verification platform for socs using instruction-level abstractions,\" in 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems conference series, TACAS 2019 held as part of the 22nd European Joint Conferences on Theory and Practice of Software, ETAPS 2019. Springer Verlag, 2019, pp. 351--357."},{"key":"e_1_3_2_1_22_1","first-page":"75","volume-title":"A modeling platform supporting multiple design abstractions,\" in Proceedings of the 14th international symposium on Systems synthesis","author":"Panda P. R.","year":"2001","unstructured":"P. R. Panda, \"SystemC: A modeling platform supporting multiple design abstractions,\" in Proceedings of the 14th international symposium on Systems synthesis, 2001, pp. 75--80."},{"issue":"1","key":"e_1_3_2_1_23_1","first-page":"297","article-title":"Transaction level modeling in SystemC","volume":"1","author":"Rose A.","year":"2005","unstructured":"A. Rose, S. Swan, J. Pierce, and J.-M. Fernandez, \"Transaction level modeling in SystemC,\" Open SystemC Initiative, vol. 1, no. 1.297, 2005.","journal-title":"Open SystemC Initiative"},{"key":"e_1_3_2_1_24_1","first-page":"69","volume-title":"Second ACM and IEEE International Conference on Formal Methods and Models for Co-Design, 2004. MEMOCODE'04. IEEE","author":"Nikhil R.","year":"2004","unstructured":"R. Nikhil, \"Bluespec System Verilog: Efficient, correct RTL from high level specifications,\" in Proceedings. Second ACM and IEEE International Conference on Formal Methods and Models for Co-Design, 2004. MEMOCODE'04. IEEE, 2004, pp. 69--70."},{"key":"e_1_3_2_1_25_1","volume-title":"dissertation","author":"Wright A. C.","year":"2021","unstructured":"A. C. Wright, \"Modular SMT-based verification of rule-based hardware designs,\" Ph.D. dissertation, Massachusetts Institute of Technology, 2021."},{"key":"e_1_3_2_1_26_1","first-page":"243","volume-title":"The essence of Bluespec: A core language for rule-based hardware design,\" in Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation","author":"Bourgeat T.","year":"2020","unstructured":"T. Bourgeat, C. Pit-Claudel, and A. Chlipala, \"The essence of Bluespec: A core language for rule-based hardware design,\" in Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, 2020, pp. 243--257."},{"key":"e_1_3_2_1_27_1","volume-title":"Kami: A platform for high-level parametric hardware specification and its modular verification","author":"Choi J.","year":"2017","unstructured":"J. Choi, M. Vijayaraghavan, B. Sherman, and A. Chlipala, \"Kami: A platform for high-level parametric hardware specification and its modular verification,\" 2017."},{"key":"e_1_3_2_1_28_1","first-page":"175","volume-title":"Wire sorts: A language abstraction for safe hardware composition,\" in Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation","author":"Christensen M.","year":"2021","unstructured":"M. Christensen, T. Sherwood, J. Balkind, and B. Hardekopf, \"Wire sorts: A language abstraction for safe hardware composition,\" in Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2021, pp. 175--189."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/503271.503226"},{"key":"e_1_3_2_1_30_1","first-page":"148","volume-title":"d. Alfaro and T. A. Henzinger, \"Interface theories for component-based design,\" in International Workshop on Embedded Software","author":"L.","year":"2001","unstructured":"L. d. Alfaro and T. A. Henzinger, \"Interface theories for component-based design,\" in International Workshop on Embedded Software. Springer, 2001, pp. 148--165."},{"key":"e_1_3_2_1_31_1","first-page":"24","article-title":"A compositional rule for hardware design refinement","author":"McMillan K. L.","year":"1997","unstructured":"K. L. McMillan, \"A compositional rule for hardware design refinement,\" in CAV, 1997, p. 24--35.","journal-title":"CAV"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_12"},{"key":"e_1_3_2_1_33_1","first-page":"396","article-title":"Microarchitecture verification by compositional model checking","author":"Jhala R.","year":"2001","unstructured":"R. Jhala and K. L. McMillan, \"Microarchitecture verification by compositional model checking,\" in CAV, 2001, p. 396--410.","journal-title":"CAV"},{"key":"e_1_3_2_1_34_1","first-page":"1","article-title":"Going with the flow: Parameterized verification using message flows,\" in 2008 Formal Methods","author":"Talupur M.","year":"2008","unstructured":"M. Talupur and M. R. Tuttle, \"Going with the flow: Parameterized verification using message flows,\" in 2008 Formal Methods in Computer-Aided Design, 2008, pp. 1--8.","journal-title":"Computer-Aided Design"},{"key":"e_1_3_2_1_35_1","first-page":"382","volume-title":"A simple method for parameterized verification of cache coherence protocols,\" in FMCAD","author":"Chou C.-T.","unstructured":"C.-T. Chou, P. K. Mannava, and S. Park, \"A simple method for parameterized verification of cache coherence protocols,\" in FMCAD. Springer Berlin Heidelberg, vol. 3312, pp. 382--398."},{"key":"e_1_3_2_1_36_1","volume-title":"Parameterized compositional model checking,\" in Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems -","author":"Namjoshi K. S.","year":"2016","unstructured":"K. S. Namjoshi and R. J. Trefler, \"Parameterized compositional model checking,\" in Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Volume 9636. Berlin, Heidelberg: Springer-Verlag, 2016, p. 589--606."}],"event":{"name":"ICCAD '22: IEEE\/ACM International Conference on Computer-Aided Design","location":"San Diego California","acronym":"ICCAD '22","sponsor":["SIGDA ACM Special Interest Group on Design Automation","IEEE-EDS Electronic Devices Society","IEEE CAS","IEEE CEDA"]},"container-title":["Proceedings of the 41st IEEE\/ACM International Conference on Computer-Aided Design"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3508352.3549341","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3508352.3549341","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3508352.3549341","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:30:23Z","timestamp":1750188623000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3508352.3549341"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,10,30]]},"references-count":36,"alternative-id":["10.1145\/3508352.3549341","10.1145\/3508352"],"URL":"https:\/\/doi.org\/10.1145\/3508352.3549341","relation":{},"subject":[],"published":{"date-parts":[[2022,10,30]]},"assertion":[{"value":"2022-12-22","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}