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

	Commit message (Collapse)	Author	Age	Files	Lines
*	Add PTree traversal functions for vericert monads	Michalis Pardalos	2021-02-15	1	-1/+20
\|
*	Add an indexed filter function to PTree	Michalis Pardalos	2021-02-12	1	-0/+27
\|
*	Implemented fork and wait (incorrectly)	Michalis Pardalos	2021-02-12	1	-46/+70
\|
*	Reformat	Michalis Pardalos	2021-02-09	1	-5/+5
\|
*	Add wait instruction to HTL control path	Michalis Pardalos	2021-01-26	7	-76/+152
\|
*	Separate HTL call into fork and join	Michalis Pardalos	2021-01-26	5	-20/+62
\|
*	Inlined modules are valid verilog, use correct clk	Michalis Pardalos	2021-01-26	3	-16/+50
\|
*	Renumbering removes name conflicts	Michalis Pardalos	2021-01-25	1	-197/+226
\|
*	Implement renumbering (wrong)	Michalis Pardalos	2021-01-25	4	-51/+269
\|
*	Get everything compiling	Michalis Pardalos	2021-01-18	2	-2/+5
\|
*	Get top-level proofs passing.	Michalis Pardalos	2020-12-01	1	-28/+26
\| \| \| \|	Needed change because inlining was removed.
*	Get proofs in HTLgenproof to pass	Michalis Pardalos	2020-12-01	1	-11/+6
\|
*	Update proofs in HTLgenspec	Michalis Pardalos	2020-12-01	1	-4/+17
\|
*	Declare dst reg for call instr	Michalis Pardalos	2020-12-01	1	-0/+1
\|
*	Add a call instruction to HTL. Use it for Icall.	Michalis Pardalos	2020-11-30	8	-97/+190
\|
*	Revert changes relating to instance generation	Michalis Pardalos	2020-11-27	8	-205/+60
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Revert "Add todo for missing logic around instantiations" This reverts commit 303a45374643f75698c61f062899973d2c297831. Revert "Add wires and use them for output of instances" This reverts commit a72f26319dabca414a2b576424b9f72afaca161c. Revert "Separate HTL instantiations from Verilog ones" This reverts commit 653c8729f4322f538aa7116c5e311c884b3c5047. Revert "Translate instantiations from HTL to verilog" This reverts commit 982e6c69a52e8ec4e677147004cc5472f8a80d6d. Revert "Print instantiations in HTL output" This reverts commit 9b87637d3e4d6a75dee1221b017e3ccf6632642e. Revert "Add a field in HTL modules for instances" This reverts commit d79dae026b150e9671e0aa7262f6aa2d1d302502. Revert "Generate (invalid) module instantiations for calls" This reverts commit dfaa3a9cbc07649feea3220693a8a854a32eafb6.
*	Add todo for missing logic around instantiations	Michalis Pardalos	2020-11-20	1	-0/+1
\|
*	Add wires and use them for output of instances	Michalis Pardalos	2020-11-20	5	-23/+55
\| \| \| \| \| \| \| \|	[WIP] Add wires to HTL [WIP] Add wires to verilog [WIP] Use wire for finished signal [WIP] merge wire and scl [WIP] Fix wrong reg in ICall translation
*	Separate HTL instantiations from Verilog ones	Michalis Pardalos	2020-11-20	7	-21/+30
\| \| \| \| \| \| \| \| \| \| \|	In HTL, they reference their data arguments, destination, and finished control signal. Meanwhile, in Verilog, they just contain an unstructured list of parameters. This is done because when modules are generated in the HTL stage we do not have access to any of the instantiating module's control signals (they are declared after the entirety of the module has been translated). Also, I believe, these signals are not part of the HTL semantics.
*	Print HTL args as reg_{n}, not x{n}	Michalis Pardalos	2020-11-20	1	-7/+7
\|
*	Translate instantiations from HTL to verilog	Michalis Pardalos	2020-11-20	3	-2/+7
\|
*	Print instantiations in HTL output	Michalis Pardalos	2020-11-20	3	-14/+29
\|
*	Add a field in HTL modules for instances	Michalis Pardalos	2020-11-20	5	-37/+102
\|
*	Print all modules in verilog output	Michalis Pardalos	2020-11-20	1	-13/+11
\|
*	Generate (invalid) module instantiations for calls	Michalis Pardalos	2020-11-20	5	-14/+29
\|
*	Add html generation and clean Coq files	Yann Herklotz	2020-08-13	4	-7/+3
\|
*	Finished all the proofsv1.0.0	Yann Herklotz	2020-08-13	3	-39/+46
\| \| \| \|	Removed support for case statements temporarily.
*	Remove unnecessary commented proof	Yann Herklotz	2020-08-12	1	-23/+0
\|
*	Finish proof of conditionals	Yann Herklotz	2020-08-12	1	-4/+11
\|
*	Nearly finished all proofs	Yann Herklotz	2020-08-12	1	-48/+228
\|
*	Remove alignment constraint during translation.	James Pollard	2020-08-11	2	-67/+69
\| \| \| \|	This is now inferred from the memory model.
*	Remove last admits from istore	Yann Herklotz	2020-08-04	1	-2/+3
\|
*	Finish istore and iload without any admits	Yann Herklotz	2020-08-04	2	-119/+115
\|
*	No admitted in iload proof	Yann Herklotz	2020-08-04	1	-38/+72
\|
*	Merge remote-tracking branch 'james/develop' into develop	Yann Herklotz	2020-08-04	1	-5/+6
\|\
\| *	Fix broken proof.	James Pollard	2020-08-04	1	-5/+6
\| \|
* \|	Add expr_ok proof	Yann Herklotz	2020-08-04	1	-11/+25
\|/
*	Fix first part of istore	Yann Herklotz	2020-08-04	1	-40/+43
\|
*	Fix iload proof	Yann Herklotz	2020-08-04	2	-43/+52
\|
*	Add proof of divisibility	Yann Herklotz	2020-08-04	1	-21/+14
\|
*	Remove check mpass	Yann Herklotz	2020-07-24	1	-2/+0
\|
*	More renames to get it to compile	Yann Herklotz	2020-07-24	4	-6/+9
\|
*	Rename to Vericertlib	Yann Herklotz	2020-07-17	1	-0/+0
\|
*	Change name to Vericert	Yann Herklotz	2020-07-14	23	-53/+52
\|
*	Fixes to operators	Yann Herklotz	2020-07-07	4	-6/+12
\|
*	Finished transl_cond	Yann Herklotz	2020-07-07	2	-62/+45
\|
*	Only translate_cond left	Yann Herklotz	2020-07-07	4	-17/+252
\|
*	No admitted in Deterministic proof	Yann Herklotz	2020-07-07	3	-14/+10
\|
*	A few operations left	Yann Herklotz	2020-07-07	1	-30/+88
\|
*	Proof of TransfHTLLink DONE	Yann Herklotz	2020-07-07	1	-1/+14
\|