aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2021-09-18 14:58:16 +0100
committerYann Herklotz <git@yannherklotz.com>2021-09-18 14:58:16 +0100
commita8a537bac50a47a5adce7c5eaa2dac0561e17a4c (patch)
tree1ae6e07c27d41f43f4abd0b1351e8be6ce44b8ca
parentc4436c02648502c4cb327d2018229e62a2c0d1c0 (diff)
downloadvericert-a8a537bac50a47a5adce7c5eaa2dac0561e17a4c.tar.gz
vericert-a8a537bac50a47a5adce7c5eaa2dac0561e17a4c.zip
Improve the changelog
-rw-r--r--CHANGELOG.org34
1 files changed, 24 insertions, 10 deletions
diff --git a/CHANGELOG.org b/CHANGELOG.org
index 621683c..af5e771 100644
--- a/CHANGELOG.org
+++ b/CHANGELOG.org
@@ -1,42 +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.1.0 - 2020-12-17
+* 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
+
+- Add memory inference capabilities in generated hardware.
+
+* 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.