aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Change Verilog to use internal CompCert Valdev/valueYann Herklotz2020-10-191-87/+78
|
* Add top level functions to scheduleYann Herklotz2020-10-191-49/+115
|
* Revert ValueInt.vYann Herklotz2020-10-181-79/+23
|
* Add output to schedulingYann Herklotz2020-10-181-25/+282
|
* Add renumbering to compiler passesYann Herklotz2020-10-181-0/+1
|
* Add scheduling to driverYann Herklotz2020-10-181-2/+2
|
* More changes to HTLBlockgenYann Herklotz2020-10-151-2/+2
|
* Add HTLBlockgen and more schedulingYann Herklotz2020-10-159-45/+1041
|
* Update CompCert dependencyYann Herklotz2020-10-061-0/+0
|
* Add long and bool support to valueYann Herklotz2020-10-061-23/+79
|
* Fix Makefile for verilog backendYann Herklotz2020-10-034-6/+6
|
* Fix compilationYann Herklotz2020-09-283-10/+11
|
* Add fixes to run scheduling on compilationYann Herklotz2020-09-033-3/+17
|
* Scheduling added to partitioningYann Herklotz2020-09-031-3/+2
|
* Add schedulingYann Herklotz2020-09-032-0/+181
|
* Fix bug for basic block construction in loopsYann Herklotz2020-08-311-3/+7
|
* Add working partitioning algorithmYann Herklotz2020-08-314-42/+175
|
* Continue on Partitioning algorithmYann Herklotz2020-08-303-14/+66
|
* Add RTLBlock intermediate languageYann Herklotz2020-08-3023-10/+187
|
* 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
|\
generated by cgit (git 2.34.1) at 2024-06-26 15:45:00 +0000