blob: 88c09532d3b86e31ebb4e2fea9061db42ad11436 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
|
# -*- fill-column: 80 -*-
#+title: Vericert Changelog
#+author: Yann Herklotz
#+email: git@ymhg.org
* 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 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
Mainly fix some documentation and remove any ~Admitted~ theorems, even though
these were in parts of the compiler that were never used.
* 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.
* 2020-08-14 - v1.0.1
Release a new minor version fixing all proofs and fixing scripts to generate the
badges.
** Fixes
- Fix some of the proofs which were not passing.
* 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
- Most int instructions and operators.
- Non-recursive function calls.
- Local arrays, structs and unions of type int.
- Pointer arithmetic with int.
* 2020-04-03 - v0.1.0
This is the first release with working HLS but without any proofs associated
with it.
|
