index
:
compcert-kvx
CPP22_if_lifting
CPP22_main
master
patched_for_velus
riscV-cmov
ssa
vericert
vericert-kvx
Unnamed repository; edit this file 'description' to name the repository.
about
summary
refs
log
tree
commit
diff
stats
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
Files
Lines
*
Fix proofs for ptr64
vericert-kvx
Yann Herklotz
2022-03-14
5
-64
/
+13
*
Add scheduling oracle to Verilog
Yann Herklotz
2022-03-14
38
-8163
/
+12886
*
Add always inlining
Yann Herklotz
2022-03-13
1
-4
/
+1
*
Small fixes to make extraction pass
Yann Herklotz
2022-03-10
4
-20
/
+6
*
Update .gitignore
Yann Herklotz
2022-03-10
1
-0
/
+3
*
Update Verilog back end
Yann Herklotz
2022-03-10
31
-3411
/
+1092
*
Fix compilation of verilog back end
Yann Herklotz
2022-03-10
2
-102
/
+77
*
Replace omega by lia
Yann Herklotz
2022-03-10
7
-52
/
+57
*
Add proof of splitlong_ptr32
Yann Herklotz
2022-03-10
1
-0
/
+3
*
Add Verilog backend
Yann Herklotz
2022-03-10
33
-0
/
+16929
*
fix missing "formally"
CPP22_main
Sylvain Boulmé
2021-12-10
1
-1
/
+1
*
authors and papers links for the CPP'22 version
Sylvain Boulmé
2021-12-06
2
-2
/
+14
*
more explanation on the web page.
Sylvain Boulmé
2021-12-03
1
-0
/
+2
*
update for CPP_2022 publication
Sylvain Boulmé
2021-12-02
1
-5
/
+6
*
opweights u74
Léo Gourdin
2021-09-17
1
-0
/
+139
*
Revert "[MERGE] weak-software-pipelining in RTLpath"
Léo Gourdin
2021-09-16
47
-3987
/
+229
*
latest coq+ocaml versions
Sylvain Boulmé
2021-09-15
1
-35
/
+12
*
update gitlab-CI from kvx-work
Sylvain Boulmé
2021-09-15
1
-12
/
+35
*
[MERGE] weak-software-pipelining in RTLpath
Léo Gourdin
2021-09-02
47
-229
/
+3987
|
\
|
*
Fix small error
Justus Fasse
2021-08-24
1
-5
/
+5
|
*
Hopefully a proper fix to code motion below side exits + NO register renaming
Justus Fasse
2021-08-21
1
-0
/
+23
|
*
Revert "Fix error"
Justus Fasse
2021-08-21
1
-17
/
+5
|
*
Fix error
Justus Fasse
2021-08-21
1
-5
/
+17
|
*
Remove hopefully useless compiler passes
Justus Fasse
2021-08-21
2
-16
/
+5
|
*
**Ugly** proof of simu_check_single_correct
Justus Fasse
2021-08-18
1
-8
/
+31
|
*
Match naming convention of surrounding code.
Justus Fasse
2021-08-18
1
-2
/
+2
|
*
Merge branch 'kvx-work' into weak-software-pipelining
Justus Fasse
2021-08-17
16
-358
/
+1353
|
|
\
|
*
|
Modified logic to detect inner loops spanned by a superblock
Justus Fasse
2021-08-17
1
-3
/
+10
|
*
|
Remove done TODO comment
Justus Fasse
2021-08-17
1
-2
/
+2
|
*
|
Work-around for prepass-past-side-exits error.
Justus Fasse
2021-08-17
1
-11
/
+17
|
*
|
Make warning about worse schedule with relaxed problem non-fatal unless
Justus Fasse
2021-08-17
1
-1
/
+3
|
*
|
Issue warning when idealized final time is larger than default final
Justus Fasse
2021-08-17
1
-2
/
+6
|
*
|
Make specifying of prepass past side exits heuristic optional
Justus Fasse
2021-08-17
1
-0
/
+1
|
*
|
Fix compilation error
Justus Fasse
2021-08-16
1
-1
/
+3
|
*
|
Use modified dependency calculation that is more generous (timing-wise)
Justus Fasse
2021-08-16
1
-1
/
+1
|
*
|
Supply correct arguments to function
Justus Fasse
2021-08-16
1
-1
/
+1
|
*
|
Remove useless comment
Justus Fasse
2021-08-16
1
-1
/
+0
|
*
|
Remove duplicate function definition
Justus Fasse
2021-08-16
1
-8
/
+0
|
*
|
Better relative estimates by systematically supplying correct liveness
Justus Fasse
2021-08-16
1
-1
/
+2
|
*
|
Insert final restoration code at very end of superblock if possible
Justus Fasse
2021-08-16
1
-22
/
+23
|
*
|
More appropriate name for function
Justus Fasse
2021-08-16
1
-5
/
+2
|
*
|
Experimenting with compiler passes
Justus Fasse
2021-08-16
2
-0
/
+19
|
*
|
Do not restore unnecessary instructions before a predicted Icond
Justus Fasse
2021-08-11
1
-10
/
+16
|
*
|
Add missing dependency for restoration_instructions'
Justus Fasse
2021-08-11
1
-0
/
+24
|
*
|
Allow restoration instructions at the very end of the path.
Justus Fasse
2021-08-11
1
-2
/
+18
|
*
|
More aggressive register renaming
Justus Fasse
2021-08-11
1
-5
/
+12
|
*
|
Make it easier to insert debugging code
Justus Fasse
2021-08-11
1
-3
/
+2
|
*
|
Better variable name and an early exit in rename_regs
Justus Fasse
2021-08-11
1
-5
/
+17
|
*
|
Forgotten change
Justus Fasse
2021-08-11
1
-1
/
+2
|
*
|
Do not incur latency hit for the fake-read of the memory by a side exit
Justus Fasse
2021-08-10
1
-2
/
+16
[next]