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
/
Predicate.v
Commit message (
Expand
)
Author
Age
Files
Lines
*
Finish sem_update_instr finally
Yann Herklotz
2023-02-12
1
-0
/
+52
*
Change evaluation of predicates and remove forest_evaluable
Yann Herklotz
2023-02-11
1
-0
/
+50
*
Add proof using to ifconversionproof
Yann Herklotz
2022-09-29
1
-1
/
+1
*
Add global monad notation using Instances
Yann Herklotz
2022-09-26
1
-1
/
+1
*
Work on implementing abstract predicates
Yann Herklotz
2022-07-19
1
-140
/
+193
*
Rearrange definitions and create IfConversion template
Yann Herklotz
2022-06-06
1
-0
/
+12
*
Fix many more lemmas
Yann Herklotz
2022-06-05
1
-0
/
+9
*
Work on CondElim proof
Yann Herklotz
2022-06-03
1
-3
/
+3
*
Abstract useful function into Predicate.v
Yann Herklotz
2022-05-31
1
-0
/
+7
*
Improve simplification of predicates
Yann Herklotz
2021-11-14
1
-2
/
+10
*
Add the tseytin transformation instead
Yann Herklotz
2021-11-14
1
-210
/
+359
*
Improve simplification of predicates
Yann Herklotz
2021-11-13
1
-57
/
+80
*
Add simplify operation and simplify IfConversion
Yann Herklotz
2021-11-11
1
-0
/
+58
*
Add intermediate step in proof of sem pres
Yann Herklotz
2021-10-27
1
-0
/
+26
*
Work more on equivalence of SAT
Yann Herklotz
2021-10-26
1
-0
/
+15
*
Add type-class proofs to Predicate.v
Yann Herklotz
2021-10-24
1
-4
/
+207
*
Add work towards decidability of SAT solver
Yann Herklotz
2021-10-21
1
-0
/
+201