From a6fdaf10c24b5b01921b34b1d2cfc9ef3c23d50d Mon Sep 17 00:00:00 2001 From: ymherklotz Date: Sun, 19 Sep 2021 00:54:08 +0000 Subject: deploy: 8d74fffc72abb3cc20df691d9d40c73fbd1c0c27 --- index.html | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) (limited to 'index.html') diff --git a/index.html b/index.html index 1fb452f..09d5dab 100644 --- a/index.html +++ b/index.html @@ -2,8 +2,12 @@ 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 -#

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 +

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 #

Papers #

OOPSLA ‘21
Yann Herklotz, James D. Pollard, Nadesh Ramanathan, and John Wickerson. Formal Verification of High-Level Synthesis. In Proc. ACM Program. Lang. 5, OOPSLA, 2021. [pdf]
LATTE ‘21
Yann Herklotz and John Wickerson. High-level synthesis tools should be proven -- cgit