diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-01-22 12:29:37 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-01-22 12:29:37 +0000 |
| commit | 3b2f8885e12fc7f92eeedb2e4b23095ef8617b6a (patch) | |
| tree | 6c94d118b919298ea8b46fb30d0d9bb687e87138 /CHANGELOG.org | |
| parent | 301713c2419196344003dd9708f16ef2eb9f7b37 (diff) | |
| parent | 5b1e355266921e101867e5d939b01c965b8cfd44 (diff) | |
| download | vericert-3b2f8885e12fc7f92eeedb2e4b23095ef8617b6a.tar.gz vericert-3b2f8885e12fc7f92eeedb2e4b23095ef8617b6a.zip | |
Merge branch 'master' into develop
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. |