#+title: Vericert Documentation #+author: Yann Herklotz #+email: git@ymhg.org #+setupfile: setup.org * Vericert :PROPERTIES: :EXPORT_FILE_NAME: _index :CUSTOM_ID: vericert :END: A formally verified high-level synthesis (HLS) tool written in Coq, building on top of [[https://github.com/AbsInt/CompCert][CompCert]]. This ensures the correctness of the C to Verilog translation according to our Verilog semantics and CompCert's C semantics, removing the need to check the resulting hardware for behavioural correctness. ** Features The project is currently a work in progress. Currently, the following C features are supported and have all been proven correct, providing a verified translation from C to Verilog: - all int operations, - non-recursive function calls, - local arrays and pointers, and - control-flow structures such as if-statements, for-loops, etc... ** Content - [[/manual/index.html][Vericert Manual]] - [[/src/toc.html][Vericert Source]] ** Papers - OOPSLA '21 :: Yann Herklotz, James D. Pollard, Nadesh Ramanathan, and John Wickerson. Formal Verification of High-Level Synthesis. In /Proc. ACM Program. Lang./ 5, OOPSLA, 2021. [ [[./static/papers/fvhls_oopsla21.pdf][pdf]] ] - LATTE '21 :: Yann Herklotz and John Wickerson. High-level synthesis tools should be proven correct. In /Workshop on Languages, Tools, and Techniques for Accelerator Design/, 2021. [ [[./static/papers/hlsspc_latte2021.pdf][pdf]] ] ** Mailing lists For discussions, you can join the following mailing list: [[https://lists.sr.ht/~ymherklotz/vericert-discuss][lists.sr.ht/~ymherklotz/vericert-discuss]]. For contributing patches to the [[https://sr.ht/~ymherklotz/vericert/][sourcehut]] repository: [[https://lists.sr.ht/~ymherklotz/vericert-devel][lists.sr.ht/~ymherklotz/vericert-devel]]. * Index :PROPERTIES: :EXPORT_HUGO_SECTION: menu :EXPORT_FILE_NAME: index :EXPORT_HUGO_CUSTOM_FRONT_MATTER: :headless true :END: - [[./static/manual/index.html][Vericert Manual]] * Blog ** Blog :PROPERTIES: :EXPORT_FILE_NAME: _index :EXPORT_HUGO_SECTION: blog :CUSTOM_ID: blog :END: Blog posts: ** A First Look at Vericert :introduction:summary:@article: :PROPERTIES: :EXPORT_DATE: 2021-10-09 :EXPORT_FILE_NAME: a-first-look-at-vericert :EXPORT_HUGO_SECTION: blog :EXPORT_HUGO_CUSTOM_FRONT_MATTER: :summary "Vericert is a formally verified high-level synthesis tool, translating C code into a hardware design expressed in Verilog." :aliases '("/2021/09/a-first-look-at-vericert/") :CUSTOM_ID: a-first-look-at-vericert :END: Compilers are increasingly being relied upon to produce binaries from code without introducing any bugs in the process. Therefore, formally verified compilers like [[https://compcert.org][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. #+caption: Typical HLS flow compared to the standard software flow. #+attr_html: :width 500px [[./static/images/hls-flow-handdrawn.svg]] 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 [[./static/papers/hlsspc_latte2021.pdf][workshop paper]] published at LATTE'21 which describes why HLS in particular is an important translation to verify. *** How do we formally verify it? #+caption: Add a back end branching off the three-address code intermediate language to produce Verilog. #+attr_html: :width 500px [[./static/images/toolflow-handdrawn.svg]] We use CompCert, an existing formally verified C compiler, to translate C into 3AC[fn:1], 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.[fn:2] **** 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 - [[./static/papers/fvhls_oopsla21.pdf][OOPSLA'21 preprint]]. - [[https://youtu.be/clPiKbKVlUA][OOPSLA'21 presentation]]. - [[https://github.com/ymherklotz/vericert][Github repository]]. * Future Work ** Future Work :PROPERTIES: :EXPORT_FILE_NAME: future :END: This section contains future work that should be added to Vericert to make it into a better high-level synthesis tool. The next interesting optimisations that should be looked at are the following: - [[#globals][globals]], - [[#type-support][type support]], - [[#memory-partitioning][memory partitioning]], and - [[#loop-pipelining][loop pipelining]]. *** Globals :PROPERTIES: :CUSTOM_ID: globals :END: Globals are an important feature to add, as have to be handled carefully in HLS, because they have to be placed into memory, and are often used in HLS designs. Proper handling of globals would allow for a larger subset of programs to be compiled, even allowing for larger benchmarks to be used, such as CHStone. #+begin_quote Vericert is a formally verified high-level synthesis (HLS) tool written in Coq, which translates C code into Verilog hardware designs. One challenge in HLS is supporting different memory architectures and interacting with memory in an optimal way. Vericert currently lacks support for multiple memories, and instead only constructs one large memory which contains all elements of the stack. Due to this limitation, Vericert mainly inlines all function calls and does not support global variables. This project would be about adding support for multiple memories to Vericert and proving the correctness of the improved translation. This would then allow globals to be compiled, which greatly increases the kinds of programs that can be translated. This project would be ideal for students interested in hardware and theorem proving in Coq. #+end_quote *** Type Support :PROPERTIES: :CUSTOM_ID: type-support :END: It would also be useful to have support for other datatypes in C, such as ~char~ or ~short~, as using these small datatypes is also quite popular in HLS to make the final designs more efficient. #+begin_quote Vericert is a formally verified high-level synthesis (HLS) tool written in Coq, which translates C code into Verilog hardware designs. However, it currently only supports 32-bit integer types, which limits the effectiveness of HLS, as smaller types cannot be supported and are therefore not represented properly. This project would address this problem by adding support for multiple different types in Vericert, and prove the new translation correct in Coq. Furthermore, the current memory in Vericert also only supports 32-bits, so this project could also address that by generalising the memory module and supporting smaller memory types. #+end_quote *** Register Allocation :PROPERTIES: :CUSTOM_ID: register-allocation :END: Register allocation is an optimisation which minimises the register resource usage of the design, while still keeping the same throughput in most cases. Compared to standard software compilers, HLS tools do not normally require a lot of register allocation, however, this can still help in a lot of cases when registers are used unnecessarily. #+begin_quote Vericert is a formally verified high-level synthesis (HLS) tool written in Coq, which translates C code into Verilog hardware designs. #+end_quote *** Memory Partitioning :PROPERTIES: :CUSTOM_ID: memory-partitioning :END: Memory partitioning is quite an advanced optimisation, which could be combined with the support for globals so as to make memory layouts on the FPGA more efficient and run various memory operations in parallel. *** Loop pipelining :PROPERTIES: :CUSTOM_ID: loop-pipelining :END: Loop pipelining is an optimisation to schedule loops, instead of only scheduling the instructions inside of the loop. There are two versions of loop pipelining, software and hardware loop pipelining. The former is done purely on instructions, whereas the latter is performed in tandem with [[/manual/Scheduling.html][scheduling]]. * Footnotes [fn:2] One example is with the ~Oshrximm~ instruction, which is represented using division in CompCert, whereas it should actually perform multiple shifts. [fn:1] Also known as RTL in the CompCert literature, however, we refer to it as 3AC to avoid confusion with register-transfer level, often used to describe the target of the HLS tool.