Practical Model Checking on FPGAs (bibtex)
by Shenghsun Cho, Mrunal Patel, Michael Ferdman, Peter Milder
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.
Reference:
Practical Model Checking on FPGAs Shenghsun Cho, Mrunal Patel, Michael Ferdman, Peter Milder, In ACM Trans. Reconfigurable Technol. Syst., Association for Computing Machinery, volume 14, 2021.
Bibtex Entry:
@article{ferdman-trets-practical-model-checking-on-fpgas,
  author = {Cho, Shenghsun and Patel, Mrunal and Ferdman, Michael and Milder, Peter},
  title = {Practical Model Checking on FPGAs},
  year = {2021},
  issue_date = {July 2021},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  volume = {14},
  number = {2},
  issn = {1936-7406},
  doi = {10.1145/3448272},
  pdf={http://compas.cs.stonybrook.edu/%7Emferdman/downloads.php/TRETS20_Practical_Model_Checking_on_FPGAs.pdf},
  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.},
  journal = {ACM Trans. Reconfigurable Technol. Syst.},
  month = jul,
  articleno = {8},
  numpages = {18},
  keywords = {Accelerators, overlay architecture}
}
Powered by bibtexbrowser