- 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 scheduling pass to go from RTLBlock to RTLPar.
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.