Hardware Acceleration for Model Checking.
Jens Brandt, Klaus Schneider, Adrian Willenbücher · MBMV · 2008
In this paper, we present a coprocessor to accelerate explicit state based model checking by computing the set of reachable states with the help of massively parallel hardware. The algorithm is based on known implementations of algorithms for the solution of the algebraic path problem on systolic arrays. We describe the mapping to a field programmable gate array, including the implementation of input and output operations. Our preliminary experimental results show a significant speedup and the applicability of our approach to real-world problems.