diff options
author | Yann Herklotz <git@yannherklotz.com> | 2021-01-22 11:10:03 +0000 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2021-01-22 11:10:03 +0000 |
commit | 5b1e355266921e101867e5d939b01c965b8cfd44 (patch) | |
tree | efa3eff7592e1dccce4e9d4101b6d6ca88007adc /CHANGELOG.org | |
parent | bb29309103b5dce4fc0a0f6d033a26a80e64f273 (diff) | |
download | vericert-5b1e355266921e101867e5d939b01c965b8cfd44.tar.gz vericert-5b1e355266921e101867e5d939b01c965b8cfd44.zip |
Add change log and rename README
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. |