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

	Commit message (Expand)	Author	Age	Files	Lines
*	Use NBAs for loads and stores.	James Pollard	2020-06-17	1	-2/+2
*	Fix broken proof.	James Pollard	2020-06-12	1	-4/+4
*	Merge branch 'master' into arrays-proof	James Pollard	2020-06-12	1	-24/+81
\|\
\| *	Add declaration of loads	Yann Herklotz	2020-06-12	1	-4/+5
\| *	Fix declaring function arguments correctly	Yann Herklotz	2020-06-12	1	-3/+59
\| *	Declare all registers properly in HTL	Yann Herklotz	2020-06-12	1	-17/+17
* \|	Working on proof.	James Pollard	2020-06-11	1	-3/+15
\|/
*	Fix HTLgenspec proof for arrays.	James Pollard	2020-06-03	1	-31/+43
*	Merge branch 'develop' into arrays-proof	James Pollard	2020-06-03	1	-35/+38
\|\
\| *	Uncomment proof	Yann Herklotz	2020-06-03	1	-31/+34
* \|	HTLgenspec status in line with develop	James Pollard	2020-06-03	1	-25/+54
\|/
*	Add proof for equivalence of mov	Yann Herklotz	2020-06-02	1	-15/+17
*	Small optimisations to proof	Yann Herklotz	2020-05-31	1	-5/+4
*	Merge branch 'develop' of github.com:ymherklotz/CoqUp into develop	Yann Herklotz	2020-05-29	1	-6/+3
\|\
\| *	Improve automation in HTLgenspec.	James Pollard	2020-05-29	1	-6/+3
* \|	Fix compilation moving to PTree	Yann Herklotz	2020-05-29	1	-2/+2
\|/
*	Add top level definition	Yann Herklotz	2020-05-27	1	-60/+65
*	Working on automation	Yann Herklotz	2020-05-26	1	-62/+48
*	Finished proof of spec completely	Yann Herklotz	2020-05-26	1	-3/+61
*	Finished second pass and fixed bug	Yann Herklotz	2020-05-26	1	-17/+36
*	Finished proving the first case	Yann Herklotz	2020-05-25	1	-1/+6
*	Continuing work on proving specification	Yann Herklotz	2020-05-25	1	-15/+212
*	Finish the proof with most assumptions	Yann Herklotz	2020-05-21	1	-1/+1
*	Add proof of translation correctness	Yann Herklotz	2020-05-20	1	-8/+8
*	Remove HTLgen and create the specification	Yann Herklotz	2020-05-07	1	-0/+92