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
/
hls
Commit message (
Expand
)
Author
Age
Files
Lines
...
*
Merge remote-tracking branch 'origin/dev/scheduling' into dev/scheduling
Yann Herklotz
2022-06-28
2
-21
/
+92
|
\
|
*
Merge remote-tracking branch 'origin/dev/scheduling' into dev/scheduling
Yann Herklotz
2022-06-28
6
-18
/
+22
|
|
\
|
*
|
Add if-conversion spec
Yann Herklotz
2022-06-28
2
-21
/
+92
*
|
|
Update if-conversion function
Yann Herklotz
2022-06-28
2
-3
/
+10
|
|
/
|
/
|
*
|
Update build files for documentation
Yann Herklotz
2022-06-24
1
-3
/
+3
*
|
Update documentation for Gible
Yann Herklotz
2022-06-24
5
-15
/
+19
|
/
*
Work on the if-conversion proof
Yann Herklotz
2022-06-09
2
-32
/
+49
*
Rearrange definitions and create IfConversion template
Yann Herklotz
2022-06-06
6
-105
/
+301
*
Finish CondElim proof and fix Gible semantics
Yann Herklotz
2022-06-06
3
-134
/
+246
*
Fix many more lemmas
Yann Herklotz
2022-06-05
4
-109
/
+329
*
Remove inv H1 from condelim proof
Yann Herklotz
2022-06-05
1
-3
/
+3
*
Add condelim proof
Yann Herklotz
2022-06-05
1
-85
/
+169
*
work on condelimproof
Yann Herklotz
2022-06-04
1
-66
/
+72
*
Add to condelim proof
Yann Herklotz
2022-06-04
1
-2
/
+111
*
Working towards ElimCond proof
Yann Herklotz
2022-06-03
2
-34
/
+87
*
Work on CondElim proof
Yann Herklotz
2022-06-03
6
-24
/
+111
*
Do not remove dependencies from control-flow
Yann Herklotz
2022-05-31
1
-1
/
+6
*
Place both case statements into the same always block
Yann Herklotz
2022-05-31
1
-4
/
+5
*
Abstract useful function into Predicate.v
Yann Herklotz
2022-05-31
1
-0
/
+7
*
Fix hardware generation
Yann Herklotz
2022-05-31
1
-59
/
+79
*
Fix GibleSeqgenproof with new semantics
Yann Herklotz
2022-05-31
2
-54
/
+70
*
Fix update function for control-flow
Yann Herklotz
2022-05-31
1
-1
/
+12
*
Update the Gible semantics with correct termination
Yann Herklotz
2022-05-31
1
-9
/
+10
*
Simplify if-conversion pass
Yann Herklotz
2022-05-31
1
-30
/
+80
*
Add new translation passes for if-conversion
Yann Herklotz
2022-05-31
3
-0
/
+337
*
Fix code generation in partitioning and scheduling
Yann Herklotz
2022-05-27
4
-9
/
+54
*
Rewrite a lot fixing scheduling of Gible
Yann Herklotz
2022-05-27
19
-615
/
+340
*
Add new block generation for Gible
Yann Herklotz
2022-05-26
4
-453
/
+291
*
Translate the base languages
Yann Herklotz
2022-05-25
7
-437
/
+431
*
Famous proven but not tested has been fixed
Yann Herklotz
2022-05-12
3
-13
/
+13
*
Completely finish RTLBlockgenproof
Yann Herklotz
2022-05-12
2
-24
/
+171
*
Remove imm_succ from match_block
Yann Herklotz
2022-05-12
1
-100
/
+27
*
Add rest of the proofs
Yann Herklotz
2022-05-12
1
-12
/
+272
*
Up to Icall is now proven
Yann Herklotz
2022-05-12
2
-86
/
+382
*
Try to expand the definition of match_code
Yann Herklotz
2022-05-12
1
-23
/
+35
*
Finish Inop proof for basic block generation
Yann Herklotz
2022-05-11
1
-12
/
+24
*
Add new definitions of match_code
Yann Herklotz
2022-05-11
1
-8
/
+13
*
Change the specification of the RTLBlockgenproof
Yann Herklotz
2022-05-09
1
-31
/
+45
*
Try to work on refining the match_states predicate
Yann Herklotz
2022-05-06
1
-9
/
+22
*
Try out a new match_code predicate
Yann Herklotz
2022-04-25
1
-13
/
+30
*
Work on proof of Inop
Yann Herklotz
2022-04-24
1
-32
/
+145
*
Fix translation passes with new semantics
Yann Herklotz
2022-04-23
5
-72
/
+75
*
Change the definition of RTLBlock
Yann Herklotz
2022-04-21
2
-97
/
+93
*
Work on smallstep proof
Yann Herklotz
2022-04-21
1
-2
/
+22
*
Start work on Inop proof
Yann Herklotz
2022-04-20
1
-0
/
+3
*
Extract some lemmas from the main proof
Yann Herklotz
2022-04-18
2
-24
/
+87
*
Proof of the initial state matching
Yann Herklotz
2022-04-12
2
-3
/
+38
*
Add intermediate files
Yann Herklotz
2022-04-08
4
-78
/
+143
*
Work on the match_states definition
Yann Herklotz
2022-04-05
3
-17
/
+26
*
Add basic blocks to the stackframe
Yann Herklotz
2022-04-05
5
-32
/
+54
[prev]
[next]