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

	Commit message (Expand)	Author	Age	Files	Lines
*	Add PTree traversal functions for vericert monads	Michalis Pardalos	2021-02-15	1	-1/+20
*	Add an indexed filter function to PTree	Michalis Pardalos	2021-02-12	1	-0/+27
*	Implemented fork and wait (incorrectly)	Michalis Pardalos	2021-02-12	1	-46/+70
*	Reformat	Michalis Pardalos	2021-02-09	1	-5/+5
*	Add wait instruction to HTL control path	Michalis Pardalos	2021-01-26	7	-76/+152
*	Separate HTL call into fork and join	Michalis Pardalos	2021-01-26	5	-20/+62
*	Inlined modules are valid verilog, use correct clk	Michalis Pardalos	2021-01-26	3	-16/+50
*	Renumbering removes name conflicts	Michalis Pardalos	2021-01-25	1	-197/+226
*	Implement renumbering (wrong)	Michalis Pardalos	2021-01-25	4	-51/+269
*	Get everything compiling	Michalis Pardalos	2021-01-18	2	-2/+5
*	Get top-level proofs passing.	Michalis Pardalos	2020-12-01	1	-28/+26
*	Get proofs in HTLgenproof to pass	Michalis Pardalos	2020-12-01	1	-11/+6
*	Update proofs in HTLgenspec	Michalis Pardalos	2020-12-01	1	-4/+17
*	Declare dst reg for call instr	Michalis Pardalos	2020-12-01	1	-0/+1
*	Add a call instruction to HTL. Use it for Icall.	Michalis Pardalos	2020-11-30	8	-97/+190
*	Revert changes relating to instance generation	Michalis Pardalos	2020-11-27	8	-205/+60
*	Add todo for missing logic around instantiations	Michalis Pardalos	2020-11-20	1	-0/+1
*	Add wires and use them for output of instances	Michalis Pardalos	2020-11-20	5	-23/+55
*	Separate HTL instantiations from Verilog ones	Michalis Pardalos	2020-11-20	7	-21/+30
*	Print HTL args as reg_{n}, not x{n}	Michalis Pardalos	2020-11-20	1	-7/+7
*	Translate instantiations from HTL to verilog	Michalis Pardalos	2020-11-20	3	-2/+7
*	Print instantiations in HTL output	Michalis Pardalos	2020-11-20	3	-14/+29
*	Add a field in HTL modules for instances	Michalis Pardalos	2020-11-20	5	-37/+102
*	Print all modules in verilog output	Michalis Pardalos	2020-11-20	1	-13/+11
*	Generate (invalid) module instantiations for calls	Michalis Pardalos	2020-11-20	5	-14/+29
*	Add html generation and clean Coq files	Yann Herklotz	2020-08-13	4	-7/+3
*	Finished all the proofsv1.0.0	Yann Herklotz	2020-08-13	3	-39/+46
*	Remove unnecessary commented proof	Yann Herklotz	2020-08-12	1	-23/+0
*	Finish proof of conditionals	Yann Herklotz	2020-08-12	1	-4/+11
*	Nearly finished all proofs	Yann Herklotz	2020-08-12	1	-48/+228
*	Remove alignment constraint during translation.	James Pollard	2020-08-11	2	-67/+69
*	Remove last admits from istore	Yann Herklotz	2020-08-04	1	-2/+3
*	Finish istore and iload without any admits	Yann Herklotz	2020-08-04	2	-119/+115
*	No admitted in iload proof	Yann Herklotz	2020-08-04	1	-38/+72
*	Merge remote-tracking branch 'james/develop' into develop	Yann Herklotz	2020-08-04	1	-5/+6
\|\
\| *	Fix broken proof.	James Pollard	2020-08-04	1	-5/+6
* \|	Add expr_ok proof	Yann Herklotz	2020-08-04	1	-11/+25
\|/
*	Fix first part of istore	Yann Herklotz	2020-08-04	1	-40/+43
*	Fix iload proof	Yann Herklotz	2020-08-04	2	-43/+52
*	Add proof of divisibility	Yann Herklotz	2020-08-04	1	-21/+14
*	Remove check mpass	Yann Herklotz	2020-07-24	1	-2/+0
*	More renames to get it to compile	Yann Herklotz	2020-07-24	4	-6/+9
*	Rename to Vericertlib	Yann Herklotz	2020-07-17	1	-0/+0
*	Change name to Vericert	Yann Herklotz	2020-07-14	23	-53/+52
*	Fixes to operators	Yann Herklotz	2020-07-07	4	-6/+12
*	Finished transl_cond	Yann Herklotz	2020-07-07	2	-62/+45
*	Only translate_cond left	Yann Herklotz	2020-07-07	4	-17/+252
*	No admitted in Deterministic proof	Yann Herklotz	2020-07-07	3	-14/+10
*	A few operations left	Yann Herklotz	2020-07-07	1	-30/+88
*	Proof of TransfHTLLink DONE	Yann Herklotz	2020-07-07	1	-1/+14