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

	Commit message (Collapse)	Author	Age	Files	Lines
*	Fix imports in Coq modules	Yann Herklotz	2021-01-21	3	-47/+94
\|
*	Improve expression equality proof	Yann Herklotz	2021-01-21	1	-57/+17
\|
*	Translate from RTLBlock to RTLPar	Yann Herklotz	2021-01-13	1	-201/+39
\|
*	Correct translation of scheduling with oracle check	Yann Herklotz	2021-01-13	1	-4/+53
\|
*	Remove HTLSchedulegen	Yann Herklotz	2021-01-13	1	-42/+0
\|
*	Add RTLPargen.v	Yann Herklotz	2021-01-13	1	-0/+27
\|
*	Add HTLPargen translation	Yann Herklotz	2021-01-13	1	-50/+130
\|
*	Add conversion from RTLPar to HTL	Yann Herklotz	2021-01-12	1	-0/+633
\|
*	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	8	-0/+25
\|
*	Add extraction and loop pipelining stage	Yann Herklotz	2020-12-17	1	-0/+11
\|
*	Fix build for Coq 8.12.1	Yann Herklotz	2020-11-26	5	-17/+5
\|
*	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	1	-1/+1
\|
*	Comment out blockgen	Yann Herklotz	2020-11-04	1	-1/+2
\|
*	Quick compile fix	Yann Herklotz	2020-11-04	2	-2/+6
\|
*	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
\|
*	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	1	-10/+23
\|
*	Fix build error with ValueVal	Yann Herklotz	2020-10-26	1	-2/+8
\|
*	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	1	-1/+1
\|
*	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
\|
*	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
\|
*	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	2	-12/+63
\|
*	Add RTLBlock intermediate language	Yann Herklotz	2020-08-30	18	-0/+7253