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

	Commit message (Collapse)	Author	Age	Files	Lines
*	Merge branch 'oopsla21' into sharing-merge	Michalis Pardalos	2021-08-26	1	-12/+34
\|\
\| *	Remove unnecessary files and proofs	Yann Herklotz	2021-07-11	1	-2/+3
\| \|
\| *	Add legup script	Yann Herklotz	2021-07-11	1	-1/+1
\| \|
\| *	Basically done with proof	Yann Herklotz	2021-04-07	1	-4/+6
\| \|
\| *	Finish load and store proof, but broke top-level	Yann Herklotz	2021-04-06	1	-6/+23
\| \|
\| *	Add RAM to HTL	Yann Herklotz	2021-03-02	1	-0/+1
\| \|
\| *	Change lists in case statements to stmnt_list	Yann Herklotz	2021-03-01	1	-1/+1
\| \|
* \|	Update HTLPargen for new HTL	Michalis Pardalos	2021-04-20	1	-30/+25
\| \|
* \|	Merge remote-tracking branch 'upstream/master' into dev-michalis	Michalis Pardalos	2021-03-29	1	-15/+18
\|\\|
\| *	Fix RTLPar to use instr list list list	Yann Herklotz	2021-02-16	1	-15/+18
\| \|
* \|	Make top-level theorems pass	Yann Herklotz	2021-02-16	1	-39/+42
\|/
*	Add temporary fixes to get everything to compile	Yann Herklotz	2021-02-12	1	-12/+75
\|
*	Fix state generation for if-conversion	Yann Herklotz	2021-02-03	1	-4/+5
\|
*	Add predicated values and instructions	Yann Herklotz	2021-02-02	1	-14/+34
\|
*	Add Vrange and predicates	Yann Herklotz	2021-02-02	1	-14/+31
\|
*	Fix HTLPargen and RTLPargen	Yann Herklotz	2021-01-29	1	-5/+5
\|
*	Fix types with new changes in RTLBlock	Yann Herklotz	2021-01-22	1	-58/+89
\| \| \| \| \|	Also formatted some files so that they are under 80 columns, which is much nicer to read.
*	Fix imports in Coq modules	Yann Herklotz	2021-01-21	1	-5/+15
\|
*	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