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

	Commit message (Collapse)	Author	Age	Files	Lines
*	Extract some lemmas from the main proof	Yann Herklotz	2022-04-18	2	-24/+87
\|
*	Proof of the initial state matching	Yann Herklotz	2022-04-12	2	-3/+38
\|
*	Add intermediate files	Yann Herklotz	2022-04-08	4	-78/+143
\|
*	Work on the match_states definition	Yann Herklotz	2022-04-05	3	-17/+26
\|
*	Add basic blocks to the stackframe	Yann Herklotz	2022-04-05	5	-32/+54
\|
*	Add whole basic block into state	Yann Herklotz	2022-04-02	3	-73/+48
\|
*	Add list of bb to semantics	Yann Herklotz	2022-03-31	7	-96/+99
\|
*	Work on semantics for RTLBlockInstr	Yann Herklotz	2022-03-28	4	-22/+57
\|
*	Add specification for RTLBlockgenproof	Yann Herklotz	2022-03-28	2	-16/+53
\|
*	Work on specification of RTLBlock generation	Yann Herklotz	2022-03-28	3	-162/+108
\|
*	Add sphinx documentation	Yann Herklotz	2022-03-26	1	-26/+29
\|
*	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
\| \|\