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

	Commit message (Expand)	Author	Age	Files	Lines
...
*	Add long and bool support to value	Yann Herklotz	2020-10-06	1	-23/+79
*	Add fixes to run scheduling on compilation	Yann Herklotz	2020-09-03	2	-1/+15
*	Scheduling added to partitioning	Yann Herklotz	2020-09-03	1	-3/+2
*	Add scheduling	Yann Herklotz	2020-09-03	2	-0/+181
*	Fix bug for basic block construction in loops	Yann Herklotz	2020-08-31	1	-3/+7
*	Add working partitioning algorithm	Yann Herklotz	2020-08-31	4	-42/+175
*	Continue on Partitioning algorithm	Yann Herklotz	2020-08-30	3	-14/+66
*	Add RTLBlock intermediate language	Yann Herklotz	2020-08-30	19	-3/+178
*	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
*	Rename asm to verilog	Yann Herklotz	2020-07-06	1	-9/+10
*	Add top level backward simulation	Yann Herklotz	2020-07-06	3	-95/+191
*	HTLgenproof compiles again	Yann Herklotz	2020-07-06	4	-22/+47
*	Fix Inop	Yann Herklotz	2020-07-05	4	-47/+58
*	Fix HTLgenspec	Yann Herklotz	2020-07-05	1	-3/+4
*	No addmitted in Veriloggenproof	Yann Herklotz	2020-07-05	4	-100/+245
*	Remove admitted in mis_stepp_Vdecl	Yann Herklotz	2020-07-05	3	-9/+12
*	Finish most of Veriloggenproof	Yann Herklotz	2020-07-05	5	-31/+205
*	Merge remote-tracking branch 'james/develop' into develop	Yann Herklotz	2020-07-04	2	-12/+175
\|\
\| *	Working on determinacy proof.	James Pollard	2020-07-04	2	-12/+175
* \|	Define ofbytes	Yann Herklotz	2020-07-04	1	-1/+72
* \|	Make HTLgen compile again	Yann Herklotz	2020-07-04	1	-3/+11
\|/
*	Fixing HTLgenproof	Yann Herklotz	2020-07-03	6	-41/+67
*	Add new value type to fix Iop proof	Yann Herklotz	2020-07-03	5	-67/+217
*	Addition to int_add_v2	Yann Herklotz	2020-07-03	1	-3/+13
*	Updates to Iop proof	Yann Herklotz	2020-07-03	3	-92/+179
*	Switch to uvalueToZ in lessdef.	James Pollard	2020-07-02	4	-67/+87