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

	Commit message (Collapse)	Author	Age	Files	Lines
*	Finished main proof with small assumptions	Yann Herklotz	2020-06-04	3	-25/+63
\|
*	Uncomment proof	Yann Herklotz	2020-06-03	1	-0/+5
\|
*	Add proof to final_states	Yann Herklotz	2020-06-02	1	-2/+2
\|
*	Add proof for equivalence of mov	Yann Herklotz	2020-06-02	1	-2/+33
\|
*	Copy over RTL global state	Yann Herklotz	2020-06-01	1	-8/+15
\|
*	Fix compilation moving to PTree	Yann Herklotz	2020-05-29	3	-11/+14
\|
*	Fix indentation	Yann Herklotz	2020-05-29	1	-6/+6
\|
*	New and improved Assocmap	Yann Herklotz	2020-05-29	1	-7/+32
\|
*	Change AssocMap to Maps.PTree	Yann Herklotz	2020-05-29	1	-47/+66
\|
*	Finish Assocmap proofs	Yann Herklotz	2020-05-28	1	-0/+59
\|
*	Add more proofs and remove Admitted	Yann Herklotz	2020-05-27	2	-16/+51
\|
*	Add HTLgen	Yann Herklotz	2020-05-24	1	-5/+4
\|
*	Finish the proof with most assumptions	Yann Herklotz	2020-05-21	1	-6/+11
\|
*	Fix the semantics to properly evaluate the state	Yann Herklotz	2020-05-20	1	-2/+4
\|
*	Switch position of empty rule	Yann Herklotz	2020-05-20	1	-4/+4
\|
*	Fix definitions in Value and add lemmas	Yann Herklotz	2020-05-20	1	-7/+35
\|
*	Add theorems about merge	Yann Herklotz	2020-05-20	1	-2/+12
\|
*	Add lessdef for values	Yann Herklotz	2020-05-08	1	-3/+10
\|
*	Add AssocMap	Yann Herklotz	2020-05-08	4	-47/+93
\|
*	Redefine HTL for intermediate Verilog language	Yann Herklotz	2020-05-07	1	-76/+69
\|
*	Use associations instead of state	Yann Herklotz	2020-05-07	2	-70/+69
\|
*	Rename assoclist to assocset	Yann Herklotz	2020-05-07	2	-28/+28
\|
*	Add changes to value	Yann Herklotz	2020-05-06	1	-2/+9
\|
*	Refine test file	Yann Herklotz	2020-05-05	1	-5/+2
\|
*	Minimised manual simulation	Yann Herklotz	2020-05-05	2	-45/+14
\|
*	Simplifications to proof	Yann Herklotz	2020-05-05	3	-18/+15
\|
*	Finish manual simulation	Yann Herklotz	2020-05-05	2	-5/+68
\|
*	Add equality check for value	Yann Herklotz	2020-05-04	2	-16/+22
\|
*	Refine the semantics	Yann Herklotz	2020-05-04	3	-56/+130
\|
*	Add code to debug execution of HLS	Yann Herklotz	2020-05-03	1	-0/+73
\|
*	Add hex notation to values	Yann Herklotz	2020-05-03	1	-0/+9
\|
*	Change to State	Yann Herklotz	2020-05-03	1	-21/+22
\|
*	Add CompCert semantics for Verilog	Yann Herklotz	2020-04-24	1	-81/+152
\|
*	Add valueToInt function	Yann Herklotz	2020-04-24	1	-0/+3
\|
*	Add stmnt_runp inductive	Yann Herklotz	2020-04-22	1	-27/+106
\|
*	Remove unnecessary Lemma	Yann Herklotz	2020-04-22	1	-8/+1
\| \| \| \| \|	Still cannot run these functions inside Coq itself, however, they work when they are extracted to Caml.
*	Use State in semantics instead of splitting it up	Yann Herklotz	2020-04-22	1	-95/+98
\|
*	Improve printing of results	Yann Herklotz	2020-04-22	2	-7/+13
\|
*	Fix Verilog.v	Yann Herklotz	2020-04-17	1	-1/+1
\|
*	Add main module run	Yann Herklotz	2020-04-17	2	-51/+79
\|
*	Fix printing with new Verilog AST	Yann Herklotz	2020-04-17	2	-26/+54
\|
*	Add Verilog semantics with new Verilog module	Yann Herklotz	2020-04-15	1	-33/+326
\|
*	Create Value module for bitvectors	Yann Herklotz	2020-04-15	1	-0/+217
\|
*	Handle loops and conditionals correctly	Yann Herklotz	2020-04-02	2	-12/+53
\|
*	Update compilation	Yann Herklotz	2020-04-01	3	-14/+81
\|
*	Add documentation and fix makefile for Compcert	Yann Herklotz	2020-03-31	2	-1/+26
\|
*	Add more operators and print them	Yann Herklotz	2020-03-31	2	-4/+15
\|
*	Improve Verilog error messages	Yann Herklotz	2020-03-31	1	-1/+4
\|
*	Fix Verilog printing	Yann Herklotz	2020-03-31	2	-33/+35
\|
*	Change Verilog AST back to more traditional AST	Yann Herklotz	2020-03-29	1	-30/+44
\|