{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,7]],"date-time":"2026-01-07T19:54:27Z","timestamp":1767815667404,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":23,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,1,16]],"date-time":"2023-01-16T00:00:00Z","timestamp":1673827200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,1,16]]},"DOI":"10.1145\/3566097.3567843","type":"proceedings-article","created":{"date-parts":[[2023,1,31]],"date-time":"2023-01-31T18:40:49Z","timestamp":1675190449000},"page":"26-32","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["An Equivalence Checking Framework for Agile Hardware Design"],"prefix":"10.1145","author":[{"given":"Yanzhao","family":"Wang","sequence":"first","affiliation":[{"name":"Portland State University"}]},{"given":"Fei","family":"Xie","sequence":"additional","affiliation":[{"name":"Portland State University"}]},{"given":"Zhenkun","family":"Yang","sequence":"additional","affiliation":[{"name":"Intel Corporation"}]},{"given":"Pasquale","family":"Cocchini","sequence":"additional","affiliation":[{"name":"Intel Corporation"}]},{"given":"Jin","family":"Yang","sequence":"additional","affiliation":[{"name":"Intel Corporation"}]}],"member":"320","published-online":{"date-parts":[[2023,1,31]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Coreir. URL github.com\/rdaly525\/coreir."},{"key":"e_1_3_2_1_2_1","unstructured":"Aha agile hardware project. URL aha.stanford.edu."},{"key":"e_1_3_2_1_3_1","unstructured":"Vc formal datapath validation. URL synopsys.com\/verification\/static-and-formal-verification\/vc-formal.html."},{"key":"e_1_3_2_1_4_1","unstructured":"Vta implementations in heterocl. URL github.com\/pasqoc\/incubator-tvm\/tree\/bsim_fpga."},{"key":"e_1_3_2_1_5_1","unstructured":"Questa sequential logic equivalence check. URL eda.sw.siemens.com\/en-US\/ic\/questa\/formal-verification\/slec\/."},{"key":"e_1_3_2_1_6_1","unstructured":"Vta hardware specification. URL github.com\/apache\/tvm\/blob\/v0.6\/vta\/include\/vta\/hw_spec.h."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628071.2628092"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.1993.580110"},{"key":"e_1_3_2_1_9_1","volume-title":"Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic. ACM Transactions on Computational Logic (TOCL), 2(1):93--134","author":"Bryant R. E.","year":"2001","unstructured":"R. E. Bryant, S. German, and M. N. Velev. Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic. ACM Transactions on Computational Logic (TOCL), 2(1):93--134, 2001."},{"key":"e_1_3_2_1_10_1","first-page":"209","volume-title":"USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Cadar C.","year":"2008","unstructured":"C. Cadar, D. Dunbar, D. R. Engler, et al. Klee: unassisted and automatic generation of high-coverage tests for complex systems programs. In USENIX Symposium on Operating Systems Design and Implementation (OSDI), pages 209--224, 2008."},{"key":"e_1_3_2_1_11_1","first-page":"578","volume-title":"13th USENIX Symposium on Operating Systems Design and Implementation (OSDI 18)","author":"Chen T.","year":"2018","unstructured":"T. Chen, T. Moreau, Z. Jiang, L. Zheng, E. Yan, H. Shen, M. Cowan, L. Wang, Y. Hu, L. Ceze, et al. {TVM}: An automated {End-to-End} optimizing compiler for deep learning. In 13th USENIX Symposium on Operating Systems Design and Implementation (OSDI 18), pages 578--594, 2018."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2003.811446"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/266021.266090"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3289602.3293910"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373087.3375320"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3400302.3415753"},{"key":"e_1_3_2_1_17_1","first-page":"1","volume-title":"Cosa: Integrated verification for agile hardware design. In 2018 Formal Methods in Computer Aided Design (FMCAD)","author":"Mattarei C.","unstructured":"C. Mattarei, M. Mann, C. Barrett, R. G. Daly, D. Huff, and P. Hanrahan. Cosa: Integrated verification for agile hardware design. In 2018 Formal Methods in Computer Aided Design (FMCAD), pages 1--5. IEEE."},{"key":"e_1_3_2_1_18_1","volume-title":"Vta: an open hardware-software stack for deep learning. arXiv preprint arXiv:1807.04188","author":"Moreau T.","year":"2018","unstructured":"T. Moreau, T. Chen, Z. Jiang, L. Ceze, C. Guestrin, and A. Krishnamurthy. Vta: an open hardware-software stack for deep learning. arXiv preprint arXiv:1807.04188, 2018."},{"key":"e_1_3_2_1_19_1","volume-title":"Programming heterogeneous systems from an image processing dsl. ACM Transactions on Architecture and Code Optimization (TACO), 14(3):1--25","author":"Pu J.","year":"2017","unstructured":"J. Pu, S. Bell, X. Yang, J. Setter, S. Richardson, J. Ragan-Kelley, and M. Horowitz. Programming heterogeneous systems from an image processing dsl. ACM Transactions on Architecture and Code Optimization (TACO), 14(3):1--25, 2017."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2499370.2462176"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/43.851997"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCD.2013.6657090"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2593069.2593209"}],"event":{"name":"ASPDAC '23: 28th Asia and South Pacific Design Automation Conference","location":"Tokyo Japan","acronym":"ASPDAC '23","sponsor":["SIGDA ACM Special Interest Group on Design Automation","IEEE CEDA","IEICE","IEEE CAS","IPSJ"]},"container-title":["Proceedings of the 28th Asia and South Pacific Design Automation Conference"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3566097.3567843","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3566097.3567843","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,7]],"date-time":"2026-01-07T17:32:51Z","timestamp":1767807171000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3566097.3567843"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,16]]},"references-count":23,"alternative-id":["10.1145\/3566097.3567843","10.1145\/3566097"],"URL":"https:\/\/doi.org\/10.1145\/3566097.3567843","relation":{},"subject":[],"published":{"date-parts":[[2023,1,16]]},"assertion":[{"value":"2023-01-31","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}