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

	Commit message (Collapse)	Author	Age	Files	Lines
*	Make HTLgenproof pass	Yann Herklotz	2021-10-08	1	-1/+1
\|
*	Fix naming and remove warnings	Yann Herklotz	2021-10-07	1	-7/+7
\|
*	Compile HTLPargen again	Yann Herklotz	2021-09-24	1	-4/+3
\|
*	Merge branch 'master' into develop	Yann Herklotz	2021-09-18	1	-3/+4
\|\
\| *	Remove unnecessary files and proofs	Yann Herklotz	2021-07-11	1	-2/+3
\| \|
\| *	Add legup script	Yann Herklotz	2021-07-11	1	-1/+1
\| \|
* \|	Change naturals to positive in predicates	Yann Herklotz	2021-05-26	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
\|
*	Fix RTLPar to use instr list list list	Yann Herklotz	2021-02-16	1	-15/+18
\|
*	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