- Add
RTLBlock, a basic block intermediate language that is based on CompCert’s RTL. - Add
RTLPar, which can execute groups of instructions in parallel. - Add SDC hyper-block scheduling pass to go from RTLBlock to RTLPar using.
- Add operation chaining support to scheduler.
- Add
Abstrintermediate language for equivalence checking of schedule. - Add built-in verified SAT solver used for equivalence checking of hyper-blocks.
Mainly fix some documentation and remove any Admitted theorems, even though
these were in parts of the compiler that were never used.
Main release for OOPSLA’21 paper.
- Add better documentation on how to run Vericert.
- Add
Dockerfilewith instructions on how to get figures of the paper.
- Add memory inference capabilities in generated hardware.
Add a stable release with all proofs completed.
Release a new minor version fixing all proofs and fixing scripts to generate the badges.
- Fix some of the proofs which were not passing.
First release of a fully verified version of Vericert with support for the translation of many C constructs to Verilog.
- Most int instructions and operators.
- Non-recursive function calls.
- Local arrays, structs and unions of type int.
- Pointer arithmetic with int.
This is the first release with working HLS but without any proofs associated with it.