diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-07-24 10:58:51 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-07-24 10:58:51 +0100 |
| commit | 7f633ad8c9b7d4580fe1a0a1b780ca4486e3fe99 (patch) | |
| tree | 098d4b16d44b592256769f20ba8ec27d8b5e284b /README.md | |
| parent | b6a094c0e3b1b5bef06d932fc73f09aba88a4fda (diff) | |
| download | vericert-7f633ad8c9b7d4580fe1a0a1b780ca4486e3fe99.tar.gz vericert-7f633ad8c9b7d4580fe1a0a1b780ca4486e3fe99.zip | |
Add more descriptions to README
Diffstat (limited to 'README.md')
| -rw-r--r-- | README.md | 6 |
1 files changed, 3 insertions, 3 deletions
@@ -1,12 +1,12 @@ -# VeriCert +# Vericert  -A formally verified HLS tool in Coq, building on top of [CompCert](https://github.com/AbsInt/CompCert). +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. ## 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. +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. 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: |