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

	Commit message (Collapse)	Author	Age	Files	Lines
*	Change Inductive to record	Yann Herklotz	2021-09-22	1	-1/+1
\|
*	Add predicate semantics to RTLBlock	Yann Herklotz	2021-05-26	1	-7/+8
\|
*	Refactoring RTLBlock and RTLPar	Yann Herklotz	2021-01-29	1	-120/+29
\|
*	Use basic blocks in context to help proof	Yann Herklotz	2021-01-26	1	-11/+15
\|
*	Fix types with new changes in RTLBlock	Yann Herklotz	2021-01-22	1	-1/+2
\| \| \| \| \|	Also formatted some files so that they are under 80 columns, which is much nicer to read.
*	Define RTLPar semantics	Yann Herklotz	2021-01-22	1	-86/+0
\| \| \| \| \| \|	These semantics are similar to the RTLBlock semantics, except that more states are needed to reason about the parallel execution in multiple cycles.
*	Add top-level semantics definitions	Yann Herklotz	2021-01-22	1	-0/+17
\|
*	Add semantics for RTLBlock	Yann Herklotz	2021-01-22	1	-5/+67
\|
*	Add semantics for RTLBlockInstr and RTLBlock	Yann Herklotz	2021-01-22	1	-8/+51
\|
*	Share code between RTLBlock and Par	Yann Herklotz	2021-01-21	1	-40/+22
\|
*	Fix compilation issue	Yann Herklotz	2020-11-10	1	-3/+3
\|
*	Change and add back HTLgen	Yann Herklotz	2020-11-09	1	-2/+2
\|
*	Quick compile fix	Yann Herklotz	2020-11-04	1	-1/+4
\|
*	WIP on RTLBlock semantics	Yann Herklotz	2020-11-02	1	-12/+98
\|
*	Add working partitioning algorithm	Yann Herklotz	2020-08-31	1	-1/+3
\|
*	Continue on Partitioning algorithm	Yann Herklotz	2020-08-30	1	-3/+13
\|
*	Add RTLBlock intermediate language	Yann Herklotz	2020-08-30	1	-0/+69