Dolmen: FPGA Swarm for Safety and Liveness Verification
Emilien Fourniera, Ciprian Teodorovb and Loïc Lagadecc
Lab-STICC, ENSTA Bretagne Brest, France
aemilien.fournier@ensta-bretagne.org
bciprian.teodorov@ensta-bretagne.fr
cloic.lagadec@ensta-bretagne.fr
ABSTRACT
To ensure correctness of critical systems, swarm verification produces proofs of failure on systems too large to be verified using model-checking. Recent research efforts exploit both intrinsic parallelism and low-latency on-chip memory offered by FPGAs to achieve 3 orders of magnitude speedups over software. However, these approaches are limited to safety verification that encodes only what the system should not do. Liveness properties express what the system should do, and are widely used in the verification of operating systems, distributed systems, and communication protocols. Both safety and liveness properties are of paramount importance to ensure systems correctness. This paper presents Dolmen, the first FPGA implementation of a swarm verification engine that supports both safety and liveness properties. Dolmen features a deeply pipelined verification core, along with a scalable architecture to allow highfrequency synthesis on large FPGAs. Our experimental results, on a Xilinx Virtex Ultrascale+ FPGA, show that the Dolmen architecture can achieve up to 4 orders of magnitude speedups compared to software model-checking.
Keywords: Model-Checking, Safety Verification, Liveness Verification, Reconfigurable Architecture, FPGA.
