New paper on Programmable Model Checking Hardware to Appear at FPL 2019

A new paper describing our recent work on programmable pipelines for accelerating model checking hardware has been accepted to appear at the International Conference on Field-Programmable Logic and Applications (FPL 2019).

This paper, titled “Runtime Programmable Pipelines for Model Checkers on FPGAs,” was co-authored with PhD students Mrunal Patel and Shenghsun Cho and my collaborator Prof. Mike Ferdman. A preprint is available here.

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 software running on general purpose cores cannot be performed in a reasonable amount of time, leading to the exploration of hardware-accelerated model checking. FPGAs have been demon- strated as a promising accelerator because of their high throughput, inherent parallelism, and flexibility. 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 runtime- programmable pipeline 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. Our experimental results show that the runtime-programmable pipeline reduces the preparation time before checking a new or modified model from multiple hours to less than a minute, while maintaining similar throughput as FPGA model checkers with model-specific pipelines.

Runtime-programmable successor state geneartor pipeline

 

This entry was posted on May 17, 2019.