Commit message (Expand) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | start checking for bugs | David Monniaux | 2020-12-02 | 2 | -3/+116 |
* | attempt at initial analysis | David Monniaux | 2020-12-02 | 1 | -1/+35 |
* | cond_depends_on | David Monniaux | 2020-12-02 | 3 | -21/+21 |
* | simpl -> cbn | David Monniaux | 2020-12-02 | 1 | -9/+9 |
* | cond_depends_on_memory for KVX | David Monniaux | 2020-12-02 | 1 | -4/+17 |
* | Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3 | David Monniaux | 2020-12-02 | 79 | -731/+10580 |
|\ | |||||
| * | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | Cyril SIX | 2020-12-01 | 6 | -11/+161 |
| |\ | |||||
| * | | Ignore loopback edges on tail-duplicate | Cyril SIX | 2020-12-01 | 1 | -0/+2 |
| * | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-11-24 | 13 | -31/+343 |
| |\ \ | |||||
| * | | | prepass scheduling proof finished ! | Sylvain Boulmé | 2020-11-20 | 1 | -24/+56 |
| * | | | merge nouveau tunneling | David Monniaux | 2020-11-19 | 1 | -1/+1 |
| * | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-11-19 | 8 | -270/+728 |
| |\ \ \ | |||||
| * | | | | seval_builtin_sval_preserved | David Monniaux | 2020-11-17 | 1 | -1/+4 |
| * | | | | a little lemma on list of builtins | David Monniaux | 2020-11-17 | 1 | -2/+15 |
| * | | | | there remains two tricky cases | David Monniaux | 2020-11-16 | 1 | -3/+14 |
| * | | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-11-06 | 2 | -27/+32 |
| |\ \ \ \ | |||||
| * \ \ \ \ | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-11-05 | 5 | -31/+114 |
| |\ \ \ \ \ | |||||
| * | | | | | | disable debug printing in scheduler | David Monniaux | 2020-11-04 | 2 | -7/+9 |
| * | | | | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-11-04 | 1 | -1/+2 |
| |\ \ \ \ \ \ | |||||
| * \ \ \ \ \ \ | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-11-03 | 7 | -36/+121 |
| |\ \ \ \ \ \ \ | |||||
| * \ \ \ \ \ \ \ | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-10-31 | 5 | -17/+121 |
| |\ \ \ \ \ \ \ \ | |||||
| * \ \ \ \ \ \ \ \ | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-10-30 | 4 | -168/+78 |
| |\ \ \ \ \ \ \ \ \ | |||||
| * \ \ \ \ \ \ \ \ \ | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-10-29 | 5 | -48/+109 |
| |\ \ \ \ \ \ \ \ \ \ | |||||
| * \ \ \ \ \ \ \ \ \ \ | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-10-28 | 4 | -42/+27 |
| |\ \ \ \ \ \ \ \ \ \ \ | |||||
| * \ \ \ \ \ \ \ \ \ \ \ | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-10-27 | 7 | -63/+166 |
| |\ \ \ \ \ \ \ \ \ \ \ \ | |||||
| * \ \ \ \ \ \ \ \ \ \ \ \ | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-10-27 | 7 | -10/+277 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ | |||||
| * | | | | | | | | | | | | | | improved CSE3 | David Monniaux | 2020-10-27 | 1 | -12/+12 |
| * | | | | | | | | | | | | | | progress in proofs on new CSE3 | David Monniaux | 2020-10-27 | 1 | -3/+34 |
| * | | | | | | | | | | | | | | deactivate LICM by default | David Monniaux | 2020-10-27 | 2 | -21/+12 |
| * | | | | | | | | | | | | | | begin fixing CSE3 to keep more inductive stuff | David Monniaux | 2020-10-27 | 2 | -10/+19 |
| * | | | | | | | | | | | | | | invariant printing more aligned with RTL dumps | David Monniaux | 2020-10-27 | 1 | -2/+2 |
| * | | | | | | | | | | | | | | print invariants | David Monniaux | 2020-10-27 | 1 | -11/+46 |
| * | | | | | | | | | | | | | | attempt at store -> load.s | David Monniaux | 2020-10-26 | 1 | -2/+3 |
| * | | | | | | | | | | | | | | new OpWeights | David Monniaux | 2020-10-22 | 2 | -0/+25 |
| * | | | | | | | | | | | | | | new OpWeights for aarch64 | David Monniaux | 2020-10-22 | 1 | -318/+342 |
| * | | | | | | | | | | | | | | -mtune= | David Monniaux | 2020-10-22 | 2 | -1/+5 |
| * | | | | | | | | | | | | | | allow changing target cpu | David Monniaux | 2020-10-22 | 2 | -21/+40 |
| * | | | | | | | | | | | | | | allow changing the target core | David Monniaux | 2020-10-22 | 2 | -120/+160 |
| * | | | | | | | | | | | | | | prefix all calls to OpWeights as preparation to using a structure | David Monniaux | 2020-10-22 | 1 | -14/+14 |
| * | | | | | | | | | | | | | | attempt at modeling Rocket | David Monniaux | 2020-10-22 | 1 | -0/+83 |
| * | | | | | | | | | | | | | | turn on cache emulation | David Monniaux | 2020-10-19 | 1 | -9/+9 |
| * | | | | | | | | | | | | | | op_valid_pointer_eq x86 | David Monniaux | 2020-10-19 | 1 | -0/+14 |
| * | | | | | | | | | | | | | | op_valid_pointer_eq ppc | David Monniaux | 2020-10-19 | 1 | -0/+14 |
| * | | | | | | | | | | | | | | op_valid_pointer_eq arm | David Monniaux | 2020-10-19 | 1 | -0/+15 |
| * | | | | | | | | | | | | | | op_valid_pointer_eq for aarch64 | David Monniaux | 2020-10-19 | 1 | -0/+14 |
| * | | | | | | | | | | | | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-10-18 | 22 | -176/+939 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||||
| * | | | | | | | | | | | | | | | simplify HSop (and merge hSop and hSop_Sinit) | Sylvain Boulmé | 2020-10-17 | 2 | -42/+23 |
| * | | | | | | | | | | | | | | | update op_valid_pointer_eq proof on the KVX | Sylvain Boulmé | 2020-10-17 | 1 | -22/+4 |
| * | | | | | | | | | | | | | | | proves op_valid_pointer_eq lemma for RISC-V (necessary for the pre-pass sched... | Sylvain Boulmé | 2020-10-17 | 2 | -0/+32 |
| * | | | | | | | | | | | | | | | fixing the move of the verified prepass scheduler into scheduling/ directory | Sylvain Boulmé | 2020-10-17 | 4 | -762/+2 |