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
/
RTLBlockInstr.v
Commit message (
Expand
)
Author
Age
Files
Lines
*
Change origin of tangled files
Yann Herklotz
2022-03-23
1
-7
/
+7
*
Add first descriptions to org file
Yann Herklotz
2022-03-22
1
-35
/
+14
*
Add comments to allow for literate detangling
Yann Herklotz
2022-03-22
1
-2
/
+4
*
Final updates to the current documentation
Yann Herklotz
2022-02-25
1
-3
/
+3
*
Fix up some more documentation
Yann Herklotz
2022-02-25
1
-32
/
+13
*
Add documentation to RTLBlockInstr
Yann Herklotz
2021-11-11
1
-11
/
+62
*
Add RTLBlockInstr proofs
Yann Herklotz
2021-11-01
1
-0
/
+23
*
Add a predicate to RBsetpred
Yann Herklotz
2021-10-30
1
-4
/
+4
*
Add type-class proofs to Predicate.v
Yann Herklotz
2021-10-24
1
-8
/
+10
*
Add work towards decidability of SAT solver
Yann Herklotz
2021-10-21
1
-222
/
+3
*
Start to prove termination of SAT
Yann Herklotz
2021-10-20
1
-6
/
+0
*
Continuations on proof of predicates
Yann Herklotz
2021-10-19
1
-29
/
+0
*
[sched] Add true and false predicates to type
Yann Herklotz
2021-10-14
1
-1
/
+23
*
Fix naming and remove warnings
Yann Herklotz
2021-10-07
1
-3
/
+3
*
RTLpargen passes compilation again
Yann Herklotz
2021-09-22
1
-2
/
+2
*
Change Inductive to record
Yann Herklotz
2021-09-22
1
-16
/
+15
*
Start adding hashing to RTLPargen
Yann Herklotz
2021-09-20
1
-2
/
+2
*
Merge branch 'master' into develop
Yann Herklotz
2021-09-18
1
-10
/
+31
|
\
|
*
Fix compilation with new CompCert version
Yann Herklotz
2021-09-17
1
-8
/
+8
|
*
Fix proofs for SAT
Yann Herklotz
2021-08-12
1
-6
/
+27
|
*
Remove unnecessary files and proofs
Yann Herklotz
2021-07-11
1
-3
/
+3
*
|
Change naturals to positive in predicates
Yann Herklotz
2021-05-26
1
-44
/
+78
|
/
*
Add temporary fixes to get everything to compile
Yann Herklotz
2021-02-12
1
-1
/
+207
*
Fix state generation for if-conversion
Yann Herklotz
2021-02-03
1
-1
/
+1
*
Add predicated values and instructions
Yann Herklotz
2021-02-02
1
-6
/
+15
*
Add Vrange and predicates
Yann Herklotz
2021-02-02
1
-19
/
+30
*
Fix definitions of proofs some more
Yann Herklotz
2021-01-29
1
-10
/
+0
*
Refactoring RTLBlock and RTLPar
Yann Herklotz
2021-01-29
1
-27
/
+132
*
Add semantics for RTLBlock
Yann Herklotz
2021-01-22
1
-7
/
+1
*
Add semantics for RTLBlockInstr and RTLBlock
Yann Herklotz
2021-01-22
1
-14
/
+21
*
Share code between RTLBlock and Par
Yann Herklotz
2021-01-21
1
-0
/
+147