Finding and understanding bugs in FPGA synthesis tools

Abstract

All software ultimately relies on hardware functioning correctly.Hardware correctness is becoming increasingly important due tothe growing use of custom accelerators using FPGAs to speed upapplications on servers. Furthermore, the increasing complexity ofhardware also leads to ever more reliance on automation, meaningthat the correctness of synthesis tools is vital for the reliability ofthe hardware.This paper aims to improve the quality of FPGA synthesis toolsby introducing a method to test them automatically using randomlygenerated, correct Verilog, and checking that the synthesised netlistis always equivalent to the original design. The main contributionsof this work are twofold: firstly a method for generating randombehavioural Verilog free of undefined values, and secondly a Verilogtest case reducer used to locate the cause of the bug that was found.These are implemented in a tool called Verismith. This paper alsoprovides a qualitative and quantitative analysis of the bugs found inYosys, Vivado, XST and Quartus Prime. Every synthesis tool exceptQuartus Prime was found to introduce discrepancies between thenetlist and the design. In addition to that, Vivado and a developmentversion of Yosys were found to crash when given valid input. UsingVerismith, eleven bugs were reported to tool vendors, of which sixhave already been fixed.