From 13e5c0e470760df77f0046fda41911ca2d4d3bd7 Mon Sep 17 00:00:00 2001 From: ymherklotz Date: Sat, 16 Jan 2021 22:57:04 +0000 Subject: deploy: b6df0b9fd6f4e8a6408ed76d923cf8aaabd04d0a --- index.html | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'index.html') diff --git a/index.html b/index.html index 0b00ac5..9b0b079 100644 --- a/index.html +++ b/index.html @@ -1,5 +1,5 @@ Vericert | Vericert +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:">Vericert | Vericert
Vericert

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 -- cgit