aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)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
* 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
* Separate HTL instantiations from Verilog onesMichalis Pardalos2020-11-207-21/+30
* 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
* 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
* | 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