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
...
*
Finish initial implementation of memory gen
Yann Herklotz
2021-03-01
2
-2
/
+89
*
Change lists in case statements to stmnt_list
Yann Herklotz
2021-03-01
6
-12
/
+30
*
Add initial memory generation
Yann Herklotz
2021-03-01
1
-0
/
+17
*
Fix printing of the final cycle count
Yann Herklotz
2021-02-21
1
-2
/
+15
*
Fix bug in schedule
Yann Herklotz
2021-02-19
1
-2
/
+1
*
Fix schedule for now
Yann Herklotz
2021-02-18
1
-1
/
+2
*
Add udiv and sdiv to constraints
Yann Herklotz
2021-02-17
1
-12
/
+20
*
Remove dead code and add more constraints
Yann Herklotz
2021-02-17
1
-107
/
+16
*
Add option to turn off if-conversion
Yann Herklotz
2021-02-16
5
-4
/
+29
*
Merge branch 'master' into develop
Yann Herklotz
2021-02-16
3
-1
/
+621
|
\
|
*
Remove dependency on Tactics
Yann Herklotz
2021-02-16
1
-1
/
+0
|
*
Add functional units and Sat
Yann Herklotz
2021-02-16
2
-0
/
+621
*
|
Use topological sort for now
Yann Herklotz
2021-02-16
1
-4
/
+9
*
|
Add schedule for new RTLPar type
Yann Herklotz
2021-02-16
1
-29
/
+42
*
|
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
[prev]
[next]