A formally verified high-level synthesis (HLS) tool written in Coq, building on top of 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

Currently all proofs of the following features have been completed.

• all int operations,
• non-recursive function calls,
• local arrays and pointers
• control-flow structures such as if-statements, for-loops, etc…

Navigating the code-base

/driver/VericertDriver.ml

The top-level OCaml driver for the HLS tool.

/src/Compiler.v

Top-level soundness proofs of the HLS tool. In particular, separate_transf_c_program_correct states the overall correctness theorem of the HLS tool.

/src/hls/Verilog.v

Main Verilog semantics that the HLS tool is targeting.

/src/hls/DHTL.v

Semantics of the finite-state machine language, which is the intermediate hardware representation before being transformed into Verilog.

/src/hls/Schedule.ml, /src/hls/GiblePargen.v and /src/hls/GiblePargenproof.v

Implementation and proof of scheduling algorithm.

/src/hls/IfConversion.v and /src/hls/IfConversionproof.v

General implementation of if-conversion with its proof of correctness.

/src/hls/DMemorygen.v

Insertion of a proper BRAM memory block for the stack of the main function.

/src/hls/ClockRegisters.v and /src/hls/ClockRegistersproof.v

Proof of parallelisation of assignments in a single state, as the scheduler rearranges instructions but these still assign values sequentially.

Building

To build Vericert, the provided Makefile can be used. External dependencies are needed to build the project, which can be pulled in automatically with nix using the provided default.nix and shell.nix files.

The project is written in Coq, a theorem prover, which is extracted to OCaml so that it can then be compiled and executed. The dependencies of this project are the following:

• Coq: theorem prover that is used to also program the HLS tool.
• OCaml: the OCaml compiler to compile the extracted files.
• dune: build tool for ocaml projects to gather all the ocaml files and compile them in the right order.
• menhir: parser generator for ocaml.
• findlib to find installed OCaml libraries.
• GCC: compiler to help build CompCert.

These dependencies can be installed manually, or automatically through Nix.

Downloading Vericert and CompCert

CompCert is added as a submodule in the lib/CompCert directory. It is needed to run the build process below, as it is the one dependency that is not downloaded by nix, and has to be downloaded together with the repository. To clone CompCert together with this project, and check it out at the correct revision, you can run:

git clone --recursive https://github.com/ymherklotz/vericert

If the repository is already cloned, you can run the following command to make sure that CompCert is also downloaded and the correct branch is checked out:

git submodule update --init

Setting up Nix

Nix is a package manager that can create an isolated environment so that the builds are reproducible. Once nix is installed, it can be used in the following way.

To open a shell which includes all the necessary dependencies, one has to enable nix flakes and one can then use:

nix --experimental-features 'nix-command flakes' develop

which will open a shell that has all the dependencies loaded.

Makefile build

If the dependencies were installed manually, or if one is in the nix develop, the project can be built by running:

make -j8

and installed locally, or under the PREFIX location using:

make install

Which will install the binary in ./bin/vericert by default. However, this can be changed by changing the PREFIX environment variable, in which case the binary will be installed in $PREFIX/bin/vericert.

Running

To test out vericert you can try the following examples which are in the test folder using the following:

./bin/vericert test/loop.c -o loop.v
./bin/vericert test/conditional.c -o conditional.v
./bin/vericert test/add.c -o add.v

Citation

If you use Vericert in any way, please cite it using our OOPSLA’21 paper:

@inproceedings{herklotz21_fvhls,
  author = {Herklotz, Yann and Pollard, James D. and Ramanathan, Nadesh and Wickerson, John},
  title = {Formal Verification of High-Level Synthesis},
  year = {2021},
  number = {OOPSLA},
  numpages = {30},
  month = {11},
  journal = {Proc. ACM Program. Lang.},
  volume = {5},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  doi = {10.1145/3485494}
}

License

This project is licensed under GPLv3. The license can be seen in LICENSE.

The following external code and its license is present in this repository:

src/pipelining

MIT

Copyright (c) 2008,2009,2010 Jean-Baptiste Tristan and INRIA