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

	Commit message (Expand)	Author	Age	Files	Lines
*	Renumber AssocMaps in HTL modules too	Michalis Pardalos	2021-04-20	2	-7/+25
*	Move renumbering to be HTL->HTL	Michalis Pardalos	2021-04-20	3	-234/+229
*	Get HTLgenproof to compile	Michalis Pardalos	2021-04-20	2	-279/+280
*	Update HTLPargen for new HTL	Michalis Pardalos	2021-04-20	1	-30/+25
*	Update ocaml code match HTL changes	Michalis Pardalos	2021-04-20	1	-25/+2
*	[WIP] Re-implement translation of calls.	Michalis Pardalos	2021-04-19	2	-33/+84
*	[WIP] Use Program instead of state_incr lemmas	Michalis Pardalos	2021-04-18	1	-165/+40
*	[WIP] Generate calling verilog in RTL->HTL	Michalis Pardalos	2021-04-18	1	-15/+40
*	[WIP] Remove extra statements from HTL.	Michalis Pardalos	2021-04-18	2	-73/+18
*	[WIP] HTLgenspec proof	Michalis Pardalos	2021-04-17	1	-46/+34
*	Fix up rest of HTLgenproof	Michalis Pardalos	2021-04-09	1	-62/+46
*	Fix merge error in oshrximm	Michalis Pardalos	2021-04-09	1	-1/+3
*	Get HTLgenproof to compile	Michalis Pardalos	2021-04-08	1	-87/+89
*	[WIP] Add semantics for new HTL instructions	Michalis Pardalos	2021-04-02	1	-38/+72
*	Merge remote-tracking branch 'upstream/master' into dev-michalis	Michalis Pardalos	2021-03-29	5	-260/+533
\|\
\| *	Fix printing of the final cycle count	Yann Herklotz	2021-02-21	1	-2/+15
\| *	Fix bug in schedule	Yann Herklotz	2021-02-19	1	-2/+1
\| *	Fix schedule for now	Yann Herklotz	2021-02-18	1	-1/+2
\| *	Add udiv and sdiv to constraints	Yann Herklotz	2021-02-17	1	-12/+20
\| *	Remove dead code and add more constraints	Yann Herklotz	2021-02-17	1	-107/+16
\| *	Add option to turn off if-conversion	Yann Herklotz	2021-02-16	1	-2/+2
\| *	Merge branch 'master' into develop	Yann Herklotz	2021-02-16	2	-0/+621
\| \|\
\| * \|	Use topological sort for now	Yann Herklotz	2021-02-16	1	-4/+9
\| * \|	Add schedule for new RTLPar type	Yann Herklotz	2021-02-16	1	-29/+42
\| * \|	Fix RTLPar to use instr list list list	Yann Herklotz	2021-02-16	3	-25/+33
\| * \|	Replace original gather function with new constraints	Yann Herklotz	2021-02-15	1	-15/+16
\| * \|	Add resource constraints	Yann Herklotz	2021-02-15	1	-6/+71
\| * \|	Add information about pipeline and comb_delay	Yann Herklotz	2021-02-15	1	-8/+41
\| * \|	Add data and control dependencies to reworked graph	Yann Herklotz	2021-02-15	1	-43/+236
\| * \|	Make the schedule a bit neater	Yann Herklotz	2021-02-15	1	-74/+63
\| * \|	Use proper graph for DFG	Yann Herklotz	2021-02-15	1	-77/+113
* \| \|	Add idle state after return	Michalis Pardalos	2021-03-01	2	-33/+37
* \| \|	Typos in Veriloggen	Michalis Pardalos	2021-03-01	1	-2/+2
* \| \|	Unset finish signal on reset	Michalis Pardalos	2021-02-28	1	-1/+3
* \| \|	Merge branch 'master' into michalis-merge	Yann Herklotz	2021-02-16	2	-0/+621
\|\ \ \ \| \| \|/ \| \|/\|
\| * \|	Add functional units and Sat	Yann Herklotz	2021-02-16	2	-0/+621
\| \|/
* \|	Make top-level theorems pass	Yann Herklotz	2021-02-16	2	-44/+49
* \|	Add changes to HTL as they weren't merged	Yann Herklotz	2021-02-16	1	-53/+122
* \|	Merge branch 'michalis' of https://github.com/mpardalos/vericert into michali...	Yann Herklotz	2021-02-16	10	-170/+688
\|/
*	Add more legible names to variables	Yann Herklotz	2021-02-12	1	-1/+17
*	Add temporary fixes to get everything to compile	Yann Herklotz	2021-02-12	6	-36/+385
*	Fix state generation for if-conversion	Yann Herklotz	2021-02-03	4	-14/+21
*	Fix scheduling for if-conversion	Yann Herklotz	2021-02-03	1	-14/+90
*	Add predicated values and instructions	Yann Herklotz	2021-02-02	6	-39/+87
*	Add if conversion pass	Yann Herklotz	2021-02-02	1	-3/+65
*	Add if conversion pass	Yann Herklotz	2021-02-02	1	-0/+32
*	Add Vrange and predicates	Yann Herklotz	2021-02-02	7	-64/+95
*	Fix OCaml files for compilation	Yann Herklotz	2021-01-31	4	-92/+94
*	Fix compilation of Coq	Yann Herklotz	2021-01-30	1	-18/+45
*	Fix proofs with better defined equality	Yann Herklotz	2021-01-30	2	-31/+57