{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,14]],"date-time":"2025-05-14T02:28:29Z","timestamp":1747189709946,"version":"3.40.5"},"reference-count":30,"publisher":"World Scientific Pub Co Pte Ltd","issue":"04","funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61902421"],"award-info":[{"award-number":["61902421"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J CIRCUIT SYST COMP"],"published-print":{"date-parts":[[2021,3,30]]},"abstract":"<jats:p> The growing complexity of modern digital design makes designers shift toward starting design exploration using high-level languages, and generating register transfer level (RTL) design from system level modeling (SLM) using high-level synthesis tools or manual transformation. Unfortunately, this translation process is very complex and error prone. The most important verification task is to check whether the RTL implementation is indeed equivalent to the system-level model. Equivalence checking is critical to ensure that the synthesized RTL conforms to its SLM specification. <\/jats:p><jats:p> In this paper, we propose a novel path-based sequential equivalence checking method to validate the transformed RTL description against its corresponding SLM description. We represent the original SLM and the transformed RTL descriptions using Finite state machines with datapath (FSMD) and compare the path-pairs of the FSMD to obtain the equivalence of the designs. Then we recognize the corresponding path-pairs from all the generated paths of FSMD with Machine learning (ML) technique, and compare the recognized path-pairs by symbolic simulation and a satisfiability modulo theories (SMT) solver. Our method can handle designs without mapping information and improve the efficiency of the state-of-the-art path-based equivalence checking methods. The promising experiments on representative benchmarks indicate the efficiency and effectiveness of our method. <\/jats:p>","DOI":"10.1142\/s0218126621500742","type":"journal-article","created":{"date-parts":[[2020,7,10]],"date-time":"2020-07-10T11:30:43Z","timestamp":1594380643000},"page":"2150074","source":"Crossref","is-referenced-by-count":4,"title":["A Path-Based Equivalence Checking Method Between System Level and RTL Descriptions Using Machine Learning"],"prefix":"10.1142","volume":"30","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3896-6938","authenticated-orcid":false,"given":"Jian","family":"Hu","sequence":"first","affiliation":[{"name":"The Sixty-Third Research Institute, National University of Defense Technology, Nanjing 210000, P. R. China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yongyang","family":"Hu","sequence":"additional","affiliation":[{"name":"The Sixty-Third Research Institute, National University of Defense Technology, Nanjing 210000, P. R. China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Qi","family":"Lv","sequence":"additional","affiliation":[{"name":"College of Meteorology and Oceanography, National University of Defense Technology, Nanjing 211101, P. R. China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wentao","family":"Wang","sequence":"additional","affiliation":[{"name":"College of Computer, National University of Defense Technology, Changsha 410000, P. R. China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Guanwu","family":"Wang","sequence":"additional","affiliation":[{"name":"The Sixty-Third Research Institute, National University of Defense Technology, Nanjing 210000, P. R. China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Guilin","family":"Chen","sequence":"additional","affiliation":[{"name":"The Sixty-Third Research Institute, National University of Defense Technology, Nanjing 210000, P. R. China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kang","family":"Wang","sequence":"additional","affiliation":[{"name":"The Sixty-Third Research Institute, National University of Defense Technology, Nanjing 210000, P. R. China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yun","family":"Kang","sequence":"additional","affiliation":[{"name":"The Sixty-Third Research Institute, National University of Defense Technology, Nanjing 210000, P. R. China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Haitao","family":"Yang","sequence":"additional","affiliation":[{"name":"The Sixty-Third Research Institute, National University of Defense Technology, Nanjing 210000, P. R. China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"219","published-online":{"date-parts":[[2020,10,9]]},"reference":[{"key":"S0218126621500742BIB001","doi-asserted-by":"publisher","DOI":"10.1109\/CADGraphics.2013.21"},{"key":"S0218126621500742BIB002","doi-asserted-by":"publisher","DOI":"10.1007\/s11704-015-4257-0"},{"key":"S0218126621500742BIB003","doi-asserted-by":"publisher","DOI":"10.1109\/EWDTS.2008.5580149"},{"key":"S0218126621500742BIB004","doi-asserted-by":"publisher","DOI":"10.1145\/1403375.1403472"},{"key":"S0218126621500742BIB005","doi-asserted-by":"publisher","DOI":"10.1109\/MTV.2005.15"},{"key":"S0218126621500742BIB006","first-page":"223","volume-title":"Proc. Great Lakes Symp. VLSI (GLSVLSI)","author":"Gro\u03b2e D.","year":"2011"},{"key":"S0218126621500742BIB007","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2007.364404"},{"key":"S0218126621500742BIB008","doi-asserted-by":"publisher","DOI":"10.1109\/VLSID.2013.208"},{"key":"S0218126621500742BIB009","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2006.1695903"},{"key":"S0218126621500742BIB010","doi-asserted-by":"publisher","DOI":"10.1007\/s10617-008-9033-z"},{"key":"S0218126621500742BIB011","doi-asserted-by":"publisher","DOI":"10.1109\/ISQED.2008.4479812"},{"key":"S0218126621500742BIB012","doi-asserted-by":"publisher","DOI":"10.1109\/ICCCAS.2009.5250316"},{"key":"S0218126621500742BIB013","doi-asserted-by":"crossref","first-page":"516","DOI":"10.1109\/ISQED.2013.6523660","volume-title":"Proc. 14th Int. Symp. Quality Electronic Design (ISQED)","author":"Li T.","year":"2013"},{"key":"S0218126621500742BIB014","doi-asserted-by":"publisher","DOI":"10.1145\/2483028.2483070"},{"key":"S0218126621500742BIB015","first-page":"1500","volume-title":"Proc. Design, Automation and Test in Europe Conference (DATE)","author":"Hao K.","year":"2010"},{"key":"S0218126621500742BIB016","doi-asserted-by":"publisher","DOI":"10.1145\/2463209.2488878"},{"key":"S0218126621500742BIB017","doi-asserted-by":"publisher","DOI":"10.1109\/ISVLSI.2015.110"},{"key":"S0218126621500742BIB018","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2007.913390"},{"key":"S0218126621500742BIB019","doi-asserted-by":"publisher","DOI":"10.1109\/ASPDAC.2011.5722241"},{"key":"S0218126621500742BIB020","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3636-9"},{"key":"S0218126621500742BIB021","first-page":"1","volume-title":"Proc. 14th Latin American Test Workshop (LATW)","author":"Marquez C. I. C.","year":"2013"},{"key":"S0218126621500742BIB022","doi-asserted-by":"publisher","DOI":"10.1109\/SOCC.2015.7406927"},{"key":"S0218126621500742BIB024","doi-asserted-by":"publisher","DOI":"10.1109\/TEST.2014.7035339"},{"key":"S0218126621500742BIB025","doi-asserted-by":"publisher","DOI":"10.1145\/2593069.2593114"},{"key":"S0218126621500742BIB026","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46148-5_5"},{"key":"S0218126621500742BIB027","doi-asserted-by":"publisher","DOI":"10.1007\/978-90-481-9929-7"},{"key":"S0218126621500742BIB028","doi-asserted-by":"publisher","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"S0218126621500742BIB029","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"S0218126621500742BIB030","doi-asserted-by":"publisher","DOI":"10.1145\/115372.115320"},{"key":"S0218126621500742BIB031","doi-asserted-by":"publisher","DOI":"10.3166\/ejc.7.311-327"}],"container-title":["Journal of Circuits, Systems and Computers"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.worldscientific.com\/doi\/pdf\/10.1142\/S0218126621500742","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,9]],"date-time":"2021-04-09T09:16:51Z","timestamp":1617959811000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.worldscientific.com\/doi\/abs\/10.1142\/S0218126621500742"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,10,9]]},"references-count":30,"journal-issue":{"issue":"04","published-print":{"date-parts":[[2021,3,30]]}},"alternative-id":["10.1142\/S0218126621500742"],"URL":"https:\/\/doi.org\/10.1142\/s0218126621500742","relation":{},"ISSN":["0218-1266","1793-6454"],"issn-type":[{"type":"print","value":"0218-1266"},{"type":"electronic","value":"1793-6454"}],"subject":[],"published":{"date-parts":[[2020,10,9]]}}}