From 7f633ad8c9b7d4580fe1a0a1b780ca4486e3fe99 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 24 Jul 2020 10:58:51 +0100 Subject: Add more descriptions to README --- README.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'README.md') diff --git a/README.md b/README.md index db255a9..b4e4038 100644 --- a/README.md +++ b/README.md @@ -1,12 +1,12 @@ -# VeriCert +# Vericert ![CI](https://github.com/ymherklotz/vericert/workflows/CI/badge.svg) -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: -- cgit