index
:
vericert-kvx
arrays-proof
dev-experiments
dev-initial
dev-initial-blocks
dev-michalis
dev-nadesh
dev-nadesh-merge
dev-nadesh-proven
dev/cond-const-prop
dev/div
dev/divider
dev/improved-names
dev/io
dev/predicated-execution
dev/scheduling
dev/value
exp/inl-cse-const
master
michalis
michalis-merge
michalis_merge_2
mpardalos-michalis
oopsla21
save/old-step
wip/reset-signals
Unnamed repository; edit this file 'description' to name the repository.
about
summary
refs
log
tree
commit
diff
stats
log msg
author
committer
range
path:
root
/
src
Commit message (
Expand
)
Author
Age
Files
Lines
*
Fix RTLPar to use instr list list list
Yann Herklotz
2021-02-16
3
-25
/
+33
*
Replace original gather function with new constraints
Yann Herklotz
2021-02-15
1
-15
/
+16
*
Add resource constraints
Yann Herklotz
2021-02-15
1
-6
/
+71
*
Add information about pipeline and comb_delay
Yann Herklotz
2021-02-15
1
-8
/
+41
*
Add data and control dependencies to reworked graph
Yann Herklotz
2021-02-15
1
-43
/
+236
*
Make the schedule a bit neater
Yann Herklotz
2021-02-15
1
-74
/
+63
*
Use proper graph for DFG
Yann Herklotz
2021-02-15
1
-77
/
+113
*
Add more legible names to variables
michalis_merge_2
dev/improved-names
Yann Herklotz
2021-02-12
1
-1
/
+17
*
Add temporary fixes to get everything to compile
dev/predicated-execution
Yann Herklotz
2021-02-12
7
-36
/
+386
*
Fix state generation for if-conversion
Yann Herklotz
2021-02-03
4
-14
/
+21
*
Fix scheduling for if-conversion
Yann Herklotz
2021-02-03
1
-14
/
+90
*
Add predicated values and instructions
Yann Herklotz
2021-02-02
7
-41
/
+92
*
Add if conversion pass
Yann Herklotz
2021-02-02
1
-3
/
+65
*
Add if conversion pass
Yann Herklotz
2021-02-02
1
-0
/
+32
*
Add Vrange and predicates
Yann Herklotz
2021-02-02
8
-66
/
+95
*
Fix OCaml files for compilation
Yann Herklotz
2021-01-31
4
-92
/
+94
*
Fix compilation of Coq
Yann Herklotz
2021-01-30
2
-19
/
+48
*
Fix proofs with better defined equality
Yann Herklotz
2021-01-30
2
-31
/
+57
*
Fix definitions of proofs some more
Yann Herklotz
2021-01-29
4
-106
/
+162
*
Fix the proof for RTLPargen
Yann Herklotz
2021-01-29
1
-32
/
+33
*
Fix HTLPargen and RTLPargen
Yann Herklotz
2021-01-29
2
-56
/
+178
*
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
[next]