Verismith

Posted on June 19, 2019

Most hardware is designed using a hardware description language (HDL) such as Verilog or VHDL. These languages allow some abstraction over the hardware that is produced so that it is more modular and easier to maintain. To translate these hardware descriptions to actual hardware, they can be passed through a synthesis tool, which generates a netlist referring to the specific hardware connections that will appear in the actual hardware.

Furthermore, high-level synthesis (HLS) is also becoming more popular, which allows for a much more behavioural description of the circuit using a standard programming language such as C or OpenCL. However, even designs written in these languages need to be translated to an HDL such as Verilog or VHDL and therefore also need to rely on a synthesis tool.

Fuzzing is a way to randomly test tools to check if their behaviour remains correct. This has been very effective at finding bugs in compilers, such as GCC and Clang. CSmith, a C fuzzer, found more than 300 bugs in these tools by randomly generating C programs and checking that all the C compilers execute these programs in the same fashion. We therefore thought it would be a good idea to test synthesis tools in a similar fashion and improve their reliability. There are three main sections that I’ll go over to explain how we fuzz these tools: Verilog generation, Equivalence checking and Verilog reduction.

** Verilog Generation

To test these tools, we have to first generate random Verilog which can be passed to the synthesis tool. There are a few important properties that we have to keep in mind though.

First, the Verilog should always have the same behaviour no matter which synthesis tool it passes through. This is not always the case, as undefined values can either result in a 1 or a 0.

Second, we have to make sure that our Verilog is actually correct and will not fail synthesis. This is important as we are trying to find deep bugs in the synthesis tools and not just it’s error reporting.

Once we have generated the Verilog, it’s time to give it to the synthesis tools to check that the output is correct. This is done using a formal equivalence check on the output of the synthesis tool.

** Equivalence Check

The synthesis tools output a netlist, which is a lower level description of the hardware that will be produced. As the design that we wrote is also just hardware, we can compare these using the various equivalence checking tools that exist. This mathematically proves that the design was the same as the netlist.

If this fails, or if the synthesis tool crashed as it was generating the netlist, we want to then locate the cause for the bug. This can be done automatically by reducing the design until the bug is not present anymore and we cannot reduced the Verilog further.

** Verilog Reduction

To find the cause of the bug, we want to reduce the design to a minimal representation that still shows the bug. This can be done by cutting the Verilog design into two, and checking which half still contains the bug. Once we do this a few times at different levels of granularity, we finally get to a smaller piece of Verilog code that still executes the bug in the synthesis tool. This is then much easier to analyse further and report to the tool vendors.

** Results

In total, we reported 12 bugs to all the synthesis tools that we tested. A full summary of the bugs that were found can be seen in the Github repository.

** Resources

The following resources provide more context about Verismith: