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

	Commit message (Collapse)	Author	Age	Files	Lines
*	Add calculations of max_reg and state in RTLPar	Yann Herklotz	2021-01-12	1	-0/+42
\|
*	Remove unnecessary definition of check	Yann Herklotz	2021-01-12	1	-6/+4
\|
*	Add concat function to abstract_sequence	Yann Herklotz	2021-01-12	1	-4/+11
\|
*	Define scheduleoracle function	Yann Herklotz	2021-01-12	1	-6/+131
\|
*	Add proof of empty items	Yann Herklotz	2021-01-11	1	-0/+10
\| \| \| \|	Proof that correct items are returned from an empty forest.
*	Improve definition of forest for infinite registers	Yann Herklotz	2021-01-11	1	-4/+10
\|
*	Add top level semantics for forests	Yann Herklotz	2021-01-11	1	-1/+19
\|
*	Add equality check for symbolic expressions	Yann Herklotz	2021-01-11	1	-0/+347
\|
*	Add correct copyright notices in files	Yann Herklotz	2021-01-10	13	-0/+118
\|
*	Add comments to pipelining code	Yann Herklotz	2021-01-06	3	-9/+25
\|
*	Invert logic on the variant function	Yann Herklotz	2020-12-30	1	-2/+2
\|
*	Fix whitespace	Yann Herklotz	2020-12-17	6	-752/+748
\|
*	Add extraction and loop pipelining stage	Yann Herklotz	2020-12-17	3	-3/+19
\|
*	Modify software pipelining for build	Yann Herklotz	2020-12-17	12	-247/+198
\|
*	Add Software pipelining stage by tristan et al.	Yann Herklotz	2020-12-17	12	-0/+2429
\|
*	Update Compiler proof with all optimisations	Yann Herklotz	2020-11-28	1	-39/+72
\|
*	Fix build for Coq 8.12.1	Yann Herklotz	2020-11-26	8	-26/+255
\|
*	Update documentation for Compiler.v	Yann Herklotz	2020-11-26	1	-0/+84
\|
*	More fixes to the proof	Yann Herklotz	2020-11-14	1	-4/+5
\|
*	[Fix #9] Fix correctness proof for Oshrximm	Yann Herklotz	2020-11-14	1	-4/+90
\| \| \| \|	This removes all the admitted.
*	Fix compilation issue	Yann Herklotz	2020-11-10	3	-12/+12
\|
*	Change and add back HTLgen	Yann Herklotz	2020-11-09	4	-10/+33
\|
*	Update definition of Vneg	Yann Herklotz	2020-11-07	2	-2/+2
\|
*	Finish implementation of shrx_shrx_alt_equiv	Yann Herklotz	2020-11-05	1	-74/+133
\|
*	Comment out blockgen	Yann Herklotz	2020-11-04	1	-1/+2
\|
*	Quick compile fix	Yann Herklotz	2020-11-04	2	-2/+6
\|
*	Proven with some assumptions	Yann Herklotz	2020-11-04	1	-4/+20
\|
*	Continue to prove signed_neg	Yann Herklotz	2020-11-04	1	-1/+44
\|
*	Add to Oshrximm proof	Yann Herklotz	2020-11-03	1	-55/+109
\|
*	Add intextra	Yann Herklotz	2020-11-03	1	-0/+115
\|
*	Add RTLPar	Yann Herklotz	2020-11-02	1	-0/+98
\|
*	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
\|