path: root/content.org

#+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.