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

	Commit message (Expand)	Author	Age	Files	Lines
...
\| * \| \|	Merge remote-tracking branch 'james/arrays-proof' into develop	Yann Herklotz	2020-06-20	4	-71/+369
\| \|\ \ \ \| \| \|/ / \| \|/\| \|
\| * \| \|	Add more unproven instructions, Admitted equiv to spec	Yann Herklotz	2020-06-14	2	-21/+26
* \| \| \|	Finish ILoad proof with some assumptions:	James Pollard	2020-06-24	2	-8/+34
* \| \| \|	Normalise entire expression to avoid overflow issues.	James Pollard	2020-06-23	3	-272/+278
* \| \| \|	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	3	-89/+177
\| \|_\|/ \|/\| \|
* \| \|	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	1	-14/+172
\| \|/ \|/\|
* \|	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	1	-12/+15
* \|	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 Inop proof to work with new array semantics.	James Pollard	2020-06-17	1	-7/+36
* \|	Some (very) useful lemmas about arrays.	James Pollard	2020-06-17	1	-4/+32
* \|	Use NBAs for loads and stores.	James Pollard	2020-06-17	2	-4/+4
* \|	Array semantics now uses dependent Array type.	James Pollard	2020-06-14	2	-9/+10
* \|	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	6	-834/+205
\|\\|
\| *	Add declaration of loads	Yann Herklotz	2020-06-12	2	-4/+6
\| *	Fix declaring function arguments correctly	Yann Herklotz	2020-06-12	2	-9/+66
\| *	Remove Verilog proofs	Yann Herklotz	2020-06-12	2	-132/+4
\| *	Declare all registers properly in HTL	Yann Herklotz	2020-06-12	3	-51/+95
\| *	Generate Verilog from HTL	Yann Herklotz	2020-06-12	1	-644/+40
* \|	Some work on store proof.	James Pollard	2020-06-12	1	-11/+38
* \|	Rough outline of stack address proof	James Pollard	2020-06-11	2	-30/+105
* \|	Working on proof.	James Pollard	2020-06-11	3	-41/+136
\|/
*	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	1	-31/+92
\|\
\| *	Finished main proof with small assumptions	Yann Herklotz	2020-06-04	2	-34/+94
* \|	Fix HTLgenspec proof for arrays.	James Pollard	2020-06-03	1	-31/+43
* \|	Merge branch 'develop' into arrays-proof	James Pollard	2020-06-03	2	-47/+45
\|\\|
\| *	Uncomment proof	Yann Herklotz	2020-06-03	2	-43/+41
* \|	HTLgenspec status in line with develop	James Pollard	2020-06-03	2	-26/+56
* \|	Copy over load/store from Veriloggen to HTLgen.	James Pollard	2020-06-03	1	-5/+36
* \|	Merge branch 'develop' into arrays-proof	James Pollard	2020-06-03	2	-4/+30
\|\\|
\| *	Add proof to final_states	Yann Herklotz	2020-06-02	1	-1/+3
\| *	Add proof for initial state	Yann Herklotz	2020-06-02	2	-3/+27
* \|	Keep track of declarations in HTLgen.	James Pollard	2020-06-03	1	-23/+62
* \|	Merge branch 'develop' into arrays-proof	James Pollard	2020-06-02	3	-82/+152
\|\\|
\| *	Get whole proof to compile	Yann Herklotz	2020-06-02	1	-14/+17
\| *	Shorten the proof a bit	Yann Herklotz	2020-06-02	1	-41/+15
\| *	Add proof for equivalence of mov	Yann Herklotz	2020-06-02	2	-38/+110
\| *	Add lemmas for preservation of globals	Yann Herklotz	2020-06-01	2	-29/+50