From 3be488277ce46005570f08888fbf3125b9187c88 Mon Sep 17 00:00:00 2001 From: ymherklotz Date: Sat, 16 Jan 2021 22:17:24 +0000 Subject: deploy: 5388aa50c0f6d329bbb10109369e9bf809c55a3e --- index.html | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'index.html') diff --git a/index.html b/index.html index e27bcc8..4b44540 100644 --- a/index.html +++ b/index.html @@ -1,7 +1,7 @@ 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 +

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 #

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…

Content #

\ No newline at end of file -- cgit