Our new paper has been accepted to appear in ACM Transactions on Reconfigurable Technology and Systems (TRETS), in a special issue dedicated to FPL 2019. The paper is available here.
Shenghsun Cho, Mrunal Patel, Michael Ferdman, and Peter Milder. “Practical Model Checking on FPGAs.” ACM Transactions on Reconfigurable Technology and Systems, Volume 14, Issue 2, July 2021.
This paper is an extension of our FPL2019 paper.
Abstract: 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 speed-up over software. Unfortunately, the “FPGA programmability wall,” particularly the long synthesis and place-and-route times, block the general adoption of FPGAs for model checking.
To address this problem, we designed a runtime-programmable pipeline specifically for model checkers on FPGAs to minimize the “preparation time” 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.
This entry was posted on February 01, 2021.