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

	Commit message (Expand)	Author	Age	Files	Lines
...
\| \| * \|	Add bugs to support more operations	Yann Herklotz	2020-06-20	1	-4/+4
\| * \| \|	Add proof of nat equiv	Yann Herklotz	2020-06-20	1	-2/+15
\| * \| \|	Merge remote-tracking branch 'james/arrays-proof' into develop	Yann Herklotz	2020-06-20	9	-111/+725
\| \|\ \ \ \| \| \|/ / \| \|/\| \|
\| * \| \|	Add more unproven instructions, Admitted equiv to spec	Yann Herklotz	2020-06-14	4	-23/+31
* \| \| \|	Finish ILoad proof with some assumptions:	James Pollard	2020-06-24	3	-192/+197
* \| \| \|	Normalise entire expression to avoid overflow issues.	James Pollard	2020-06-23	5	-272/+523
* \| \| \|	Finish off Load proof sketches.	James Pollard	2020-06-22	1	-35/+17
* \| \| \|	Start Aindexed proof.	James Pollard	2020-06-22	2	-19/+226
* \| \| \|	Tidy up proof for Aindexed2scaled.	James Pollard	2020-06-22	4	-90/+231
\| \|_\|/ \|/\| \|
* \| \|	Factor out addressing checks, check signed range.	James Pollard	2020-06-21	1	-10/+17
* \| \|	Lea op now checks alignment.	James Pollard	2020-06-21	1	-12/+15
* \| \|	Finish structure of Aindexed2scaled ILoad proof.	James Pollard	2020-06-20	2	-14/+177
\| \|/ \|/\|
* \|	Working on proof.	James Pollard	2020-06-19	1	-10/+86
* \|	Enforce stack size alignment to fix proof.	James Pollard	2020-06-18	3	-10/+22
* \|	Tidy up proof.	James Pollard	2020-06-18	2	-13/+16
* \|	Finish AInStack proof with minor assertions.	James Pollard	2020-06-18	1	-32/+21
* \|	Fix up ILoad proof.	James Pollard	2020-06-18	1	-95/+58
* \|	Fix array semantics behaviour for undefined values.	James Pollard	2020-06-18	1	-1/+1
* \|	Fix Inop proof to work with new array semantics.	James Pollard	2020-06-17	2	-7/+44
* \|	Some (very) useful lemmas about arrays.	James Pollard	2020-06-17	3	-7/+139
* \|	Use NBAs for loads and stores.	James Pollard	2020-06-17	2	-4/+4
* \|	Fix array semantics merge granularity.	James Pollard	2020-06-17	4	-30/+87
* \|	Array semantics now uses dependent Array type.	James Pollard	2020-06-14	4	-48/+49
* \|	Move some standard tactics to Coquplib.	James Pollard	2020-06-14	1	-0/+10
* \|	Add a basic length-indexed list type.	James Pollard	2020-06-13	1	-0/+123
* \|	Fix broken proof.	James Pollard	2020-06-12	1	-4/+4
* \|	Merge branch 'master' into arrays-proof	James Pollard	2020-06-12	1	-4/+6
\|\\|
\| *	Fix addressing bug.	James Pollard	2020-06-12	1	-4/+6
* \|	Merge branch 'master' into arrays-proof	James Pollard	2020-06-12	14	-1028/+364
\|\\|
\| *	Add declaration of loads	Yann Herklotz	2020-06-12	2	-4/+6
\| *	Fix declaring function arguments correctly	Yann Herklotz	2020-06-12	3	-12/+69
\| *	Fix printing of Verilog with new datatypes	Yann Herklotz	2020-06-12	2	-17/+27
\| *	Remove Verilog proofs	Yann Herklotz	2020-06-12	3	-133/+10
\| *	Declare all registers properly in HTL	Yann Herklotz	2020-06-12	3	-51/+95
\| *	Remove extraction of simulator	Yann Herklotz	2020-06-12	1	-2/+2
\| *	Fix top level invocation to translate through HTL	Yann Herklotz	2020-06-12	2	-4/+8
\| *	Remove Test.v	Yann Herklotz	2020-06-12	1	-99/+0
\| *	Generate Verilog from HTL	Yann Herklotz	2020-06-12	2	-713/+154
* \|	Some work on store proof.	James Pollard	2020-06-12	1	-11/+38
* \|	Rough outline of stack address proof	James Pollard	2020-06-11	3	-34/+109
* \|	Working on proof.	James Pollard	2020-06-11	5	-47/+156
\|/
*	Start fixing proof	James Pollard	2020-06-09	1	-94/+116
*	Fix automation tactic for modified constructor	James Pollard	2020-06-09	1	-2/+4
*	Start extending HTL proof to cover arrays.	James Pollard	2020-06-09	1	-18/+31
*	Merge branch 'develop' into arrays-proof	James Pollard	2020-06-09	4	-56/+156
\|\
\| *	Finished main proof with small assumptions	Yann Herklotz	2020-06-04	5	-59/+157
* \|	Fix HTLgenspec proof for arrays.	James Pollard	2020-06-03	1	-31/+43
* \|	Merge branch 'develop' into arrays-proof	James Pollard	2020-06-03	3	-47/+50
\|\\|
\| *	Uncomment proof	Yann Herklotz	2020-06-03	3	-43/+46
* \|	HTLgenspec status in line with develop	James Pollard	2020-06-03	3	-26/+57