{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,18]],"date-time":"2026-06-18T04:28:02Z","timestamp":1781756882198,"version":"3.54.5"},"publisher-location":"New York, NY, USA","reference-count":35,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,6,23]],"date-time":"2024-06-23T00:00:00Z","timestamp":1719100800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"Strategic Priority Research Program of the Chinese Academy of Sciences","award":["Grant No. XDA0320101"],"award-info":[{"award-number":["Grant No. XDA0320101"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,6,23]]},"DOI":"10.1145\/3649329.3657311","type":"proceedings-article","created":{"date-parts":[[2024,11,7]],"date-time":"2024-11-07T19:27:22Z","timestamp":1731007642000},"page":"1-6","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Formally Verifying Arithmetic Chisel Designs for All Bit Widths at Once"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0710-223X","authenticated-orcid":false,"given":"Weizhi","family":"Feng","sequence":"first","affiliation":[{"name":"Institute of Software, Chinese Academy of Sciences, Beijing, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-0505-9935","authenticated-orcid":false,"given":"Yicheng","family":"Liu","sequence":"additional","affiliation":[{"name":"Institute of Software, Chinese Academy of Sciences, Beijing, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6725-8167","authenticated-orcid":false,"given":"Jiaxiang","family":"Liu","sequence":"additional","affiliation":[{"name":"Shenzhen University, Shenzhen, Guangdong, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6636-3301","authenticated-orcid":false,"given":"David N","family":"Jansen","sequence":"additional","affiliation":[{"name":"Institute of Software, Chinese Academy of Sciences, Beijing, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3692-2088","authenticated-orcid":false,"given":"Lijun","family":"Zhang","sequence":"additional","affiliation":[{"name":"Institute of Software, Chinese Academy of Sciences, Beijing, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0899-628X","authenticated-orcid":false,"given":"Zhilin","family":"Wu","sequence":"additional","affiliation":[{"name":"Institute of Software, Chinese Academy of Sciences, Beijing, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,11,7]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"K. Asanovi\u0107 R. Avi\u017eienis et al. 2016. The rocket chip generator. Technical Report. UCB\/EECS-2016-17 EECS Department University of California Berkeley."},{"key":"e_1_3_2_1_2_1","unstructured":"K. Asanovi\u0107 R. Avi\u017eienis et al. 2023. Multiplier and divider in Rocket-Chip. https:\/\/github.com\/chipsalliance\/rocket-chip\/blob\/master\/src\/main\/scala\/rocket\/Multiplier.scala."},{"key":"e_1_3_2_1_3_1","unstructured":"J. Bachrach H. Vo B. C. Richards et al. 2012. Chisel: constructing hardware in a Scala embedded language. In DAC. 1216--1225."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"crossref","unstructured":"F. Bornebusch C. L\u00fcth and et al. 2020. Towards Automatic Hardware Synthesis from Formal Specification to Implementation. In ASP-DAC. 375--380.","DOI":"10.1109\/ASP-DAC47756.2020.9045406"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"crossref","unstructured":"R. E. Bryant. 1996. Bit-Level Analysis of an SRT Divider Circuit. In DAC. 661--665.","DOI":"10.1109\/DAC.1996.545657"},{"key":"e_1_3_2_1_7_1","unstructured":"J. Choi M. Vijayaraghavan B. Sherman et al. 2023. Non-restoring divider in Kami. https:\/\/github.com\/mit-plv\/kami\/blob\/rv32i\/Kami\/Ex\/Divider64.v."},{"key":"e_1_3_2_1_8_1","unstructured":"J. Choi M. Vijayaraghavan B. Sherman et al. 2023. Radix-4 Booth Multiplier in Kami. https:\/\/github.com\/mit-plv\/kami\/blob\/rv32i\/Kami\/Ex\/Multiplier64.v."},{"key":"e_1_3_2_1_9_1","volume-title":"Proc. ACM Program. Lang. 1, ICFP","author":"Choi J.","year":"2017","unstructured":"J. Choi, M. Vijayaraghavan, B. Sherman, and et al. 2017. Kami: a platform for high-level parametric hardware specification and its modular verification. Proc. ACM Program. Lang. 1, ICFP (2017), 24:1--24:30."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"crossref","unstructured":"E. M. Clarke M. Khaira and X. Zhao. 1996. Word Level Model Checking - Avoiding the Pentium FDIV Error. In DAC. 645--648.","DOI":"10.1109\/DAC.1996.545654"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.micpro.2022.104737"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"crossref","unstructured":"A. Dobis T. Petersen H. J. Damsgaard et al. 2021. ChiselVerify: An Open-Source Hardware Verification Library for Chisel and Scala. In NorCAS. 1--7.","DOI":"10.1109\/NorCAS53631.2021.9599869"},{"key":"e_1_3_2_1_13_1","volume-title":"Pi-Ware: Hardware Description and Verification in Agda. In TYPES (LIPIcs","volume":"27","author":"Flor J. P. P.","unstructured":"J. P. P. Flor, W. Swierstra, and Y. Sijsling. 2015. Pi-Ware: Hardware Description and Verification in Agda. In TYPES (LIPIcs, Vol. 69). 9:1--9:27."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/PL00010808"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"crossref","unstructured":"D. Kaufmann and A. Biere. 2021. AMulet 2.0 for Verifying Multiplier Circuits. In TACAS. 357--364.","DOI":"10.1007\/978-3-030-72013-1_19"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-022-00688-6"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2022.3192176"},{"key":"e_1_3_2_1_18_1","volume-title":"Stainless: Verification framework for a subset of the Scala programming language. https:\/\/github.com\/epfl-lara\/stainless.","author":"EPFL","year":"2023","unstructured":"EPFL IC LARA. 2023. Stainless: Verification framework for a subset of the Scala programming language. https:\/\/github.com\/epfl-lara\/stainless."},{"key":"e_1_3_2_1_19_1","unstructured":"Richard Lin and Kevin Laeufer. 2023. ChiselTest. https:\/\/github.com\/ucb-bar\/chiseltest"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2013.2259540"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"crossref","unstructured":"R. Mukherjee M. Tautschnig and D. Kroening. 2016. v2c - A Verilog to C Translator. In TACAS. 580--586.","DOI":"10.1007\/978-3-662-49674-9_38"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"crossref","unstructured":"C. Scholl and A. Konrad. 2020. Symbolic Computer Algebra and SAT Based Information Forwarding for Fully Automatic Divider Verification. In DAC. 1--6.","DOI":"10.1109\/DAC18072.2020.9218721"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"crossref","unstructured":"C. Scholl A. Konrad and et al. 2021. Verifying Dividers Using Symbolic Computer Algebra and Don't Care Optimization. In DATE. 1110--1115.","DOI":"10.23919\/DATE51398.2021.9474019"},{"key":"e_1_3_2_1_24_1","unstructured":"OSCPU team. 2023. NutShell RISC-V CPU. https:\/\/github.com\/OSCPU\/NutShell."},{"key":"e_1_3_2_1_25_1","unstructured":"M. Temel and W. A. Hunt. 2021. Sound and Automated Verification of Real-World RTL Multipliers. In FMCAD. 53--62."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"crossref","unstructured":"M. Temel A. Slobodov\u00e1 and W. A. Hunt. 2020. Automated and Scalable Verification of Integer Multipliers. In CAV. 485--507.","DOI":"10.1007\/978-3-030-53288-8_23"},{"key":"e_1_3_2_1_27_1","volume-title":"Dynamic verification library for Chisel. Master's thesis","author":"Tsai YCA","unstructured":"YCA Tsai. 2021. Dynamic verification library for Chisel. Master's thesis. University of California, Berkeley."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","unstructured":"N. Voirol. 2019. Verified Functional Programming. Ph. D. Dissertation. EPFL Switzerland. 10.5075\/epfl-thesis-9479","DOI":"10.5075\/epfl-thesis-9479"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"crossref","unstructured":"M. Xiang Y. Li and Y. Zhao. 2023. ChiselFV: A Formal Verification Framework for Chisel. In DATE. 1--6.","DOI":"10.23919\/DATE56975.2023.10137221"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"crossref","unstructured":"Y. Xu Z. Yu D. Tang et al. 2022. Towards Developing High Performance RISC-V Processors Using Agile Methodology. In MICRO. 1178--1199.","DOI":"10.1109\/MICRO56248.2022.00080"},{"key":"e_1_3_2_1_31_1","unstructured":"Y. Xu Z. Yu D. Tang et al. 2023. Multiplier in XiangShan. https:\/\/github.com\/OpenXiangShan\/XiangShan\/blob\/master\/src\/main\/scala\/xiangshan\/backend\/fu\/Multiplier.scala."},{"key":"e_1_3_2_1_32_1","unstructured":"Y. Xu Z. Yu D. Tang et al. 2023. Radix2Divider in XiangShan. https:\/\/github.com\/OpenXiangShan\/XiangShan\/blob\/master\/src\/main\/scala\/xiangshan\/backend\/fu\/Radix2Divider.scala."},{"key":"e_1_3_2_1_33_1","unstructured":"Y. Xu Z. Yu D. Tang et al. 2023. XiangShan: An open-source high-performance RISC-V processor. https:\/\/github.com\/OpenXiangShan\/XiangShan."},{"key":"e_1_3_2_1_34_1","volume-title":"CHA: Supporting SVA-Like Assertions in Formal Verification of Chisel Programs (Tool Paper). In SEFM. 324--331.","author":"Yu S.","year":"2022","unstructured":"S. Yu, Y. Dong, J. Liu, et al. 2022. CHA: Supporting SVA-Like Assertions in Formal Verification of Chisel Programs (Tool Paper). In SEFM. 324--331."},{"key":"e_1_3_2_1_35_1","unstructured":"J. Zhao B Korpan A. Gonzalez and K. Asanovic. 2023. RISC-V BOOM: The Berkeley Out-of-Order RISC-V Processor. https:\/\/boom-core.org\/."}],"event":{"name":"DAC '24: 61st ACM\/IEEE Design Automation Conference","location":"San Francisco CA USA","acronym":"DAC '24","sponsor":["SIGDA ACM Special Interest Group on Design Automation","IEEE-CEDA","SIGBED ACM Special Interest Group on Embedded Systems"]},"container-title":["Proceedings of the 61st ACM\/IEEE Design Automation Conference"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3649329.3657311","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3649329.3657311","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:17:56Z","timestamp":1750295876000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3649329.3657311"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,23]]},"references-count":35,"alternative-id":["10.1145\/3649329.3657311","10.1145\/3649329"],"URL":"https:\/\/doi.org\/10.1145\/3649329.3657311","relation":{},"subject":[],"published":{"date-parts":[[2024,6,23]]},"assertion":[{"value":"2024-11-07","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}