| Commit message (Collapse) | Author | Age | Files | Lines | |
|---|---|---|---|---|---|
| * | Put memorygen after renaming/applyexternctrl | Michalis Pardalos | 2021-09-02 | 1 | -13/+14 |
| | | |||||
| * | Get top-level proof passing | Michalis Pardalos | 2021-09-01 | 1 | -12/+14 |
| | | |||||
| * | Merge branch 'oopsla21' into sharing-merge | Michalis Pardalos | 2021-08-26 | 1 | -7/+15 |
| |\ | |||||
| | * | Remove unnecessary files and proofs | Yann Herklotz | 2021-07-11 | 1 | -2/+2 |
| | | | |||||
| | * | Add docker file and some comments | Yann Herklotz | 2021-07-09 | 1 | -0/+2 |
| | | | |||||
| | * | Remove Admitted in the highest of top-levelsv1.2.0 | Yann Herklotz | 2021-04-07 | 1 | -5/+10 |
| | | | |||||
| | * | Add option to turn on/off ram inferrence | Yann Herklotz | 2021-03-02 | 1 | -2/+4 |
| | | | |||||
| * | | Remove all Admitted from top-level Compiler.v | Michalis Pardalos | 2021-06-10 | 1 | -35/+20 |
| | | | |||||
| * | | Get top-level (Compiler) proof closer to Qed | Michalis Pardalos | 2021-06-08 | 1 | -3/+27 |
| | | | | | | | | | Add Renaming and ApplyExternctrl to correctness statement | ||||
| * | | Make externctrl application its own HTL pass | Michalis Pardalos | 2021-06-06 | 1 | -1/+4 |
| | | | |||||
| * | | Move HTL renaming pass to own file | Michalis Pardalos | 2021-06-06 | 1 | -1/+2 |
| | | | |||||
| * | | Move renumbering to be HTL->HTL | Michalis Pardalos | 2021-04-20 | 1 | -3/+5 |
| | | | |||||
| * | | Merge remote-tracking branch 'upstream/master' into dev-michalis | Michalis Pardalos | 2021-03-29 | 1 | -1/+2 |
| |\| | |||||
| | * | Add option to turn off if-conversion | Yann Herklotz | 2021-02-16 | 1 | -1/+2 |
| | | | |||||
| * | | Make top-level theorems pass | Yann Herklotz | 2021-02-16 | 1 | -4/+4 |
| | | | |||||
| * | | Merge branch 'michalis' of https://github.com/mpardalos/vericert into ↵ | Yann Herklotz | 2021-02-16 | 1 | -9/+10 |
| |\ \ | |/ |/| | | | michalis-merge | ||||
| | * | Implement renumbering (wrong) | Michalis Pardalos | 2021-01-25 | 1 | -8/+12 |
| | | | |||||
| | * | Get top-level proofs passing. | Michalis Pardalos | 2020-12-01 | 1 | -28/+26 |
| | | | | | | | | | Needed change because inlining was removed. | ||||
| | * | Add a call instruction to HTL. Use it for Icall. | Michalis Pardalos | 2020-11-30 | 1 | -28/+28 |
| | | | |||||
| | * | Revert changes relating to instance generation | Michalis Pardalos | 2020-11-27 | 1 | -2/+3 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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. | ||||
| | * | Generate (invalid) module instantiations for calls | Michalis Pardalos | 2020-11-20 | 1 | -3/+2 |
| | | | |||||
| * | | Add predicated values and instructions | Yann Herklotz | 2021-02-02 | 1 | -2/+5 |
| | | | |||||
| * | | Add Vrange and predicates | Yann Herklotz | 2021-02-02 | 1 | -2/+0 |
| | | | |||||
| * | | Fix imports in Coq modules | Yann Herklotz | 2021-01-21 | 1 | -43/+33 |
| | | | |||||
| * | | Add missing modules to extraction and compile | Yann Herklotz | 2021-01-13 | 1 | -2/+4 |
| | | | |||||
| * | | Add extraction and loop pipelining stage | Yann Herklotz | 2020-12-17 | 1 | -1/+4 |
| | | | |||||
| * | | Update Compiler proof with all optimisations | Yann Herklotz | 2020-11-28 | 1 | -39/+72 |
| | | | |||||
| * | | Update documentation for Compiler.v | Yann Herklotz | 2020-11-26 | 1 | -0/+84 |
| | | | |||||
| * | | Add optimisations to output | Yann Herklotz | 2020-11-02 | 1 | -15/+73 |
| | | | |||||
| * | | Add printing of intermediate rtlblock language | Yann Herklotz | 2020-10-23 | 1 | -1/+5 |
| | | | |||||
| * | | Finish implementing scheduling and add top level export | Yann Herklotz | 2020-10-20 | 1 | -3/+7 |
| | | | |||||
| * | | Add renumbering to compiler passes | Yann Herklotz | 2020-10-18 | 1 | -0/+1 |
| | | | |||||
| * | | Add fixes to run scheduling on compilation | Yann Herklotz | 2020-09-03 | 1 | -1/+14 |
| |/ | |||||
| * | Remove check mpass | Yann Herklotz | 2020-07-24 | 1 | -2/+0 |
| | | |||||
| * | Change name to Vericert | Yann Herklotz | 2020-07-14 | 1 | -3/+3 |
| | | |||||
| * | Fixes to operators | Yann Herklotz | 2020-07-07 | 1 | -0/+2 |
| | | |||||
| * | Rename asm to verilog | Yann Herklotz | 2020-07-06 | 1 | -9/+10 |
| | | |||||
| * | Add top level backward simulation | Yann Herklotz | 2020-07-06 | 1 | -15/+112 |
| | | |||||
| * | HTLgenproof compiles again | Yann Herklotz | 2020-07-06 | 1 | -1/+6 |
| | | | | | - Commented out Iload, Istore proofs for now | ||||
| * | Add htl pretty printing | Yann Herklotz | 2020-06-30 | 1 | -0/+2 |
| | | |||||
| * | Fix top level invocation to translate through HTL | Yann Herklotz | 2020-06-12 | 1 | -3/+6 |
| | | |||||
| * | Add equality check for value | Yann Herklotz | 2020-05-04 | 1 | -1/+1 |
| | | |||||
| * | Extract simulator | Yann Herklotz | 2020-04-17 | 1 | -2/+2 |
| | | |||||
| * | Update compilation | Yann Herklotz | 2020-04-01 | 1 | -2/+2 |
| | | |||||
| * | Convert from RTL to Verilog directly | Yann Herklotz | 2020-03-31 | 1 | -3/+22 |
| | | |||||
| * | Move compiler | Yann Herklotz | 2020-03-29 | 1 | -0/+113 |
 |
index : vericert | |
| Vericert is a formally verified high-level synthesis tool. |
| aboutsummaryrefslogtreecommitdiffstats |