Carnac: Algorithm Variability for Fast Swarm Verification on FPGA - Archive ouverte HAL Accéder directement au contenu
Communication Dans Un Congrès Année :

Carnac: Algorithm Variability for Fast Swarm Verification on FPGA

(1, 2) , (1, 3) , (2, 1)
1
2
3

Résumé

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.
Fichier non déposé

Dates et versions

hal-03550389 , version 1 (01-02-2022)

Identifiants

Citer

Emilien Fournier, Ciprian Teodorov, Loïc Lagadec. Carnac: Algorithm Variability for Fast Swarm Verification on FPGA. 2021 31st International Conference on Field-Programmable Logic and Applications (FPL), Aug 2021, Dresden, Germany. pp.185-189, ⟨10.1109/FPL53798.2021.00038⟩. ⟨hal-03550389⟩
13 Consultations
0 Téléchargements

Altmetric

Partager

Gmail Facebook Twitter LinkedIn More