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

	Commit message (Collapse)	Author	Age	Files	Lines
*	Complete HTLspec (mostly)	Michalis Pardalos	2021-08-12	1	-1/+3
\|
*	Remove all Admitted from top-level Compiler.v	Michalis Pardalos	2021-06-10	1	-7/+10
\|
*	Get entire HTLgenspec proof passing	Michalis Pardalos	2021-05-10	1	-0/+10
\|
*	Progress on tr_module proof	Michalis Pardalos	2021-05-08	1	-0/+2
\|
*	Fully clean up the iter_expand_instr_spec proof	Michalis Pardalos	2021-05-07	1	-0/+13
\|
*	Solve iter_expand_instr_spec by tactic (not Icall)	Michalis Pardalos	2021-05-05	1	-2/+3
\|
*	Add lemmas relating to new HTLgen operations	Michalis Pardalos	2021-05-03	1	-2/+2
\|
*	Add externctrl props to HTLgen's st_prop	Michalis Pardalos	2021-05-03	1	-0/+7
\|
*	Simplify some HTLgenspec proofs	Michalis Pardalos	2021-05-02	1	-0/+5
\|
*	Merge branch 'master' into michalis-merge	Yann Herklotz	2021-02-16	1	-1/+0
\|\
\| *	Remove dependency on Tactics	Yann Herklotz	2021-02-16	1	-1/+0
\| \|
* \|	Merge branch 'michalis' of https://github.com/mpardalos/vericert into ↵	Yann Herklotz	2021-02-16	1	-0/+9
\|\ \ \| \|/ \|/\| \| \|	michalis-merge
\| *	Inlined modules are valid verilog, use correct clk	Michalis Pardalos	2021-01-26	1	-0/+9
\| \|
* \|	Add destruction to context match expressions	Yann Herklotz	2021-01-26	1	-2/+5
\| \|
* \|	Fix imports in Coq modules	Yann Herklotz	2021-01-21	1	-13/+19
\|/
*	Rename to Vericertlib	Yann Herklotz	2020-07-17	1	-0/+237