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

	Commit message (Collapse)	Author	Age	Files	Lines
*	Remove literal files again	Yann Herklotz	2022-03-26	18	-232/+487
\|
*	Add more documentation	Yann Herklotz	2022-03-24	5	-149/+73
\|
*	Rename lit directory	Yann Herklotz	2022-03-24	6	-16/+18
\|
*	Change origin of tangled files	Yann Herklotz	2022-03-23	8	-21/+19
\|
*	Add back equalities	Yann Herklotz	2022-03-22	1	-2/+0
\|
*	Add first descriptions to org file	Yann Herklotz	2022-03-22	2	-45/+30
\|
*	Add literate Coq file	Yann Herklotz	2022-03-22	2	-7/+3
\|
*	Add comments to allow for literate detangling	Yann Herklotz	2022-03-22	7	-18/+362
\|
*	Add nops to partition generation	Yann Herklotz	2022-03-22	1	-4/+4
\|
*	Move forall_ptree into common	Yann Herklotz	2022-03-22	1	-42/+0
\|
*	Fix proofs in Sat.v	Yann Herklotz	2022-03-22	1	-1/+1
\|
*	Remove main binary	Yann Herklotz	2022-03-22	1	-0/+0
\|
*	Add RTLBlockgenproof	Yann Herklotz	2022-03-22	1	-0/+52
\|
*	Delete extra data files and scripts	Yann Herklotz	2022-03-22	1	-0/+0
\|
*	Update copyright notice	Yann Herklotz	2022-03-17	1	-1/+1
\|
*	Start work on reverse if-conversion	Yann Herklotz	2022-03-07	2	-1/+84
\|
*	Fix RAW dependency calculation for predicates	Yann Herklotz	2022-03-06	1	-0/+3
\|
*	Add back proof of beq2_correct	Yann Herklotz	2022-03-03	1	-23/+76
\|
*	Fix Abstr	Yann Herklotz	2022-03-03	1	-30/+17
\|
*	Update Coq version to 8.14.1	Yann Herklotz	2022-03-02	1	-37/+49
\|
*	Final updates to the current documentation	Yann Herklotz	2022-02-25	2	-9/+9
\|
*	Fix up some more documentation	Yann Herklotz	2022-02-25	7	-146/+68
\|
*	Start converting comments	Yann Herklotz	2022-02-25	2	-21/+7
\|
*	Add bourdoncle to build	Yann Herklotz	2021-12-09	4	-7/+40
\|
*	Add a printer for RTLParFU	Yann Herklotz	2021-11-18	1	-0/+120
\|
*	Fix operation chaining in scheduler	Yann Herklotz	2021-11-18	1	-8/+12
\| \| \| \|	It now respects the delays properly.
*	Remove unnecessary proof from RTLParFUgen	Yann Herklotz	2021-11-18	1	-1/+0
\|
*	Fix compilation with new HTL language	Yann Herklotz	2021-11-18	9	-149/+151
\|
*	Fix generation of RTLParFU	Yann Herklotz	2021-11-17	3	-46/+23
\|
*	Merge remote-tracking branch 'origin/dev/divider' into dev/scheduling	Yann Herklotz	2021-11-16	8	-69/+347
\|\
\| *	Get some Verilog output with dividersdev/divider	Yann Herklotz	2021-02-22	2	-11/+22
\| \|
\| *	Fix Scheduling to add missing states	Yann Herklotz	2021-02-22	1	-14/+34
\| \|
\| *	Fix arguments to RBassign and piped	Yann Herklotz	2021-02-22	4	-5/+10
\| \|
\| *	Add operation pipelining	Yann Herklotz	2021-02-22	1	-8/+133
\| \|
\| *	Add RTLPar printing	Yann Herklotz	2021-02-22	1	-0/+74
\| \|
\| *	Add operator pipelining pass	Yann Herklotz	2021-02-21	1	-0/+67
\| \|
\| *	Add new instructions for pipelines	Yann Herklotz	2021-02-21	9	-24/+33
\| \|
\| *	Correctly add initial scheduling variables	Yann Herklotz	2021-02-21	1	-4/+20
\| \|
\| *	Merge branch 'develop' into dev/divider	Yann Herklotz	2021-02-21	7	-260/+1154
\| \|\
\| * \|	Add beginning to scheduling division	Yann Herklotz	2021-02-15	7	-310/+181
\| \| \|
* \| \|	Finish generation of RTLParFU with RAM insertion	Yann Herklotz	2021-11-15	1	-24/+92
\| \| \|
* \| \|	Fix max funtion in RTLParFU	Yann Herklotz	2021-11-15	1	-1/+2
\| \| \|
* \| \|	Fix HTL generation from RTLParFU	Yann Herklotz	2021-11-15	1	-11/+34
\| \| \|
* \| \|	Use new RAM defined in FunctionalUnits.v	Yann Herklotz	2021-11-15	2	-2/+4
\| \| \|
* \| \|	Remove unnecessary RAM	Yann Herklotz	2021-11-15	1	-16/+1
\| \| \|
* \| \|	Add helper functions to FunctionalUnits	Yann Herklotz	2021-11-15	1	-3/+22
\| \| \|
* \| \|	Replace HTLPargen by HTLParFUgen	Yann Herklotz	2021-11-14	2	-896/+19
\| \| \|
* \| \|	Improve simplification of predicates	Yann Herklotz	2021-11-14	1	-2/+10
\| \| \|
* \| \|	Add proper functional unit generation	Yann Herklotz	2021-11-14	2	-23/+98
\| \| \|
* \| \|	Add helper functions to FunctionalUnits	Yann Herklotz	2021-11-14	1	-0/+74
\| \| \|