aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Add a call instruction to HTL. Use it for Icall.Michalis Pardalos2020-11-308-97/+190
|
* Revert changes relating to instance generationMichalis Pardalos2020-11-278-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 instantiationsMichalis Pardalos2020-11-201-0/+1
|
* Add wires and use them for output of instancesMichalis Pardalos2020-11-205-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 onesMichalis Pardalos2020-11-207-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 Pardalos2020-11-201-7/+7
|
* Translate instantiations from HTL to verilogMichalis Pardalos2020-11-203-2/+7
|
* Print instantiations in HTL outputMichalis Pardalos2020-11-203-14/+29
|
* Add a field in HTL modules for instancesMichalis Pardalos2020-11-205-37/+102
|
* Print all modules in verilog outputMichalis Pardalos2020-11-201-13/+11
|
* Generate (invalid) module instantiations for callsMichalis Pardalos2020-11-205-14/+29
|
* Fix links in gh-pages sitev1.0.1Yann Herklotz2020-08-142-2/+16
|
* Update documentation with linksYann Herklotz2020-08-142-66/+71
|
* Add download of Coq documentationYann Herklotz2020-08-142-0/+13
|
* Remove on:Yann Herklotz2020-08-141-14/+0
|
* Update workflowYann Herklotz2020-08-143-10/+623
|
* Add modified polybench benchmarksYann Herklotz2020-08-1328-0/+3234
|
* Add html generation and clean Coq filesYann Herklotz2020-08-135-7/+8
|
* Finished all the proofsv1.0.0Yann Herklotz2020-08-133-39/+46
| | | | Removed support for case statements temporarily.
* Add statistics to be trackedYann Herklotz2020-08-131-3/+20
|
* Merge branch 'develop'Yann Herklotz2020-08-121-57/+221
|\
| * Remove unnecessary commented proofYann Herklotz2020-08-121-23/+0
| |
| * Finish proof of conditionalsYann Herklotz2020-08-121-4/+11
| |
| * Nearly finished all proofsYann Herklotz2020-08-121-48/+228
| |
* | Add documentation badge to READMEYann Herklotz2020-08-114-4/+4
|/
* Add benchmark changesYann Herklotz2020-08-119-1929/+3466
|
* Add content to documentationYann Herklotz2020-08-111-0/+79
|
* Fix admitted icon in READMEYann Herklotz2020-08-111-14/+4
|
* Fix yaml and generationYann Herklotz2020-08-112-4/+6
|
* Merge remote-tracking branch 'origin/master'Yann Herklotz2020-08-112-67/+69
|\
| * Remove alignment constraint during translation.James Pollard2020-08-112-67/+69
| | | | | | | | This is now inferred from the memory model.
* | Update website buildYann Herklotz2020-08-116-3/+1086
|/
* Update the link to the badgeYann Herklotz2020-08-101-1/+1
|
* Correctly pick colour for the badgeYann Herklotz2020-08-101-2/+10
|
* Add badge for admitted proofsYann Herklotz2020-08-101-0/+1
|
* Add gh-pagesYann Herklotz2020-08-102-3/+7
|
* Remove the nameYann Herklotz2020-08-101-1/+0
|
* Add badge for admitted proofsYann Herklotz2020-08-103-0/+69
|
* Remove last admits from istoreYann Herklotz2020-08-041-2/+3
|
* Finish istore and iload without any admitsYann Herklotz2020-08-042-119/+115
|
* No admitted in iload proofYann Herklotz2020-08-041-38/+72
|
* Merge remote-tracking branch 'james/develop' into developYann Herklotz2020-08-041-5/+6
|\
| * Fix broken proof.James Pollard2020-08-041-5/+6
| |
* | Add expr_ok proofYann Herklotz2020-08-041-11/+25
|/
* Fix first part of istoreYann Herklotz2020-08-041-40/+43
|
* Fix iload proofYann Herklotz2020-08-042-43/+52
|
* Add proof of divisibilityYann Herklotz2020-08-041-21/+14
|
* Add feature list to READMEYann Herklotz2020-07-241-0/+9
|
* Add more descriptions to READMEYann Herklotz2020-07-241-3/+3
|
* Remove check mpassYann Herklotz2020-07-241-2/+0
|
generated by cgit (git 2.34.1) at 2024-07-07 14:12:05 +0000