aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Add an indexed filter function to PTreeMichalis Pardalos2021-02-121-0/+27
* Implemented fork and wait (incorrectly)Michalis Pardalos2021-02-121-46/+70
* ReformatMichalis Pardalos2021-02-091-5/+5
* Add wait instruction to HTL control pathMichalis Pardalos2021-01-267-76/+152
* Separate HTL call into fork and joinMichalis Pardalos2021-01-265-20/+62
* Inlined modules are valid verilog, use correct clkMichalis Pardalos2021-01-263-16/+50
* Renumbering removes name conflictsMichalis Pardalos2021-01-251-197/+226
* Implement renumbering (wrong)Michalis Pardalos2021-01-254-51/+269
* Get everything compilingMichalis Pardalos2021-01-182-2/+5
* Get top-level proofs passing.Michalis Pardalos2020-12-011-28/+26
* Get proofs in HTLgenproof to passMichalis Pardalos2020-12-011-11/+6
* Update proofs in HTLgenspecMichalis Pardalos2020-12-011-4/+17
* Declare dst reg for call instrMichalis Pardalos2020-12-011-0/+1
* 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