A First Look at Vericert

October 9, 2021, by Yann Herklotz

Compilers are increasingly being relied upon to produce binaries from code without introducing any bugs in the process. Therefore, formally verified compilers like CompCert were introduced to formally prove that the compilation process does not change the behaviour of the program. This allowed companies like Airbus to move critical code from pure assembly to C.

Similarly, the hardware industry mainly uses hardware description languages, such as Verilog or VHDL, to design their hardware, which can then either be placed onto an FPGA for quick testing, or eventually turned into an ASIC. As there are many commercial tools available for the verification of HDLs, designers prefer to have full control over the hardware and therefore use HDLs directly. However, there are a few downsides with using an HDL instead of higher-level abstractions. First, it makes is computationally harder to check the functionality of hardware, as it needs to be simulated. Second, it often requires a lot of boilerplate code that could be abstracted away otherwise. Alternatives do exist though, such as high-level synthesis tools (HLS), or higher-level hardware description languages.

So why not use higher-level HDLs then? They seem to solve all the problems that current HDLs face. Well, the adoption is hindered by the fact that even though it seems like the perfect solution to have a new language dedicated to hardware design that provides a higher-level of abstraction than existing HDLs, the fact is that the syntax and semantics of such a language often change drastically compared to the existing HDLs which everyone is familiar with. It is already the case that there is a shortage of hardware designers, and it is therefore even more unlikely that these hardware designers would know an alternative hardware design language.

HLS, on the other hand, tackles the problem from a different perspective, and instead ideally aims to bring hardware design to the software designer. This is achieved by compiling a subset of valid software programs directly into hardware, therefore making it much easier to get started with hardware design and write algorithms in hardware. This not only brings hardware design to a larger number of people, but also brings all the benefits of the software ecosystem to verify the hardware designs and algorithms. The following sections will describe the benefits and drawbacks of HLS in more detail, as well as why one would even consider having to formally verify the translation as well.

A bit about HLS #

Ideally, HLS converts any software code into an equivalent hardware design, meaning one does not have to worry about designing any hardware and only has to focus on the functionality of the hardware. In addition to that, this means that a lot of software code can be reused to create hardware accelerators, speeding up the design process even more.

However, in practice this does not seem to be the case yet. For now, the state-of-the-art HLS compilers restrict the subset of the input language greatly, and often cannot optimise it optimally. The main problem with optimisations is that hardware has a much greater design space which can be explored, compared to software. The HLS compiler therefore has to guess in which direction it should optimise, and try and find a Pareto optimal solution. This is unlikely to be optimal, especially if one has various different constraints one could not supply to the HLS tool, making it very difficult to then use the generated hardware. These are currently the main research questions in HLS.

One aspect which is often overlooked though, is that HLS also needs to be correct to be useful, as it generates designs that are often difficult to check. One of the main advantages of HLS is also that it should be possible to check the correctness of the hardware design purely in software, making the design process so much more efficient. The fact that it might therefore introduce bugs in the process, means that the final HLS designs need to be re-verified afterwards.

We have written a workshop paper published at LATTE'21 which describes why HLS in particular is an important translation to verify.

How do we formally verify it? #

We use CompCert, an existing formally verified C compiler, to translate C into 3AC¹, which is the starting point of our high-level synthesis pass. We chose this intermediate language in CompCert to branch off of, as it does not make any assumptions on the number of registers available, which is ideal for hardware as registers are abundantly available. In addition to that, each instruction in 3AC actually directly corresponds to simple operations that can be implemented in hardware.

The process of formally verifying the translation of instructions is quite simple then, we just need to prove that the Verilog statement we translate it to corresponds to the instruction. In most cases there is an equivalent operator in Verilog that performs this action, however, in some cases they don’t quite match up perfectly, in which case we need to prove some properties about integer arithmetic to prove that the two operations are the same.²

Translating the memory model #

The main problem in the proof is: how do we translate CompCert’s abstract view and description of memory to a more concrete implementation of RAM which can subsequently be implemented as a proper RAM by the synthesis tool?

Implementation wise this is quite straight-forward. However, there are some constraints that need to be taken into account:

• The memory in hardware needs to be word-addressed for the best performance.
• Memory in hardware needs to use a proper interface to work.

These two constraints don’t really complicate the implementation much, but they do complicate the proofs quite considerably. Firstly, it’s not straightforward that any address can even be divided by four (to translate it from a byte-addressed memory into an index of a word-addressed array). Secondly, it’s not clear that the RAM will always behave properly, as one now has to reason about a completely different always block, which will be triggered at all clock edges.

However, this translation is still provable. The first issue can be simplified by proving that loads and stores that are valid always have to be word-aligned, meaning they can then be divided by four.

The insertion of the RAM is also provable, because we can design a self-disabling RAM which will only be activated when it is being used, making the proof considerably simpler as one doesn’t have to reason about the RAM when it isn’t enabled.

Useful links #

• OOPSLA'21 preprint.
• OOPSLA'21 presentation.
• Github repository.