aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c/Asmblockdeps.v
Commit message (Expand)AuthorAgeFilesLines
* Lq finished ?David Monniaux2019-05-031-15/+16
* begin add PlqDavid Monniaux2019-05-031-2/+58
* use sq to save pairs of registersDavid Monniaux2019-05-031-3/+16
* ça avanceDavid Monniaux2019-05-031-0/+27
* Merge remote-tracking branch 'origin/mppa-work' into mppa-peepholeDavid Monniaux2019-05-031-4/+5
|\
| * rm Ofslow (résidu du Risc-V, inutilisé et complique les preuves)David Monniaux2019-05-031-4/+5
* | getting stuck need to move offsetsDavid Monniaux2019-05-031-3/+8
|/
* does not yet work, arity mismatchDavid Monniaux2019-05-011-0/+1
* it compilesDavid Monniaux2019-05-011-0/+20
* begin load.xsDavid Monniaux2019-05-011-0/+20
* removed fake ops for int32 -> doubleDavid Monniaux2019-04-291-2/+0
* Srsd / SrswDavid Monniaux2019-04-291-0/+4
* begin add bitfield insertionDavid Monniaux2019-04-271-2/+18
* start of extfzl/extfslDavid Monniaux2019-04-251-0/+2
* progressDavid Monniaux2019-04-251-0/+1
* begin bitfieldsDavid Monniaux2019-04-241-0/+1
* more robust pattern-matching in *op_eqSylvain Boulmé2019-04-111-8/+10
* refactor for #92Sylvain Boulmé2019-04-111-785/+305
* achieve issue #89 ?Sylvain Boulmé2019-04-101-185/+47
* Merge remote-tracking branch 'origin/mppa-work' into mppa-refactorCyril SIX2019-04-081-0/+2
|\
| * select cmpuDavid Monniaux2019-04-051-0/+1
| * Merge remote-tracking branch 'origin/mppa-work' into mppa-ternaryDavid Monniaux2019-04-041-350/+185
| |\
| * \ Merge remote-tracking branch 'origin/mppa-work' into mppa-ternaryDavid Monniaux2019-04-031-262/+432
| |\ \
| * \ \ merge VLIW proofsDavid Monniaux2019-03-281-4/+518
| |\ \ \
| * | | | progress on cmoveDavid Monniaux2019-03-251-0/+1
* | | | | Merge remote-tracking branch 'origin/mppa-refactor-reviewed' into mppa-refactorCyril SIX2019-04-081-17/+17
|\ \ \ \ \
| * | | | | relecture sylvainSylvain Boulmé2019-04-051-17/+17
* | | | | | #91 Removed completely the duplicated semantics in AsmblockCyril SIX2019-04-051-34/+34
|/ / / / /
* | | | / #90 Asmvliw/Asmblock refactoring attemptCyril SIX2019-04-051-7/+7
| |_|_|/ |/| | |
* | | | Refactorisation de forward_simu_basicCyril SIX2019-04-041-102/+55
* | | | refactorized forward_simu_controlCyril SIX2019-04-041-107/+67
* | | | Refactorisation de forward_simu_par_controlCyril SIX2019-04-041-141/+63
| |_|/ |/| |
* | | Merge remote-tracking branch 'origin/mppa_k1c' into mppa-workCyril SIX2019-04-031-218/+188
|\ \ \
| * | | robustness of Asmblockdeps.*op_eqSylvain Boulmé2019-04-021-27/+38
| * | | comment on Asmblockdeps.is_constantSylvain Boulmé2019-04-021-9/+12
| * | | Impure: improved iandb + struct_eqSylvain Boulmé2019-04-011-31/+17
| * | | renommage abstractbb: Name -> PRegSylvain Boulmé2019-04-011-25/+25
| * | | renommages abstract_bbSylvain Boulmé2019-04-011-24/+24
| * | | petite factorisation de preuveSylvain Boulmé2019-04-011-69/+59
| * | | simpler parexec_wio_bblock_auxSylvain Boulmé2019-04-011-2/+2
| * | | cleaning Asmvliw semanticsSylvain Boulmé2019-04-011-5/+3
* | | | Load/Store reg-reg are now proven everywhereCyril SIX2019-04-031-68/+54
* | | | Preuve des load/store registre registre. Reste des modifs mineures dans les p...Cyril SIX2019-04-031-12/+14
* | | | Small refactoring and renaming of Stores and LoadsCyril SIX2019-04-031-12/+12
* | | | Added definition of PLoadRRR and PStoreRRR - no Asmblockgen generation yetCyril SIX2019-04-021-60/+166
|/ / /
* | | Preuve de Jumptable dans Asmblockdeps.vCyril SIX2019-03-291-0/+15
* | | Merge remote-tracking branch 'origin/mppa_postpass' into mppa-jumptableCyril SIX2019-03-291-4/+565
|\ \ \
| * | | No more AdmittedCyril SIX2019-03-291-55/+102
| | |/ | |/|
| * | Merge remote-tracking branch 'origin/mppa_vliw_essai_sylvain' into mppa_postpassDavid Monniaux2019-03-281-33/+518
| |\ \
| | * \ Merge branch 'mppa_vliw_essai_sylvain' of gricad-gitlab.univ-grenoble-alpes.f...Sylvain Boulmé2019-03-271-60/+73
| | |\ \
generated by cgit (git 2.34.1) at 2024-07-07 06:05:05 +0000