%0 Conference Proceedings
%T Carnac: Algorithm Variability for Fast Swarm Verification on FPGA
%+ É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 2021 31st International Conference on Field-Programmable Logic and Applications (FPL)
%C Dresden, Germany
%I IEEE
%3 2021 31st International Conference on Field-Programmable Logic and Applications (FPL)
%P 185-189
%8 2021-08-30
%D 2021
%R 10.1109/FPL53798.2021.00038
%K field programmable gate arrays
%K logic design
%K optimisation
%K program verification
%K field programmable gate arrays
%Z Computer Science [cs]Conference papers
%X The mapping of software verification algorithms on FPGA promise orders of magnitude faster verification. FP-GASwarm shows 900X speedup over software swarm verification. However, this approach misses important optimization opportunities and glosses over algorithmic design-space exploration.This paper introduces Carnac, a deeply pipelined swarm verification architecture, which by exposing the algorithmic variability points can realize multiple verification algorithms. Furthermore, we introduce the Mixed Young Random Frontier-Bounded (MYR_FB), a new swarm verification algorithm, found through an efficiency-based design-space exploration.Evaluated on the BEEM benchmark, the MYR_FB algorithm shows up to 144% efficiency gain over FPGASwarm on 72% of the models. The Carnac architecture runs at 400MHz on Xilinx Ultrascale+ FPGA, and can accommodate twice more verification cores than FPGASwarm. Overall the evaluation shows a 7.58X speedup over FPGASwarm, while enabling an unprecedented scalability on high-end FPGAs.
%G English
%L hal-03550389
%U https://hal-ensta-bretagne.archives-ouvertes.fr/hal-03550389
%~ 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