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

	Commit message (Collapse)	Author	Age	Files	Lines
*	Add construction of state in sem	Yann Herklotz	2021-10-31	1	-23/+147
\|
*	Fix compilation issues with new types	Yann Herklotz	2021-10-30	4	-46/+37
\|
*	Make Abstr pass with admitted to check top-level	Yann Herklotz	2021-10-30	1	-45/+110
\|
*	Add a predicate to RBsetpred	Yann Herklotz	2021-10-30	3	-6/+6
\|
*	Remove admitted from subproof	Yann Herklotz	2021-10-29	1	-6/+57
\|
*	Add intermediate step in proof of sem pres	Yann Herklotz	2021-10-27	2	-24/+108
\|
*	Work more on equivalence of SAT	Yann Herklotz	2021-10-26	3	-34/+137
\|
*	Continue on semantics preservation proof	Yann Herklotz	2021-10-24	1	-198/+178
\|
*	Fix if-conversion and translation with Plit	Yann Herklotz	2021-10-24	2	-5/+5
\|
*	Add type-class proofs to Predicate.v	Yann Herklotz	2021-10-24	2	-12/+217
\|
*	Add setoid typeclass	Yann Herklotz	2021-10-21	1	-15/+21
\|
*	Add work towards decidability of SAT solver	Yann Herklotz	2021-10-21	7	-279/+377
\|
*	Start to prove termination of SAT	Yann Herklotz	2021-10-20	3	-244/+266
\|
*	Continuations on proof of predicates	Yann Herklotz	2021-10-19	2	-127/+151
\|
*	[sched] Fix passes with new predicates	Yann Herklotz	2021-10-14	2	-1/+3
\|
*	[sched] Add combination of equivalent expressions	Yann Herklotz	2021-10-14	1	-10/+40
\|
*	[sched] Add true and false predicates to type	Yann Herklotz	2021-10-14	1	-1/+23
\|
*	[sched] Finish det proofs of basic Abstr semantics	Yann Herklotz	2021-10-13	1	-27/+44
\|
*	[sched] Add more proof to sem_pred_det	Yann Herklotz	2021-10-13	2	-1/+6
\|
*	[sched] Add proofs of sem_pred_det	Yann Herklotz	2021-10-13	1	-8/+44
\|
*	[sched] Add start to proof of sem_value_det	Yann Herklotz	2021-10-12	1	-0/+12
\|
*	[sched] Remove unnecessary imports	Yann Herklotz	2021-10-12	1	-11/+0
\|
*	[sched] Add more lemmas into HashTree	Yann Herklotz	2021-10-12	2	-10/+37
\|
*	[sched] Update Abstr.v to use HashTree	Yann Herklotz	2021-10-12	1	-29/+97
\|
*	[sched] Add HashTree.v for hashing arbitrary values	Yann Herklotz	2021-10-12	1	-0/+413
\|
*	Add div benchmarks to .gitignore	Yann Herklotz	2021-10-12	1	-0/+28
\|
*	Update .gitignore again	Yann Herklotz	2021-10-12	1	-27/+27
\|
*	Add updated .gitignore for benchmarks	Yann Herklotz	2021-10-12	1	-0/+40
\|
*	Merge branch 'dev/scheduling' of git.ymhg.org:vericert into dev/scheduling	Yann Herklotz	2021-10-12	12	-76/+94
\|\
\| *	Fix some of the testing in Makefile	Yann Herklotz	2021-10-09	1	-3/+3
\| \|
\| *	Update the changelog	Yann Herklotz	2021-10-09	1	-3/+7
\| \|
\| *	Fix warnings for Coq 8.13.2	Yann Herklotz	2021-10-09	10	-70/+84
\| \|
* \|	[sched] Small changes to definitions	Yann Herklotz	2021-10-12	1	-5/+5
\|/
*	End section in Abstr.v	Yann Herklotz	2021-10-08	1	-0/+2
\|
*	Add abstract intermediate language to RTLPargen	Yann Herklotz	2021-10-08	1	-17/+49
\|
*	Remove warnings of attributes	Yann Herklotz	2021-10-08	3	-126/+126
\|
*	Make HTLgenproof pass	Yann Herklotz	2021-10-08	1	-1/+1
\|
*	Add proof of beq_check_correctness	Yann Herklotz	2021-10-08	1	-57/+120
\|
*	Fix running of tests using a Makefile	Yann Herklotz	2021-10-08	2	-1/+36
\|
*	Add scheduling by default to benchmark execution	Yann Herklotz	2021-10-07	1	-1/+1
\|
*	Fix naming and remove warnings	Yann Herklotz	2021-10-07	2	-10/+10
\|
*	RTLPargen now uses Abstr as symbolic execution target	Yann Herklotz	2021-10-07	1	-705/+1
\|
*	Update functional units to be more general	Yann Herklotz	2021-10-07	1	-14/+62
\|
*	Add Abstr intermediate language	Yann Herklotz	2021-10-07	1	-0/+749
\|
*	[test] Fix testing from Makefile	Yann Herklotz	2021-10-01	1	-0/+2
\|
*	[scheduling] Fix connected components of DFG	Yann Herklotz	2021-10-01	1	-6/+7
\|
*	Merge branch 'master' into dev/scheduling	Yann Herklotz	2021-10-01	4	-13/+20
\|\
\| *	Add menhirLib as an explicit dependency	Yann Herklotz	2021-10-01	1	-0/+1
\| \|
\| *	Update README with checkout instructions	Yann Herklotz	2021-10-01	1	-10/+12
\| \|
\| *	Merge branch 'release/v1.2.2'	Yann Herklotz	2021-10-01	3	-3/+7
\| \|\