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
Commit message (
Expand
)
Author
Age
Files
Lines
*
Refactoring RTLBlock and RTLPar
Yann Herklotz
2021-01-29
3
-297
/
+205
*
Finish all proofs except executing basic blocks
Yann Herklotz
2021-01-27
1
-1
/
+4
*
Add more proofs for RTLPargen correctness
Yann Herklotz
2021-01-27
3
-26
/
+97
*
Add basic block matching and proof
Yann Herklotz
2021-01-26
1
-3
/
+78
*
Remove the schedule oracle
Yann Herklotz
2021-01-26
2
-518
/
+515
*
Add an inductive to enter the basic block
Yann Herklotz
2021-01-26
1
-3
/
+3
*
Use basic blocks in context to help proof
Yann Herklotz
2021-01-26
1
-11
/
+15
*
Add destruction to context match expressions
Yann Herklotz
2021-01-26
1
-2
/
+5
*
Remove match on basic blocks
Yann Herklotz
2021-01-23
1
-6
/
+0
*
Add match_states for RTLPargen proof
Yann Herklotz
2021-01-22
2
-4
/
+78
*
Fix imports to remove warnings when compiling
Yann Herklotz
2021-01-22
7
-49
/
+101
*
Fix types with new changes in RTLBlock
Yann Herklotz
2021-01-22
4
-91
/
+133
*
Define RTLPar semantics
Yann Herklotz
2021-01-22
2
-172
/
+85
*
Add top-level semantics definitions
Yann Herklotz
2021-01-22
1
-0
/
+17
*
Add semantics for RTLBlock
Yann Herklotz
2021-01-22
2
-12
/
+68
*
Add semantics for RTLBlockInstr and RTLBlock
Yann Herklotz
2021-01-22
2
-22
/
+72
*
Share code between RTLBlock and Par
Yann Herklotz
2021-01-21
4
-149
/
+314
*
Fix imports in Coq modules
Yann Herklotz
2021-01-21
7
-116
/
+162
*
Improve expression equality proof
Yann Herklotz
2021-01-21
1
-57
/
+17
*
Translate from RTLBlock to RTLPar
Yann Herklotz
2021-01-13
1
-201
/
+39
*
Correct translation of scheduling with oracle check
Yann Herklotz
2021-01-13
1
-4
/
+53
*
Remove HTLSchedulegen
Yann Herklotz
2021-01-13
1
-42
/
+0
*
Add missing modules to extraction and compile
Yann Herklotz
2021-01-13
2
-4
/
+5
*
Add RTLPargen.v
Yann Herklotz
2021-01-13
1
-0
/
+27
*
Add HTLPargen translation
Yann Herklotz
2021-01-13
1
-50
/
+130
*
Add conversion from RTLPar to HTL
Yann Herklotz
2021-01-12
1
-0
/
+633
*
Add calculations of max_reg and state in RTLPar
Yann Herklotz
2021-01-12
1
-0
/
+42
*
Remove unnecessary definition of check
Yann Herklotz
2021-01-12
1
-6
/
+4
*
Add concat function to abstract_sequence
Yann Herklotz
2021-01-12
1
-4
/
+11
*
Define scheduleoracle function
Yann Herklotz
2021-01-12
1
-6
/
+131
*
Add proof of empty items
Yann Herklotz
2021-01-11
1
-0
/
+10
*
Improve definition of forest for infinite registers
Yann Herklotz
2021-01-11
1
-4
/
+10
*
Add top level semantics for forests
Yann Herklotz
2021-01-11
1
-1
/
+19
*
Add equality check for symbolic expressions
Yann Herklotz
2021-01-11
1
-0
/
+347
*
Add correct copyright notices in files
Yann Herklotz
2021-01-10
13
-0
/
+118
*
Add comments to pipelining code
Yann Herklotz
2021-01-06
3
-9
/
+25
*
Invert logic on the variant function
Yann Herklotz
2020-12-30
1
-2
/
+2
*
Fix whitespace
Yann Herklotz
2020-12-17
6
-752
/
+748
*
Add extraction and loop pipelining stage
Yann Herklotz
2020-12-17
3
-3
/
+19
*
Modify software pipelining for build
Yann Herklotz
2020-12-17
12
-247
/
+198
*
Add Software pipelining stage by tristan et al.
Yann Herklotz
2020-12-17
12
-0
/
+2429
*
Update Compiler proof with all optimisations
Yann Herklotz
2020-11-28
1
-39
/
+72
*
Fix build for Coq 8.12.1
Yann Herklotz
2020-11-26
8
-26
/
+255
*
Update documentation for Compiler.v
Yann Herklotz
2020-11-26
1
-0
/
+84
*
More fixes to the proof
Yann Herklotz
2020-11-14
1
-4
/
+5
*
[Fix #9] Fix correctness proof for Oshrximm
Yann Herklotz
2020-11-14
1
-4
/
+90
*
Fix compilation issue
Yann Herklotz
2020-11-10
3
-12
/
+12
*
Change and add back HTLgen
Yann Herklotz
2020-11-09
4
-10
/
+33
*
Update definition of Vneg
Yann Herklotz
2020-11-07
2
-2
/
+2
*
Finish implementation of shrx_shrx_alt_equiv
Yann Herklotz
2020-11-05
1
-74
/
+133
[next]