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

	Commit message (Collapse)	Author	Age	Files	Lines
*	Merge branch 'master' into develop	Yann Herklotz	2020-04-19	1	-0/+24
\|\
\| *	Add travis url	Yann Herklotz	2020-04-17	1	-1/+1
\| \|
\| *	Fix examples for current version of coqup	Yann Herklotz	2020-04-17	1	-3/+3
\| \|
\| *	Add information about downloading compcert	Yann Herklotz	2020-04-17	1	-0/+14
\| \|
\| *	Add examples on how to run HLS tool	Yann Herklotz	2020-04-17	1	-0/+10
\| \|
\| *	[#1 #2] Update README for installation	Yann Herklotz	2020-04-17	1	-8/+14
\| \|
* \|	Add travis url	Yann Herklotz	2020-04-17	1	-1/+1
\| \|
* \|	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
\| \|
* \|	Update driver to support simulator	Yann Herklotz	2020-04-17	1	-15/+60
\| \|
* \|	Add Simulator.v	Yann Herklotz	2020-04-17	2	-1/+33
\| \|
* \|	[#1 #2] Update README for installation	Yann Herklotz	2020-04-17	1	-8/+14
\| \|
* \|	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
\|
*	Update the readmev0.1.0	Yann Herklotz	2020-04-03	1	-1/+47
\|
*	Fix extraction on linux	Yann Herklotz	2020-04-02	1	-1/+1
\|
*	Add gcc to build dependencies	Yann Herklotz	2020-04-02	1	-1/+3
\|
*	Update compcert dependency	Yann Herklotz	2020-04-02	2	-0/+2
\|
*	Update readme	Yann Herklotz	2020-04-02	1	-1/+1
\|
*	Handle loops and conditionals correctly	Yann Herklotz	2020-04-02	4	-114/+183
\|
*	Update makefile for tests	Yann Herklotz	2020-04-02	1	-1/+4
\|
*	Add tests	Yann Herklotz	2020-04-02	4	-0/+68
\|
*	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
\|
*	Add necessary dependencies	Yann Herklotz	2020-04-01	1	-1/+1
\|
*	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	6	-77/+107
\|
*	Update .gitignore	Yann Herklotz	2020-03-31	1	-0/+4
\|
*	Add more operators and print them	Yann Herklotz	2020-03-31	3	-41/+84
\|
*	Fix the Makefile build	Yann Herklotz	2020-03-31	2	-6/+9
\|
*	Use Compcert extraction	Yann Herklotz	2020-03-31	1	-2/+161
\|
*	Fix Makefile build	Yann Herklotz	2020-03-31	2	-2/+6
\|
*	Improve Verilog error messages	Yann Herklotz	2020-03-31	2	-2/+11
\|
*	Fix Verilog printing	Yann Herklotz	2020-03-31	2	-33/+35
\|
*	Remove main driver	Yann Herklotz	2020-03-31	1	-19/+0
\|
*	Add main file and global building	Yann Herklotz	2020-03-31	4	-12/+450
\|
*	Rename to transf_program	Yann Herklotz	2020-03-29	1	-1/+1
\|
*	Move compiler	Yann Herklotz	2020-03-29	1	-2/+18
\|
*	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
\|
*	Update .gitignore	Yann Herklotz	2020-03-29	2	-1/+4
\|
*	Remove unnecessary examples from HTL	Yann Herklotz	2020-03-29	2	-10/+5
\|