aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c/Asmblockdeps.v
Commit message (Expand)AuthorAgeFilesLines
* select cmpuDavid Monniaux2019-04-051-0/+1
* Merge remote-tracking branch 'origin/mppa-work' into mppa-ternaryDavid Monniaux2019-04-041-350/+185
|\
| * 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-work' into mppa-ternaryDavid Monniaux2019-04-031-262/+432
|\|
| * 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 branch 'mppa-mul' into mppa-jumptableDavid Monniaux2019-03-221-29/+1
| |\ \
| * | | Fixed proof of Asmblockdeps wrt PjumptableCyril SIX2019-03-221-25/+28
| * | | begin jumptables (does not work)David Monniaux2019-03-211-1/+41
* | | | merge VLIW proofsDavid Monniaux2019-03-281-4/+518
|\ \ \ \ | | |_|/ | |/| |
| * | | 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
| | |\ \
| | | * | Proof of the entire forward simulation (still stuck to do + permutations)Cyril SIX2019-03-271-3/+10
| | | * | Preuve du forward_simu du parexec_wio_bblock_auxCyril SIX2019-03-271-53/+63
| | * | | dealing with permutationsSylvain Boulmé2019-03-271-29/+82
| | |/ /
| | * | Avancement dans Asmblockdeps.vCyril SIX2019-03-271-88/+109
| | * | 1 coup de pouce !Sylvain Boulmé2019-03-261-9/+29
| | * | Un peu d'avancementCyril SIX2019-03-261-2/+274
| | * | Avancement dans la preuve des bundlesCyril SIX2019-03-221-3/+51
| | * | fix for Coq.8.8 ??Sylvain Boulmé2019-03-221-2/+3
| | * | Décomposition de la preuve en une forward_simu_par_stuck et une forward_simu...Cyril SIX2019-03-221-0/+68
* | | | progress on cmoveDavid Monniaux2019-03-251-0/+1
| |_|/ |/| |
* | | rm Pdiv / PdivuDavid Monniaux2019-03-221-29/+0
|/ /
* | Merge branch 'mppa-madd' into mppa_postpassDavid Monniaux2019-03-191-15/+82
|\ \
| * | mul immediate beginDavid Monniaux2019-03-191-0/+2
| * | improve robustness of Asmblockdeps.arith_op_eq.Sylvain Boulmé2019-03-191-13/+29
| * | fix missing case in Asmblockdeps.arith_op_eqSylvain Boulmé2019-03-191-2/+2
| * | ça passe mais pas encore l'oracleDavid Monniaux2019-03-181-1/+50
* | | Pseudo instruction for 32 bits division, no code generation yetCyril SIX2019-03-191-0/+45
* | | Merge branch 'mppa_postpass' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/Co...Cyril SIX2019-03-181-0/+8
|\| |
| * | orn / andn in asmDavid Monniaux2019-03-181-0/+8
* | | The parent frame pointer is now R17 instead of R14Cyril SIX2019-03-181-2/+2
|/ /
* | long nand, nor, nxorDavid Monniaux2019-03-161-0/+6
* | nxorDavid Monniaux2019-03-161-0/+2
generated by cgit (git 2.34.1) at 2024-07-06 17:33:35 +0000