diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-09-20 17:23:25 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-09-20 17:23:25 +0100 |
| commit | 9148e1c52b3125da76a7e81aedab42c4d6e046dd (patch) | |
| tree | 7eee1c7c1ba060c97f28134ebab6feb14a79abd6 | |
| parent | b666f88219893c82361606f8652297ecc7fb7a9f (diff) | |
| parent | 5bfd5dd55dc9500a799f9abe7460e14d75455f4e (diff) | |
| download | vericert-kvx-9148e1c52b3125da76a7e81aedab42c4d6e046dd.tar.gz vericert-kvx-9148e1c52b3125da76a7e81aedab42c4d6e046dd.zip | |
Merge branch 'master' into develop
| -rw-r--r-- | CHANGELOG.org | 34 | ||||
| m--------- | docs | 0 |
2 files changed, 22 insertions, 12 deletions
diff --git a/CHANGELOG.org b/CHANGELOG.org index 52db994..af5e771 100644 --- a/CHANGELOG.org +++ b/CHANGELOG.org @@ -1,46 +1,56 @@ # -*- fill-column: 80 -*- +#+title: Vericert Changelog +#+author: Yann Herklotz +#+email: git@ymhg.org -* Vericert Changelog +* Unreleased -** Unreleased - -*** New Features +** 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.2.0 - 2021-04-07 +* 2021-07-12 - v1.2.1 + +Main release for OOPSLA'21 paper. + +- Add better documentation on how to run Vericert. +- Add =Dockerfile= with instructions on how to get figures of the paper. + +* 2021-04-07 - v1.2.0 + +** New Features -- Proper RAM inference support. +- Add memory inference capabilities in generated hardware. -** v1.1.0 - 2020-12-17 +* 2020-12-17 - v1.1.0 Add a stable release with all proofs completed. -** v1.0.1 - 2020-08-14 +* 2020-08-14 - v1.0.1 Release a new minor version fixing all proofs and fixing scripts to generate the badges. -*** Bug Fixes +** Fixes - Fix some of the proofs which were not passing. -** v1.0.0 - 2020-08-13 +* 2020-08-13 - v1.0.0 First release of a fully verified version of Vericert with support for the translation of many C constructs to Verilog. -*** New Features +** 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 +* 2020-04-03 - v0.1.0 This is the first release with working HLS but without any proofs associated with it. diff --git a/docs b/docs -Subproject 3b2ce146bc6e651df8ac9910d08da05d88c06fb +Subproject 5508c21e064276aa4d5146b3af5b6f6e9a4c236 |