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

	Commit message (Collapse)	Author	Age	Files	Lines
*	Finish load proofdev/scheduling	Yann Herklotz	2023-11-05	8	-1930/+3243
\|
*	Changed and proved some more theorems	Yann Herklotz	2023-10-30	4	-1338/+2192
\|
*	Fix more proofs moving to proving instructions	Yann Herklotz	2023-10-20	2	-13/+247
\|
*	Fix compilation without FunctionUnits	Yann Herklotz	2023-10-20	1	-1/+1
\|
*	Finish Giblesubpargenproof	Yann Herklotz	2023-10-20	1	-7/+13
\|
*	Nearly finish the subpargenproof	Yann Herklotz	2023-10-20	1	-2/+130
\|
*	Add the actual proof	Yann Herklotz	2023-10-19	3	-0/+2025
\|
*	Finished most of the giblesubpar proof	Yann Herklotz	2023-10-19	9	-41/+138
\|
*	Add more sub languages	Yann Herklotz	2023-10-19	4	-1/+608
\|
*	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	10	-262/+498
\|
*	Add settings file	Yann Herklotz	2023-10-06	2	-0/+5
\|
*	Finish eval_correct proof	Yann Herklotz	2023-10-06	5	-248/+1043
\|
*	Add incremental evaluability check	Yann Herklotz	2023-09-25	6	-11/+1127
\|
*	Add better implementation of evaluability	Yann Herklotz	2023-09-22	1	-28/+38
\|
*	Add timing of scheduling to Compiler.v	Yann Herklotz	2023-09-22	2	-40/+40
\|
*	Add new constraints checking	Yann Herklotz	2023-09-22	1	-1/+56
\|
*	Fix documentation generation	Yann Herklotz	2023-09-17	4	-330/+625
\|
*	Add Bambu synthesis and ClockRegisters	Yann Herklotz	2023-08-11	4	-0/+414
\|
*	Fix backend hardware generation and scheduling	Yann Herklotz	2023-08-11	13	-66/+114
\|
*	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
\|