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

	Commit message (Collapse)	Author	Age	Files	Lines
*	Define RTLPar semantics	Yann Herklotz	2021-01-22	2	-172/+85
\| \| \| \| \| \|	These semantics are similar to the RTLBlock semantics, except that more states are needed to reason about the parallel execution in multiple cycles.
*	Add top-level semantics definitions	Yann Herklotz	2021-01-22	1	-0/+17
\|
*	Add semantics for RTLBlock	Yann Herklotz	2021-01-22	2	-12/+68
\|
*	Add semantics for RTLBlockInstr and RTLBlock	Yann Herklotz	2021-01-22	2	-22/+72
\|
*	Share code between RTLBlock and Par	Yann Herklotz	2021-01-21	4	-149/+314
\|
*	Fix imports in Coq modules	Yann Herklotz	2021-01-21	7	-116/+162
\|
*	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 missing modules to extraction and compile	Yann Herklotz	2021-01-13	2	-4/+5
\|
*	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	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
\|