{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:20:45Z","timestamp":1750220445759,"version":"3.41.0"},"reference-count":17,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2021,6,30]],"date-time":"2021-06-30T00:00:00Z","timestamp":1625011200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Reconfigurable Technol. Syst."],"published-print":{"date-parts":[[2021,6,30]]},"abstract":"<jats:p>Software verification is an important stage of the software development process, particularly for mission-critical systems. As the traditional methodology of using unit tests falls short of verifying complex software, developers are increasingly relying on formal verification methods, such as explicit state model checking, to automatically verify that the software functions properly. However, due to the ever-increasing complexity of software designs, model checking cannot be performed in a reasonable amount of time when running on general-purpose cores, leading to the exploration of hardware-accelerated model checking. FPGAs have been demonstrated to be promising verification accelerators, exhibiting nearly three orders of magnitude speedup over software. Unfortunately, the \u201cFPGA programmability wall,\u201d particularly the long synthesis and place-and-route times, block the general adoption of FPGAs for model checking.<\/jats:p>\n          <jats:p>To address this problem, we designed a runtime-programmable pipeline specifically for model checkers on FPGAs to minimize the \u201cpreparation time\u201d before a model can be checked. Our design of the successor state generator and the state validator modules enables FPGA-acceleration of model checking without incurring the time-consuming FPGA implementation stages, reducing the preparation time before checking a model from hours to less than a minute, while incurring only a 26% execution time overhead compared to model-specific implementations.<\/jats:p>","DOI":"10.1145\/3448272","type":"journal-article","created":{"date-parts":[[2021,7,15]],"date-time":"2021-07-15T16:57:06Z","timestamp":1626368226000},"page":"1-18","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Practical Model Checking on FPGAs"],"prefix":"10.1145","volume":"14","author":[{"given":"Shenghsun","family":"Cho","sequence":"first","affiliation":[{"name":"Stony Brook University, Stony Brook, NY"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mrunal","family":"Patel","sequence":"additional","affiliation":[{"name":"University of California, Los Angeles, Stony Brook, NY"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Ferdman","sequence":"additional","affiliation":[{"name":"Stony Brook University, Stony Brook, NY"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"Milder","sequence":"additional","affiliation":[{"name":"Stony Brook University, Stony Brook, NY"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2021,7,15]]},"reference":[{"doi-asserted-by":"publisher","key":"e_1_2_1_1_1","DOI":"10.1109\/ICPADS.2010.82"},{"doi-asserted-by":"publisher","key":"e_1_2_1_2_1","DOI":"10.1109\/ICPADS.2009.50"},{"doi-asserted-by":"publisher","key":"e_1_2_1_3_1","DOI":"10.1145\/2632362.2632379"},{"doi-asserted-by":"publisher","key":"e_1_2_1_4_1","DOI":"10.1007\/s10009-010-0176-4"},{"key":"e_1_2_1_5_1","volume-title":"28th International Conference on Field Programmable Logic and Applications (FPL\u201918)","author":"Cho S.","year":"2018","unstructured":"S. Cho , M. Ferdman , and P. Milder . 2018. FPGASwarm: High throughput model checking on FPGAs . In 28th International Conference on Field Programmable Logic and Applications (FPL\u201918) . 435\u2013442. DOI:DOI:https:\/\/doi.org\/10.1109\/FPL. 2018 .00080 10.1109\/FPL.2018.00080 S. Cho, M. Ferdman, and P. Milder. 2018. FPGASwarm: High throughput model checking on FPGAs. In 28th International Conference on Field Programmable Logic and Applications (FPL\u201918). 435\u2013442. DOI:DOI:https:\/\/doi.org\/10.1109\/FPL.2018.00080"},{"doi-asserted-by":"publisher","key":"e_1_2_1_6_1","DOI":"10.5555\/1928137.1928148"},{"key":"e_1_2_1_7_1","volume-title":"PRISM: Probabilistic Symbolic Model Checker","author":"Field Tony","year":"2002","unstructured":"Tony Field , Peter G. Harrison , Jeremy Bradley , and Uli Harder (Eds.). 2002 . PRISM: Probabilistic Symbolic Model Checker . Springer Berlin . DOI:DOI:https:\/\/doi.org\/10.1007\/3-540-46029-2_13 10.1007\/3-540-46029-2_13 Tony Field, Peter G. Harrison, Jeremy Bradley, and Uli Harder (Eds.). 2002. PRISM: Probabilistic Symbolic Model Checker. Springer Berlin. DOI:DOI:https:\/\/doi.org\/10.1007\/3-540-46029-2_13"},{"doi-asserted-by":"publisher","key":"e_1_2_1_8_1","DOI":"10.1109\/FCCM.2008.36"},{"doi-asserted-by":"publisher","key":"e_1_2_1_9_1","DOI":"10.5555\/2029108"},{"doi-asserted-by":"publisher","key":"e_1_2_1_10_1","DOI":"10.1109\/32.588521"},{"doi-asserted-by":"publisher","key":"e_1_2_1_11_1","DOI":"10.1109\/TSE.2010.110"},{"unstructured":"K. Jiang. 2009. Model checking C programs by translating C to Promela.  K. Jiang. 2009. Model checking C programs by translating C to Promela.","key":"e_1_2_1_12_1"},{"unstructured":"Modex 2018. Modex - Model Extraction. Retrieved from http:\/\/spinroot.com\/modex\/.  Modex 2018. Modex - Model Extraction. Retrieved from http:\/\/spinroot.com\/modex\/.","key":"e_1_2_1_13_1"},{"volume-title":"29th International Conference on Field Programmable Logic and Applications (FPL\u201919)","author":"Patel M.","unstructured":"M. Patel , S. Cho , M. Ferdman , and P. Milder . 2019. Runtime-Programmable pipelines for model checkers on FPGAs . In 29th International Conference on Field Programmable Logic and Applications (FPL\u201919) . 51\u201358. M. Patel, S. Cho, M. Ferdman, and P. Milder. 2019. Runtime-Programmable pipelines for model checkers on FPGAs. In 29th International Conference on Field Programmable Logic and Applications (FPL\u201919). 51\u201358.","key":"e_1_2_1_14_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_15_1","DOI":"10.5555\/1770532.1770556"},{"doi-asserted-by":"publisher","key":"e_1_2_1_16_1","DOI":"10.5555\/524721"},{"unstructured":"SwarmWeb 2017. Swarm Verification Website. Retrieved from http:\/\/spinroot.com\/swarm\/.  SwarmWeb 2017. Swarm Verification Website. Retrieved from http:\/\/spinroot.com\/swarm\/.","key":"e_1_2_1_17_1"}],"container-title":["ACM Transactions on Reconfigurable Technology and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3448272","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3448272","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:47:41Z","timestamp":1750193261000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3448272"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,6,30]]},"references-count":17,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2021,6,30]]}},"alternative-id":["10.1145\/3448272"],"URL":"https:\/\/doi.org\/10.1145\/3448272","relation":{},"ISSN":["1936-7406","1936-7414"],"issn-type":[{"type":"print","value":"1936-7406"},{"type":"electronic","value":"1936-7414"}],"subject":[],"published":{"date-parts":[[2021,6,30]]},"assertion":[{"value":"2019-07-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-01-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-07-15","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}