%0 Conference Proceedings
%T Dolmen: FPGA Swarm for Safety and Liveness Verification
%+ École Nationale Supérieure de Techniques Avancées Bretagne (ENSTA Bretagne)
%+ Equipe Hardware ARchitectures and CAD tools (Lab-STICC_ARCAD)
%+ Equipe Processes for Safe and Secure Software and Systems (Lab-STICC_P4S)
%A Fournier, Emilien
%A Teodorov, Ciprian
%A Lagadec, Loïc
%< avec comité de lecture
%B 2022 Design, Automation & Test in Europe Conference & Exhibition (DATE)
%C Antwerp, Belgium
%I IEEE
%3 Proceedings of the 2022 Design, Automation and Test in Europe Conference and Exhibition, DATE 2022
%P 1425-1430
%8 2022-03-14
%D 2022
%R 10.23919/DATE54114.2022.9774528
%K Model checking
%K Reconfigurable architectures
%K FPGA
%K liveness verification
%K Model-checking
%K reconfigurable architecture
%K safety verification
%Z Computer Science [cs]Conference papers
%X 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 high-frequency 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.
%G English
%L hal-03708237
%U https://hal-ensta-bretagne.archives-ouvertes.fr/hal-03708237
%~ UNIV-BREST
%~ INSTITUT-TELECOM
%~ ENSTA-BRETAGNE
%~ CNRS
%~ UNIV-UBS
%~ ENSTA-BRETAGNE-STIC
%~ ENIB
%~ LAB-STICC
%~ INSTITUTS-TELECOM
%~ LAB-STICC_ARCAD
%~ LAB-STICC_P4S
%~ LAB-STICC_SHARP