From 678816865a90216b750b9cf43f570ff3b868350f Mon Sep 17 00:00:00 2001 From: ymherklotz Date: Sat, 16 Jan 2021 22:14:50 +0000 Subject: deploy: baa147fd4935bc7f395847b2377ba1ffcfeb57a1 --- index.html | 7 +++++++ 1 file changed, 7 insertions(+) create mode 100644 index.html (limited to 'index.html') diff --git a/index.html b/index.html new file mode 100644 index 0000000..e27bcc8 --- /dev/null +++ b/index.html @@ -0,0 +1,7 @@ +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 +#

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