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

	Commit message (Collapse)	Author	Age	Files	Lines
*	Add the actual proof	Yann Herklotz	2023-10-19	3	-0/+2025
\|
*	Finished most of the giblesubpar proof	Yann Herklotz	2023-10-19	5	-41/+131
\|
*	Add more sub languages	Yann Herklotz	2023-10-19	3	-0/+603
\|
*	More work on proof	Yann Herklotz	2023-10-18	6	-118/+676
\|
*	Add callstate correct proof	Yann Herklotz	2023-10-13	2	-13/+248
\|
*	Add changes for HTL proof	Yann Herklotz	2023-10-13	9	-260/+493
\|
*	Finish eval_correct proof	Yann Herklotz	2023-10-06	5	-248/+1043
\|
*	Add incremental evaluability check	Yann Herklotz	2023-09-25	4	-6/+1116
\|
*	Add better implementation of evaluability	Yann Herklotz	2023-09-22	1	-28/+38
\|
*	Add new constraints checking	Yann Herklotz	2023-09-22	1	-1/+56
\|
*	Add Bambu synthesis and ClockRegisters	Yann Herklotz	2023-08-11	1	-0/+245
\|
*	Fix backend hardware generation and scheduling	Yann Herklotz	2023-08-11	6	-42/+80
\|
*	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	17	-2662/+6789
\|
*	Add equivalence classes	Yann Herklotz	2023-07-11	6	-191/+334
\|
*	Add if-conversion decision procedure	Yann Herklotz	2023-07-06	5	-27/+53
\|
*	Finish some proofs and remove unnecessary Admitted	Yann Herklotz	2023-06-26	5	-32/+74
\|
*	Finish mutual exclusivity check	Yann Herklotz	2023-06-25	4	-30/+121
\|
*	Finish SMT proof	Yann Herklotz	2023-06-23	1	-3/+100
\|
*	Add SMTCoq solver as dependency	Yann Herklotz	2023-06-21	6	-47/+216
\|
*	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
\|
*	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	6	-44/+304
\|
*	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	4	-11/+125
\|
*	Prove more admitted theorems	Yann Herklotz	2023-05-29	5	-47/+169
\|
*	Finish two AbstrSemIdent false proofs	Yann Herklotz	2023-05-28	1	-11/+50
\|
*	Finish max predicate proof	Yann Herklotz	2023-05-28	1	-1/+78
\|
*	Finish proofs in GiblePargenproofForward.v	Yann Herklotz	2023-05-28	2	-5/+49
\|
*	Work on forward proofs	Yann Herklotz	2023-05-28	2	-1/+18
\|