Practical Model Checking on FPGAs
- 30 June 2021
- journal article
- research article
- Published by Association for Computing Machinery (ACM) in ACM Transactions on Reconfigurable Technology and Systems
- Vol. 14 (2), 1-18
- https://doi.org/10.1145/3448272
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 speedup 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.Keywords
This publication has 10 references indexed in Scilit:
- Runtime-Programmable Pipelines for Model Checkers on FPGAsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2019
- FPGASwarm: High Throughput Model Checking on FPGAsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2018
- Towards a GPGPU-parallel SPIN model checkerPublished by Association for Computing Machinery (ACM) ,2014
- Swarm Verification TechniquesIEEE Transactions on Software Engineering, 2010
- Employing Multiple CUDA Devices to Accelerate LTL Model CheckingPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2010
- Parallel probabilistic model checking on general purpose graphics processorsInternational Journal on Software Tools for Technology Transfer, 2010
- DiVinE-CUDA - A Tool for GPU Accelerated LTL Model CheckingElectronic Proceedings in Theoretical Computer Science, 2009
- CUDA Accelerated LTL Model CheckingPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2009
- An FPGA Implementation of Explicit-State Model CheckingPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2008
- The model checker SPINIEEE Transactions on Software Engineering, 1997