aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2021-10-09 14:30:37 +0100
committerYann Herklotz <git@yannherklotz.com>2021-10-09 14:30:37 +0100
commit0f7aef619bc13711f942108be97eb9966f7826e1 (patch)
tree227c1fba872d0b58251f09354deb0d3e67e3dcb9
parentf06e5fc0ee651c3ffe357c3c3302ca1517381b4c (diff)
downloadvericert-kvx-0f7aef619bc13711f942108be97eb9966f7826e1.tar.gz
vericert-kvx-0f7aef619bc13711f942108be97eb9966f7826e1.zip
Update the changelog
-rw-r--r--CHANGELOG.org10
1 files changed, 7 insertions, 3 deletions
diff --git a/CHANGELOG.org b/CHANGELOG.org
index 66f754d..88c0953 100644
--- a/CHANGELOG.org
+++ b/CHANGELOG.org
@@ -7,10 +7,14 @@
** New Features
-- Add *RTLBlock*, a basic block intermediate language that is based on CompCert's
+- 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.
+- Add ~RTLPar~, which can execute groups of instructions in parallel.
+- Add SDC hyper-block scheduling pass to go from RTLBlock to RTLPar using.
+- Add operation chaining support to scheduler.
+- Add ~Abstr~ intermediate language for equivalence checking of schedule.
+- Add built-in verified SAT solver used for equivalence checking of
+ hyper-blocks.
* 2021-10-01 - v1.2.2