diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-07-24 11:26:09 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-07-24 11:26:09 +0100 |
| commit | 426108aef2912bba65e34157cb43b0a67813dee5 (patch) | |
| tree | 60dbdf84ef41eb911a9fb03f7075f4ff84e2042f /README.md | |
| parent | 7f633ad8c9b7d4580fe1a0a1b780ca4486e3fe99 (diff) | |
| download | vericert-426108aef2912bba65e34157cb43b0a67813dee5.tar.gz vericert-426108aef2912bba65e34157cb43b0a67813dee5.zip | |
Add feature list to README
Diffstat (limited to 'README.md')
| -rw-r--r-- | README.md | 9 |
1 files changed, 9 insertions, 0 deletions
@@ -4,6 +4,15 @@ A formally verified high-level synthesis (HLS) tool written in Coq, building on top of [CompCert](https://github.com/AbsInt/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, so proofs remain to be finished. Currently, the following C features are supported, but are not all proven correct yet: + +- all int operations, +- non-recursive function calls, +- local arrays and pointers +- control-flow structures such as if-statements, for-loops, etc... + ## Building To build Vericert, the provided [Makefile](/Makefile) can be used. External dependencies are needed to build the project, which can be pulled in automatically with [nix](https://nixos.org/nix/) using the provided [default.nix](/default.nix) and [shell.nix](/shell.nix) files. |