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

	Commit message (Collapse)	Author	Age	Files	Lines
*	Find called module in Icall proof	Michalis Pardalos	2021-08-19	1	-7/+1
\|
*	Complete HTLspec (mostly)	Michalis Pardalos	2021-08-12	1	-34/+64
\|
*	Tie clocks in the ApplyExternctrl pass	Michalis Pardalos	2021-08-12	1	-1/+0
\|
*	Correct lookup for called funcs, simplify tr_module	Michalis Pardalos	2021-08-04	1	-8/+24
\|
*	Check whether callee is internal for Icall	Michalis Pardalos	2021-08-02	1	-19/+24
\|
*	Add "join state is <=Int.max_unsigned" to HTLgenspec	Michalis Pardalos	2021-06-10	1	-9/+11
\|
*	Move HTL renaming pass to own file	Michalis Pardalos	2021-06-06	1	-240/+0
\|
*	Most of Ireturn proof	Michalis Pardalos	2021-05-16	1	-11/+17
\|
*	Prove a spec for the mapping of function params	Michalis Pardalos	2021-05-06	1	-5/+12
\| \| \| \| \|	Extracted the traversal of call args into a function and gave it a spec, so that it can be used to prove the overall spec for the Icall instruction.
*	Define map_incr to clarify st_incr	Michalis Pardalos	2021-05-05	1	-9/+13
\|
*	Rewrite transf_instr, move complicated part up	Michalis Pardalos	2021-05-03	1	-6/+6
\| \| \| \| \|	Mapping the externctrl for the parameters requires a traversal on a list. Moved it up to the top of the branch to make it stand out in the proof.
*	Add externctrl props to HTLgen's st_prop	Michalis Pardalos	2021-05-03	1	-41/+44
\|
*	Use ltac:() instead of Program in HTLgen	Michalis Pardalos	2021-05-03	1	-140/+116
\| \| \| \|	Program rewrites match statements, making proofs much harder.
*	Use Defined for obligations in Program Definitions	Michalis Pardalos	2021-05-02	1	-12/+12
\| \| \| \|	The created terms might need to be inspected.
*	Give a (questionable) translation spec for HTLgen	Michalis Pardalos	2021-05-02	1	-27/+37
\| \| \| \| \|	I am not yet convinced it is the right one, particularly around the way I've used existentials. I will be updating it as I progress with the proof.
*	Fix HTLgen using wrong register in call wait state	Michalis Pardalos	2021-05-01	1	-2/+3
\|
*	Tie all modules' clock to main	Michalis Pardalos	2021-04-30	1	-6/+6
\|
*	Fix map_externctrl double-incrementing freshreg	Michalis Pardalos	2021-04-30	1	-3/+2
\|
*	Delete unused get_main_clk function from HTLgen	Michalis Pardalos	2021-04-30	1	-11/+0
\|
*	Map clock correctly in RTL->HTL	Michalis Pardalos	2021-04-29	1	-15/+9
\| \| \| \|	Remove the renumber_clk param of the renumber state
*	Renumber AssocMaps in HTL modules too	Michalis Pardalos	2021-04-20	1	-7/+24
\|
*	Move renumbering to be HTL->HTL	Michalis Pardalos	2021-04-20	1	-0/+213
\|
*	[WIP] Re-implement translation of calls.	Michalis Pardalos	2021-04-19	1	-33/+67
\| \| \| \| \|	Add an explicit map of local HTL registers to control signals and params of other modules, used to implement calls.
*	[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	1	-17/+14
\|
*	Fix merge error in oshrximm	Michalis Pardalos	2021-04-09	1	-1/+3
\|
*	Add idle state after return	Michalis Pardalos	2021-03-01	1	-6/+7
\|
*	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 ↵	Yann Herklotz	2021-02-16	1	-2/+2
\| \| \| \|	michalis-merge
*	Fix imports to remove warnings when compiling	Yann Herklotz	2021-01-22	1	-9/+20
\|
*	Add correct copyright notices in files	Yann Herklotz	2021-01-10	1	-0/+1
\|
*	Change and add back HTLgen	Yann Herklotz	2020-11-09	1	-4/+4
\|
*	Add RTLBlock intermediate language	Yann Herklotz	2020-08-30	1	-0/+654