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

	Commit message (Collapse)	Author	Age	Files	Lines
*	Fix pretty printing bug in Verilog	Yann Herklotz	2020-11-02	1	-2/+2
\|
*	WIP on RTLBlock semantics	Yann Herklotz	2020-11-02	1	-12/+98
\|
*	Add optimisations to output	Yann Herklotz	2020-11-02	2	-15/+74
\|
*	Add flag to control if scheduling is active	Yann Herklotz	2020-11-01	1	-0/+1
\|
*	Improve performance dramatically for RTLBlock generation	Yann Herklotz	2020-10-31	1	-17/+19
\|
*	Fix bugs in Scheduling	Yann Herklotz	2020-10-31	1	-3/+12
\|
*	Add tbl_to_casestatement into extraction	Yann Herklotz	2020-10-26	2	-11/+26
\|
*	Fix build error with ValueVal	Yann Herklotz	2020-10-26	1	-2/+8
\|
*	Add printing of intermediate rtlblock language	Yann Herklotz	2020-10-23	3	-1/+7
\|
*	Fix printing of negative numbers	Yann Herklotz	2020-10-23	1	-1/+5
\|
*	Fix scheduling for loads and stores with WAR dependencies	Yann Herklotz	2020-10-23	1	-16/+120
\|
*	Finish implementing scheduling and add top level export	Yann Herklotz	2020-10-20	3	-5/+11
\|
*	Fix bug in scheduling	Yann Herklotz	2020-10-20	1	-1/+1
\|
*	Add top level functions to schedule	Yann Herklotz	2020-10-19	1	-49/+115
\|
*	Revert ValueInt.v	Yann Herklotz	2020-10-18	1	-79/+23
\|
*	Add output to scheduling	Yann Herklotz	2020-10-18	1	-25/+282
\|
*	Add renumbering to compiler passes	Yann Herklotz	2020-10-18	1	-0/+1
\|
*	More changes to HTLBlockgen	Yann Herklotz	2020-10-15	1	-2/+2
\|
*	Add HTLBlockgen and more scheduling	Yann Herklotz	2020-10-15	3	-42/+921
\|
*	Add long and bool support to value	Yann Herklotz	2020-10-06	1	-23/+79
\|
*	Add fixes to run scheduling on compilation	Yann Herklotz	2020-09-03	2	-1/+15
\|
*	Scheduling added to partitioning	Yann Herklotz	2020-09-03	1	-3/+2
\|
*	Add scheduling	Yann Herklotz	2020-09-03	2	-0/+181
\|
*	Fix bug for basic block construction in loops	Yann Herklotz	2020-08-31	1	-3/+7
\|
*	Add working partitioning algorithm	Yann Herklotz	2020-08-31	4	-42/+175
\|
*	Continue on Partitioning algorithm	Yann Herklotz	2020-08-30	3	-14/+66
\|
*	Add RTLBlock intermediate language	Yann Herklotz	2020-08-30	19	-3/+178
\|
*	Add html generation and clean Coq files	Yann Herklotz	2020-08-13	4	-7/+3
\|
*	Finished all the proofsv1.0.0	Yann Herklotz	2020-08-13	3	-39/+46
\| \| \| \|	Removed support for case statements temporarily.
*	Remove unnecessary commented proof	Yann Herklotz	2020-08-12	1	-23/+0
\|
*	Finish proof of conditionals	Yann Herklotz	2020-08-12	1	-4/+11
\|
*	Nearly finished all proofs	Yann Herklotz	2020-08-12	1	-48/+228
\|
*	Remove alignment constraint during translation.	James Pollard	2020-08-11	2	-67/+69
\| \| \| \|	This is now inferred from the memory model.
*	Remove last admits from istore	Yann Herklotz	2020-08-04	1	-2/+3
\|
*	Finish istore and iload without any admits	Yann Herklotz	2020-08-04	2	-119/+115
\|
*	No admitted in iload proof	Yann Herklotz	2020-08-04	1	-38/+72
\|
*	Merge remote-tracking branch 'james/develop' into develop	Yann Herklotz	2020-08-04	1	-5/+6
\|\
\| *	Fix broken proof.	James Pollard	2020-08-04	1	-5/+6
\| \|
* \|	Add expr_ok proof	Yann Herklotz	2020-08-04	1	-11/+25
\|/
*	Fix first part of istore	Yann Herklotz	2020-08-04	1	-40/+43
\|
*	Fix iload proof	Yann Herklotz	2020-08-04	2	-43/+52
\|
*	Add proof of divisibility	Yann Herklotz	2020-08-04	1	-21/+14
\|
*	Remove check mpass	Yann Herklotz	2020-07-24	1	-2/+0
\|
*	More renames to get it to compile	Yann Herklotz	2020-07-24	4	-6/+9
\|
*	Rename to Vericertlib	Yann Herklotz	2020-07-17	1	-0/+0
\|
*	Change name to Vericert	Yann Herklotz	2020-07-14	23	-53/+52
\|
*	Fixes to operators	Yann Herklotz	2020-07-07	4	-6/+12
\|
*	Finished transl_cond	Yann Herklotz	2020-07-07	2	-62/+45
\|
*	Only translate_cond left	Yann Herklotz	2020-07-07	4	-17/+252
\|
*	No admitted in Deterministic proof	Yann Herklotz	2020-07-07	3	-14/+10
\|