aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
...
| * | | | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-315-17/+121
| |\ \ \ \ \ \
| * \ \ \ \ \ \ Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-304-168/+78
| |\ \ \ \ \ \ \
| * \ \ \ \ \ \ \ Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-295-48/+109
| |\ \ \ \ \ \ \ \
| * \ \ \ \ \ \ \ \ Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-284-42/+27
| |\ \ \ \ \ \ \ \ \
| * \ \ \ \ \ \ \ \ \ Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-277-63/+166
| |\ \ \ \ \ \ \ \ \ \
| * \ \ \ \ \ \ \ \ \ \ Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-277-10/+277
| |\ \ \ \ \ \ \ \ \ \ \
| * | | | | | | | | | | | improved CSE3David Monniaux2020-10-271-12/+12
| | | | | | | | | | | | |
| * | | | | | | | | | | | progress in proofs on new CSE3David Monniaux2020-10-271-3/+34
| | | | | | | | | | | | |
| * | | | | | | | | | | | deactivate LICM by defaultDavid Monniaux2020-10-272-21/+12
| | | | | | | | | | | | |
| * | | | | | | | | | | | begin fixing CSE3 to keep more inductive stuffDavid Monniaux2020-10-272-10/+19
| | | | | | | | | | | | |
| * | | | | | | | | | | | invariant printing more aligned with RTL dumpsDavid Monniaux2020-10-271-2/+2
| | | | | | | | | | | | |
| * | | | | | | | | | | | print invariantsDavid Monniaux2020-10-271-11/+46
| | | | | | | | | | | | |
| * | | | | | | | | | | | attempt at store -> load.sDavid Monniaux2020-10-261-2/+3
| | | | | | | | | | | | |
| * | | | | | | | | | | | new OpWeightsDavid Monniaux2020-10-222-0/+25
| | | | | | | | | | | | |
| * | | | | | | | | | | | new OpWeights for aarch64David Monniaux2020-10-221-318/+342
| | | | | | | | | | | | |
| * | | | | | | | | | | | -mtune=David Monniaux2020-10-222-1/+5
| | | | | | | | | | | | |
| * | | | | | | | | | | | allow changing target cpuDavid Monniaux2020-10-222-21/+40
| | | | | | | | | | | | |
| * | | | | | | | | | | | allow changing the target coreDavid Monniaux2020-10-222-120/+160
| | | | | | | | | | | | |
| * | | | | | | | | | | | prefix all calls to OpWeights as preparation to using a structureDavid Monniaux2020-10-221-14/+14
| | | | | | | | | | | | |
| * | | | | | | | | | | | attempt at modeling RocketDavid Monniaux2020-10-221-0/+83
| | | | | | | | | | | | |
| * | | | | | | | | | | | turn on cache emulationDavid Monniaux2020-10-191-9/+9
| | | | | | | | | | | | |
| * | | | | | | | | | | | op_valid_pointer_eq x86David Monniaux2020-10-191-0/+14
| | | | | | | | | | | | |
| * | | | | | | | | | | | op_valid_pointer_eq ppcDavid Monniaux2020-10-191-0/+14
| | | | | | | | | | | | |
| * | | | | | | | | | | | op_valid_pointer_eq armDavid Monniaux2020-10-191-0/+15
| | | | | | | | | | | | |
| * | | | | | | | | | | | op_valid_pointer_eq for aarch64David Monniaux2020-10-191-0/+14
| | | | | | | | | | | | |
| * | | | | | | | | | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-1822-176/+939
| |\ \ \ \ \ \ \ \ \ \ \ \
| * | | | | | | | | | | | | 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
| | |\ \ \ \ \ \ \ \ \ \ \ \ \
| | * | | | | | | | | | | | | | 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
| | |\ \ \ \ \ \ \ \ \ \ \ \ \ \
| | * | | | | | | | | | | | | | | 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
| | |\| | | | | | | | | | | | | | |
generated by cgit (git 2.34.1) at 2024-07-12 05:06:50 +0000