vericert-kvx - Unnamed repository; edit this file 'description' to name the repository.

	Commit message (Collapse)	Author	Age	Files	Lines
*	Return the actual result of the module	Yann Herklotz	2020-04-22	1	-2/+5
\|
*	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
\|
*	Only generate clocked always blocks	Yann Herklotz	2020-04-17	1	-13/+13
\|
*	Extract simulator	Yann Herklotz	2020-04-17	2	-5/+5
\|
*	Add Simulator.v	Yann Herklotz	2020-04-17	1	-0/+32
\|
*	Add do notation for option	Yann Herklotz	2020-04-15	1	-0/+11
\|
*	Make proofs simpler using auto	Yann Herklotz	2020-04-15	1	-59/+45
\| \| \| \| \|	This makes changes to theorems easier, as the proofs will likely not have to be fixed. The runtime is also not much slower.
*	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
\|
*	Add proof about state wf	Yann Herklotz	2020-04-08	1	-40/+193
\|
*	Add partial proof of well formed state	Yann Herklotz	2020-04-06	1	-24/+136
\|
*	Fix extraction on linux	Yann Herklotz	2020-04-02	1	-1/+1
\|
*	Handle loops and conditionals correctly	Yann Herklotz	2020-04-02	3	-112/+181
\|
*	Complete translation from simple RTL to Verilog	Yann Herklotz	2020-04-01	1	-101/+162
\|
*	Update compilation	Yann Herklotz	2020-04-01	5	-17/+84
\|
*	Convert from RTL to Verilog directly	Yann Herklotz	2020-03-31	3	-21/+45
\|
*	Add documentation and fix makefile for Compcert	Yann Herklotz	2020-03-31	5	-76/+101
\|
*	Add more operators and print them	Yann Herklotz	2020-03-31	3	-41/+84
\|
*	Use Compcert extraction	Yann Herklotz	2020-03-31	1	-2/+161
\|
*	Improve Verilog error messages	Yann Herklotz	2020-03-31	2	-2/+11
\|
*	Fix Verilog printing	Yann Herklotz	2020-03-31	2	-33/+35
\|
*	Add main file and global building	Yann Herklotz	2020-03-31	1	-6/+0
\|
*	Rename to transf_program	Yann Herklotz	2020-03-29	1	-1/+1
\|
*	Move compiler	Yann Herklotz	2020-03-29	1	-0/+113
\|
*	Complete conversion from HTL to Verilog	Yann Herklotz	2020-03-29	1	-8/+91
\|
*	Change Verilog AST back to more traditional AST	Yann Herklotz	2020-03-29	1	-30/+44
\|
*	Add Verilog generation from HTL	Yann Herklotz	2020-03-29	1	-0/+135
\|
*	Remove unnecessary examples from HTL	Yann Herklotz	2020-03-29	2	-10/+5
\|
*	Update AST and value representations	Yann Herklotz	2020-03-29	1	-213/+42
\|
*	Rename Verilog AST files	Yann Herklotz	2020-03-29	3	-0/+0
\|
*	Update printing	Yann Herklotz	2020-03-25	4	-38/+56
\|
*	Remove dunes and make the build recursive	Yann Herklotz	2020-03-25	4	-13/+5
\|
*	Create HTLgen	Yann Herklotz	2020-03-25	3	-148/+5
\|
*	Move driver	Yann Herklotz	2020-03-25	3	-126/+0
\|
*	Add Maps and HTL.v	Yann Herklotz	2020-03-25	2	-0/+235
\|
*	Rename to HTL	Yann Herklotz	2020-03-23	1	-18/+28
\|
*	Create intermediate VTL language	Yann Herklotz	2020-03-22	1	-0/+63
\|
*	Create a new direct translation	Yann Herklotz	2020-03-22	2	-14/+125
\|
*	Add compcert library to coquplib	Yann Herklotz	2020-03-22	2	-8/+13
\|
*	Convert Tactics to Coquplib: export common modules	Yann Herklotz	2020-03-20	1	-1/+8
\|
*	Lower case folders	Yann Herklotz	2020-03-19	13	-0/+0
\|
*	Update names of directories	Yann Herklotz	2020-03-19	3	-21/+40
\|
*	Update Verilog AST with flat array	Yann Herklotz	2020-02-18	2	-0/+7
\|
*	Create translation	Yann Herklotz	2020-02-18	1	-0/+18
\|
*	Update license to be compatible with CompCert	Yann Herklotz	2020-02-17	9	-16/+173
\|