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

	Commit message (Collapse)	Author	Age	Files	Lines
*	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
\|
*	Update AST and value representations	Yann Herklotz	2020-03-29	1	-213/+42
\|
*	Update nix files with bbv dependency	Yann Herklotz	2020-03-29	2	-7/+29
\|
*	Rename Verilog AST files	Yann Herklotz	2020-03-29	3	-0/+0
\|
*	Update printing	Yann Herklotz	2020-03-25	4	-38/+56
\|
*	Update dependencies	Yann Herklotz	2020-03-25	2	-16/+15
\|
*	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	-5/+4
\|
*	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
\|