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

	Commit message (Collapse)	Author	Age	Files	Lines
*	Remove RTLParFu and fix DMemorygen.v	Yann Herklotz	2023-07-31	1	-52/+4
\|
*	Add beginning to memory generation proof	Yann Herklotz	2023-07-29	1	-1366/+1477
\|
*	Add if-conversion decision procedure	Yann Herklotz	2023-07-06	1	-6/+6
\|
*	Update to Coq 8.17 and CompCert 3.12	Yann Herklotz	2023-04-27	1	-1/+1
\|
*	Clean up proofs	Yann Herklotz	2022-10-11	1	-41/+41
\|
*	Remove literal files again	Yann Herklotz	2022-03-26	1	-18/+21
\|
*	Final updates to the current documentation	Yann Herklotz	2022-02-25	1	-6/+6
\|
*	Fix compilation with new HTL language	Yann Herklotz	2021-11-18	1	-7/+8
\|
*	Remove warnings of attributes	Yann Herklotz	2021-10-08	1	-23/+23
\|
*	Basically done with proof	Yann Herklotz	2021-04-07	1	-2/+2
\|
*	Add negative edge reasoning to HTLgenproof	Yann Herklotz	2021-03-09	1	-12/+76
\|
*	Add RAM semantics to HTL and fix proof	Yann Herklotz	2021-03-03	1	-6/+8
\|
*	Add implementation	Yann Herklotz	2021-03-02	1	-1/+1
\|
*	Add match_states for RTLPargen proof	Yann Herklotz	2021-01-22	1	-4/+18
\|
*	Add correct copyright notices in files	Yann Herklotz	2021-01-10	1	-0/+1
\|
*	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	1	-5/+5
\|
*	Change and add back HTLgen	Yann Herklotz	2020-11-09	1	-1/+24
\|
*	Add RTLBlock intermediate language	Yann Herklotz	2020-08-30	1	-0/+2683