index
:
vericert
debug/unhashed
dev-michalis
dev/asplos
dev/div
dev/divider
dev/full-nix-build
dev/mac-op
dev/michalis
dev/scheduling
dev/value
exp/inl-cse-const
master
stable
Vericert is a formally verified high-level synthesis tool.
about
summary
refs
log
tree
commit
diff
stats
log msg
author
committer
range
path:
root
/
src
/
Compiler.v
Commit message (
Expand
)
Author
Age
Files
Lines
*
Finished most of the giblesubpar proof
Yann Herklotz
2023-10-19
1
-0
/
+2
*
Add more sub languages
Yann Herklotz
2023-10-19
1
-1
/
+5
*
Add changes for HTL proof
Yann Herklotz
2023-10-13
1
-2
/
+5
*
Add timing of scheduling to Compiler.v
Yann Herklotz
2023-09-22
1
-1
/
+1
*
Fix backend hardware generation and scheduling
Yann Herklotz
2023-08-11
1
-12
/
+15
*
Add beginning to memory generation proof
Yann Herklotz
2023-07-29
1
-2
/
+7
*
Add if-conversion decision procedure
Yann Herklotz
2023-07-06
1
-2
/
+7
*
Add SMTCoq solver as dependency
Yann Herklotz
2023-06-21
1
-1
/
+2
*
Add new if-conversion pass with top-level fold
Yann Herklotz
2022-09-29
1
-1
/
+16
*
Add new translations to top-level
Yann Herklotz
2022-05-31
1
-1
/
+7
*
Rewrite a lot fixing scheduling of Gible
Yann Herklotz
2022-05-27
1
-12
/
+8
*
Add new block generation for Gible
Yann Herklotz
2022-05-26
1
-2
/
+2
*
Add sphinx documentation
Yann Herklotz
2022-03-26
1
-63
/
+109
*
Remove literal files again
Yann Herklotz
2022-03-26
1
-38
/
+77
*
Final updates to the current documentation
Yann Herklotz
2022-02-25
1
-9
/
+9
*
Start converting comments
Yann Herklotz
2022-02-25
1
-64
/
+38
*
Add bourdoncle to build
Yann Herklotz
2021-12-09
1
-1
/
+1
*
Fix compilation with new HTL language
Yann Herklotz
2021-11-18
1
-10
/
+10
*
Fix generation of RTLParFU
Yann Herklotz
2021-11-17
1
-0
/
+2
*
Merge remote-tracking branch 'origin/dev/divider' into dev/scheduling
Yann Herklotz
2021-11-16
1
-0
/
+1
|
\
|
*
Add operation pipelining
Yann Herklotz
2021-02-22
1
-0
/
+4
|
*
Add RTLPar printing
Yann Herklotz
2021-02-22
1
-0
/
+1
*
|
Add RTLParFU to top-level
Yann Herklotz
2021-11-14
1
-0
/
+2
*
|
Fix compilation of new intermediate languages
Yann Herklotz
2021-10-01
1
-5
/
+8
*
|
Compile HTLPargen again
Yann Herklotz
2021-09-24
1
-2
/
+2
*
|
Remove unnecessary files and proofs
Yann Herklotz
2021-07-11
1
-2
/
+2
*
|
Add docker file and some comments
Yann Herklotz
2021-07-09
1
-0
/
+2
*
|
Remove Admitted in the highest of top-levels
v1.2.0
Yann Herklotz
2021-04-07
1
-5
/
+10
*
|
Add option to turn on/off ram inferrence
Yann Herklotz
2021-03-02
1
-2
/
+4
|
/
*
Add option to turn off if-conversion
Yann Herklotz
2021-02-16
1
-1
/
+2
*
Add predicated values and instructions
Yann Herklotz
2021-02-02
1
-2
/
+5
*
Add Vrange and predicates
Yann Herklotz
2021-02-02
1
-2
/
+0
*
Fix imports in Coq modules
Yann Herklotz
2021-01-21
1
-43
/
+33
*
Add missing modules to extraction and compile
Yann Herklotz
2021-01-13
1
-2
/
+4
*
Add extraction and loop pipelining stage
Yann Herklotz
2020-12-17
1
-1
/
+4
*
Update Compiler proof with all optimisations
Yann Herklotz
2020-11-28
1
-39
/
+72
*
Update documentation for Compiler.v
Yann Herklotz
2020-11-26
1
-0
/
+84
*
Add optimisations to output
Yann Herklotz
2020-11-02
1
-15
/
+73
*
Add printing of intermediate rtlblock language
Yann Herklotz
2020-10-23
1
-1
/
+5
*
Finish implementing scheduling and add top level export
Yann Herklotz
2020-10-20
1
-3
/
+7
*
Add renumbering to compiler passes
Yann Herklotz
2020-10-18
1
-0
/
+1
*
Add fixes to run scheduling on compilation
Yann Herklotz
2020-09-03
1
-1
/
+14
*
Remove check mpass
Yann Herklotz
2020-07-24
1
-2
/
+0
*
Change name to Vericert
Yann Herklotz
2020-07-14
1
-3
/
+3
*
Fixes to operators
Yann Herklotz
2020-07-07
1
-0
/
+2
*
Rename asm to verilog
Yann Herklotz
2020-07-06
1
-9
/
+10
*
Add top level backward simulation
Yann Herklotz
2020-07-06
1
-15
/
+112
*
HTLgenproof compiles again
Yann Herklotz
2020-07-06
1
-1
/
+6
*
Add htl pretty printing
Yann Herklotz
2020-06-30
1
-0
/
+2
*
Fix top level invocation to translate through HTL
Yann Herklotz
2020-06-12
1
-3
/
+6
[next]