aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
...
| | * | [BROKEN] Some progress, need to figure out conversion HashedPSet -> ListCyril SIX2020-10-061-14/+111
| | | |
| | * | Detecting inner loops with LICMaux.inner_loopsCyril SIX2020-10-021-12/+75
| | | |
| | * | Rewriting some print to use a oc argumentCyril SIX2020-10-021-16/+11
| | | |
| | * | Moving some code from Duplicateaux to LICMaux to prevent cyclic depsCyril SIX2020-10-022-55/+63
| | | |
| * | | Updating builtins for Accesscore 4.2 (atomic stuff)Cyril SIX2020-10-141-1/+14
| | |/ | |/|
| * | centralize if_sameDavid Monniaux2020-10-093-12/+6
| | |
| * | do not synthesize select if both operands are identicalDavid Monniaux2020-10-092-7/+22
| | |
| * | update the title of our paperSylvain Boulmé2020-10-071-2/+2
| |/
* | simplify HSop (and merge hSop and hSop_Sinit)Sylvain Boulmé2020-10-172-42/+23
| |
* | update op_valid_pointer_eq proof on the KVXSylvain Boulmé2020-10-171-22/+4
| |
* | proves op_valid_pointer_eq lemma for RISC-V (necessary for the pre-pass ↵Sylvain Boulmé2020-10-172-0/+32
| | | | | | | | scheduler)
* | fixing the move of the verified prepass scheduler into scheduling/ directorySylvain Boulmé2020-10-174-762/+2
| |
* | Merge remote-tracking branch 'origin/kvx-test-prepass' into mppa-RTLpathSE-verifCyril SIX2020-10-1692-11356/+3357
|\ \
| * | pour ARMDavid Monniaux2020-10-021-4/+4
| | |
| * | fix need for kvx-elfDavid Monniaux2020-10-021-5/+1
| | |
| * | so that all architectures compileDavid Monniaux2020-10-027-8/+24
| | |
| * | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-027-19/+38
| |\|
| | * Duplicate no longer overwrites existing prediction informationCyril SIX2020-10-011-2/+9
| | |
| | * Updating test/kvx for KVX toolsCyril SIX2020-10-016-17/+29
| | |
| * | ccomp.force target for forcing compilation without Coq processingDavid Monniaux2020-10-012-0/+8
| | |
| * | non pipelined units = none on KVXDavid Monniaux2020-09-301-1/+3
| | |
| * | non trapping opDavid Monniaux2020-09-304-88/+73
| | |
| * | non trappingDavid Monniaux2020-09-301-2/+0
| | |
| * | AArch64 division no longer "traps"David Monniaux2020-09-306-81/+221
| | |
| * | floating-point division uses the divisorDavid Monniaux2020-09-291-4/+5
| | |
| * | attempt at separating the divisionsDavid Monniaux2020-09-292-1/+18
| | |
| * | try to model resourcesDavid Monniaux2020-09-291-5/+164
| | |
| * | attempt at latencies for Cortex A53David Monniaux2020-09-291-2/+147
| | |
| * | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-09-2924-770/+766
| |\|
| | * simpl -> cbnDavid Monniaux2020-09-2923-793/+789
| | |
| * | rules.mk for zigzagDavid Monniaux2020-09-241-7/+7
| | |
| * | attempt at "zigzag" scheduler; not quite testable due to issues in the ↵David Monniaux2020-09-242-1/+36
| | | | | | | | | | | | duplicate/linearize passes
| * | Merge remote-tracking branch 'origin/kvx-work-riscV' into kvx-test-prepassDavid Monniaux2020-09-221-14/+0
| |\ \
| | * | reflect changesDavid Monniaux2020-09-221-14/+0
| | | |
| * | | Merge remote-tracking branch 'origin/kvx-work-riscV' into kvx-test-prepassDavid Monniaux2020-09-2110-512/+874
| |\| |
| | * | risc-V now without trapping instructionsDavid Monniaux2020-09-215-74/+114
| | | |
| | * | moved Risc-V div ValueAOp to central locationDavid Monniaux2020-09-212-293/+215
| | | |
| | * | moved some "total" value domain functions to a central locationDavid Monniaux2020-09-212-272/+243
| | | |
| | * | maketotal mod & divDavid Monniaux2020-09-216-165/+593
| | |/
| | * config for KVX ELFDavid Monniaux2020-09-101-0/+1
| | | | | | | | | | | | config for KVX ELF
| | * use scheduler_by_nameDavid Monniaux2020-09-103-9/+11
| | |
| * | fix issue 210 in simu_checkSylvain Boulmé2020-09-212-15/+33
| | |
| * | more debug info for simu_checkSylvain Boulmé2020-09-211-6/+16
| | |
| * | wrong resourcesDavid Monniaux2020-09-181-1/+1
| | |
| * | EH1 schedulingDavid Monniaux2020-09-181-5/+18
| | |
| * | bogus OpWeights for Risc-VDavid Monniaux2020-09-182-1/+20
| | |
| * | first opweights, bogus weightsDavid Monniaux2020-09-161-0/+19
| | |
| * | just missing OpWeights for AARCH64David Monniaux2020-09-1617-5/+15
| | |
| * | starting to move common filesDavid Monniaux2020-09-1619-4/+5
| | |
| * | Merge branch 'mppa-RTLpathSE-verif-hash-junk' of ↵David Monniaux2020-09-1020-10048/+342
| |\ \ | | | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-RTLpathSE-verif-hash-junk
generated by cgit (git 2.34.1) at 2024-07-12 00:55:25 +0000