diff options
Diffstat (limited to 'CHANGELOG.org')
| -rw-r--r-- | CHANGELOG.org | 42 |
1 files changed, 42 insertions, 0 deletions
diff --git a/CHANGELOG.org b/CHANGELOG.org new file mode 100644 index 0000000..621683c --- /dev/null +++ b/CHANGELOG.org @@ -0,0 +1,42 @@ +# -*- fill-column: 80 -*- + +* Vericert Changelog + +** Unreleased + +*** New Features + +- 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. + +** v1.1.0 - 2020-12-17 + +Add a stable release with all proofs completed. + +** v1.0.1 - 2020-08-14 + +Release a new minor version fixing all proofs and fixing scripts to generate the +badges. + +*** Bug Fixes + +- Fix some of the proofs which were not passing. + +** v1.0.0 - 2020-08-13 + +First release of a fully verified version of Vericert with support for the +translation of many C constructs to Verilog. + +*** New Features + +- Most int instructions and operators. +- Non-recursive function calls. +- Local arrays, structs and unions of type int. +- Pointer arithmetic with int. + +** v0.1.0 - 2020-04-03 + +This is the first release with working HLS but without any proofs associated +with it. |