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

	Commit message (Expand)	Author	Age	Files	Lines
*	Merge branch 'arrays-proof' into develop	Yann Herklotz	2020-06-22	2	-31/+199
\|\
\| *	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
* \|	Merge branch 'master' into develop	Yann Herklotz	2020-06-22	1	-5/+5
\|\ \
\| * \|	Some fixes, but still buggy probably	Yann Herklotz	2020-06-20	1	-2/+2
\| * \|	Add bugs to support more operations	Yann Herklotz	2020-06-20	1	-4/+4
* \| \|	Merge remote-tracking branch 'james/arrays-proof' into develop	Yann Herklotz	2020-06-20	4	-71/+369
\|\ \ \ \| \|/ / \|/\| / \| \|/
\| *	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
\| \|\
\| * \	Merge branch 'master' into arrays-proof	James Pollard	2020-06-12	6	-834/+205
\| \|\ \
\| * \| \|	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
* \| \| \|	Add more unproven instructions, Admitted equiv to spec	Yann Herklotz	2020-06-14	2	-21/+26
\| \|_\|/ \|/\| \|
* \| \|	Fix addressing bug.	James Pollard	2020-06-12	1	-4/+6
\| \|/ \|/\|
* \|	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
\|/
*	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
* \|	Merge branch 'develop' into arrays-proof	James Pollard	2020-06-01	1	-5/+4
\|\\|