aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c/Asmblockdeps.v
Commit message (Expand)AuthorAgeFilesLines
...
| * | | 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
| | |\ \
| | | * | 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
* | | | Merge branch 'mppa-mul' into mppa-jumptableDavid Monniaux2019-03-221-29/+1
|\ \ \ \ | | |_|/ | |/| |
| * | | rm Pdiv / PdivuDavid Monniaux2019-03-221-29/+0
| |/ /
* | | Fixed proof of Asmblockdeps wrt PjumptableCyril SIX2019-03-221-25/+28
* | | begin jumptables (does not work)David Monniaux2019-03-211-1/+41
|/ /
* | 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
* | partial norwDavid Monniaux2019-03-161-0/+2
* | nand is implementedDavid Monniaux2019-03-161-0/+2
* | 32-bit rotate finishedDavid Monniaux2019-03-161-0/+1
|/
* Enlevé la dépendance mémoire de PcbuCyril SIX2019-03-131-20/+20
* Proof of exec_trans_pcincr solvedCyril SIX2019-03-121-7/+31
* Merge remote-tracking branch 'origin/mppa_parcheck' into mppa_parcheckCyril SIX2019-03-121-12/+12
|\
| * fix trans_pcincr for parcheck. (Proof is broken. cf FIXME)Sylvain Boulmé2019-03-121-12/+12
* | Simplification des preuves "de discrimination" dans AsmblockdepsCyril SIX2019-03-121-94/+77
|/
* [BROKEN] Added parallelizability check - breaks all the conditional jumpsCyril SIX2019-03-121-0/+8
* Refactorisation des load et des storeCyril SIX2019-03-081-27/+5
* Merge remote-tracking branch 'origin/mppa_postpass' into mppa_memory_model_patchCyril SIX2019-03-081-10/+14
|\
| * Remplacement de phys_eq par Z.eqb pour Allocframe (1 & 2) et Freeframe (1 & 2)Cyril SIX2019-03-071-10/+14
* | Fixing Asmblockdeps proofsCyril SIX2019-03-081-147/+21
* | remove dep of exec_arith_instr on memory.Sylvain Boulmé2019-03-071-17/+8
* | Experiment Patch of Memory ModelSylvain Boulmé2019-03-071-2/+2
|/
* fix eq sur OIncremPCSylvain Boulmé2019-03-061-7/+14
generated by cgit (git 2.34.1) at 2024-07-12 05:55:17 +0000