vericert - Vericert is a formally verified high-level synthesis tool.

	Commit message (Collapse)	Author	Age	Files	Lines
*	Annonimize submissiondev/asplos	Yann Herklotz	2023-08-10	81	-216/+120
\|
*	Add comments next to admitted theorems	Yann Herklotz	2023-08-10	3	-6/+6
\|
*	Finish final forward simulation correctness	Yann Herklotz	2023-08-10	15	-7305/+172
\|
*	Abort steytin proofs	Yann Herklotz	2023-08-10	1	-2/+2
\|
*	Add Bambu synthesis and ClockRegisters	Yann Herklotz	2023-08-10	4	-0/+414
\|
*	Fix backend hardware generation and scheduling	Yann Herklotz	2023-08-10	13	-66/+114
\|
*	Remove tseytin transformation temporarily	Yann Herklotz	2023-08-10	1	-1/+1
\|
*	Put every load/store into it's own cycle	Yann Herklotz	2023-08-02	3	-179/+204
\|
*	Finish datapath memory generation	Yann Herklotz	2023-08-02	2	-409/+546
\|
*	Fixing store transformation	Yann Herklotz	2023-08-01	3	-96/+179
\|
*	Add fixes to main memory generation proof	Yann Herklotz	2023-07-31	2	-799/+808
\|
*	Remove RTLParFu and fix DMemorygen.v	Yann Herklotz	2023-07-31	5	-1974/+1949
\|
*	Add beginning to memory generation proof	Yann Herklotz	2023-07-29	22	-2671/+6810
\|
*	Add equivalence classes	Yann Herklotz	2023-07-11	10	-192/+552
\|
*	Add if-conversion decision procedure	Yann Herklotz	2023-07-06	6	-29/+60
\|
*	Fix man file generation	Yann Herklotz	2023-06-26	2	-4/+3
\|
*	Update cohpred with renamed files	Yann Herklotz	2023-06-26	1	-0/+0
\|
*	Add COHPREDSTAMP to .gitignore	Yann Herklotz	2023-06-26	1	-0/+2
\|
*	Finish some proofs and remove unnecessary Admitted	Yann Herklotz	2023-06-26	7	-33/+76
\|
*	Finish mutual exclusivity check	Yann Herklotz	2023-06-25	5	-31/+150
\|
*	Finish SMT proof	Yann Herklotz	2023-06-23	1	-3/+100
\|
*	Add SMTCoq solver as dependency	Yann Herklotz	2023-06-21	14	-71/+233
\|
*	Update makefile to build cohpred	Yann Herklotz	2023-06-19	1	-2/+6
\|
*	Update cohpred library	Yann Herklotz	2023-06-18	1	-0/+0
\|
*	Update cohpred git submodule	Yann Herklotz	2023-06-14	2	-1/+1
\|
*	Add CohPred and SMTCoq dependency	Yann Herklotz	2023-06-12	4	-2/+29
\|
*	Finish complete evaluability proof	Yann Herklotz	2023-06-10	1	-19/+88
\|
*	Try to prove main theorem	Yann Herklotz	2023-06-10	1	-0/+5
\| \| \| \|	Missing some link between forests
*	Add more to proof of evaluability	Yann Herklotz	2023-06-10	2	-1/+57
\|
*	Finish abstract_sequence_evaluable_m	Yann Herklotz	2023-06-09	1	-1/+104
\|
*	Prove abstract_sequence_evaluable	Yann Herklotz	2023-06-09	1	-0/+2
\|
*	Finish abstract_sequence_evaluable_fold2	Yann Herklotz	2023-06-09	1	-5/+42
\|
*	Finish abstract_sequence_evaluable_fold	Yann Herklotz	2023-06-09	1	-12/+68
\|
*	Add outline of proof of evaluable when predicate is false	Yann Herklotz	2023-06-09	1	-19/+54
\|
*	Add proof outline for evaluability	Yann Herklotz	2023-06-08	2	-20/+44
\|
*	Work towards proving evaluability	Yann Herklotz	2023-06-05	3	-38/+169
\|
*	Move around generating functions	Yann Herklotz	2023-06-03	2	-68/+68
\|
*	Add lp_solve dependency to nix	Yann Herklotz	2023-06-02	1	-1/+1
\|
*	Fix proof of predicates completely	Yann Herklotz	2023-06-02	2	-7/+24
\|
*	Fix top-level proof with Isetpred missing	Yann Herklotz	2023-06-02	1	-12/+55
\|
*	Finished the propert version of from_predicated_sem_pred_expr2	Yann Herklotz	2023-06-02	7	-44/+316
\|
*	Finish from_predicated_sem_pred_expr	Yann Herklotz	2023-05-31	1	-8/+97
\|
*	Remove unnecessary assumption from sem_merge_list	Yann Herklotz	2023-05-30	1	-4/+3
\|
*	Fix other proofs and attempt from_predicated proof	Yann Herklotz	2023-05-30	1	-7/+26
\|
*	Prove merge list_translation	Yann Herklotz	2023-05-30	1	-2/+16
\|
*	Prove fold_right over Elist	Yann Herklotz	2023-05-30	1	-4/+74
\|
*	Finish second flap2 proof	Yann Herklotz	2023-05-30	1	-1/+9
\|
*	Finished painful product proof	Yann Herklotz	2023-05-30	5	-13/+127
\|
*	Prove more admitted theorems	Yann Herklotz	2023-05-29	6	-47/+190
\|
*	Finish two AbstrSemIdent false proofs	Yann Herklotz	2023-05-28	1	-11/+50
\|