Carnac: Algorithm Variability for Fast Swarm Verification on FPGA

International audienceThe 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