Vericert’s Documentation

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. Currently, the following C features are supported and have all been proven correct, providing a verified translation from C to Verilog:

• all int operations,

• non-recursive function calls,

• local arrays and pointers, and

• control-flow structures such as if-statements, for-loops, etc…

Content

• Introduction
• COPYING
• Building Vericert
  • Testing
• Using Vericert
  • Running Vericert on the PolyBench/C benchmarks
• Man Page
• Unreleased Features
  • Scheduling
  • Operation Chaining
  • If-conversion
  • Functions
• Scheduling proof
  • Semantic identity properties
  • Backward proof
• Coq Style Guide
  • Code organization
  • Formatting
  • Definitions and Fixpoints
  • Inductives
  • Lemma/Theorem statements
  • Proofs and tactics
  • Naming
  • Example
• Index - Features
• GNU Free Documentation License

Sources

• Compiler Proof
• Gible
• GibleSeq
• Gible Seq
• Gible Seq Generation
• Gible Seq Generation Proof

Publications

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.

LATTE ‘21:

Yann Herklotz and John Wickerson. High-level synthesis tools should be proven correct. In Workshop on Languages, Tools, and Techniques for Accelerator Design, 2021.

Mailing lists

For discussions, you can join the following mailing list: lists.sr.ht/~ymherklotz/vericert-discuss.

For contributing patches to the sourcehut repository: lists.sr.ht/~ymherklotz/vericert-devel.

Indices

• Index

• Search Page