aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c
Commit message (Expand)AuthorAgeFilesLines
* Possible fix pour l'issue #82 (mauvais calcul de taille de bundle pour les st...Cyril SIX2019-04-051-1/+1
* 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
* Erreur idiote dans les latences ?Cyril SIX2019-04-041-2/+2
* Merge remote-tracking branch 'origin/mppa_k1c' into mppa-workCyril SIX2019-04-0314-1456/+421
|\
| * 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-013-34/+28
| * renommage abstractbb: Name -> PRegSylvain Boulmé2019-04-015-32/+32
| * renommages abstract_bbSylvain Boulmé2019-04-015-156/+156
| * petite factorisation de preuveSylvain Boulmé2019-04-011-69/+59
| * minor simplSylvain Boulmé2019-04-011-8/+14
| * simpler parexec_wio_bblock_auxSylvain Boulmé2019-04-012-3/+2
| * cleaning Asmvliw semanticsSylvain Boulmé2019-04-014-42/+73
| * delete useless DepExample* filesSylvain Boulmé2019-04-014-1051/+0
* | Load/Store reg-reg are now proven everywhereCyril SIX2019-04-032-92/+68
* | Preuve des load/store registre registre. Reste des modifs mineures dans les p...Cyril SIX2019-04-036-77/+196
* | Preuve du transl_load et transl_store registre offsetCyril SIX2019-04-032-30/+89
* | We now generate load/store with 3 registers (ld rd rs1[rs2]), proofs admittedCyril SIX2019-04-033-494/+51
* | Small refactoring and renaming of Stores and LoadsCyril SIX2019-04-033-70/+50
* | Added definition of PLoadRRR and PStoreRRR - no Asmblockgen generation yetCyril SIX2019-04-0210-205/+417
* | Started to add addressing with register + register, Mach -> Asm not done yetCyril SIX2019-04-015-3/+12
* | Using fixedd.rz in longofsingle instead of i64_dtosCyril SIX2019-04-012-8/+13
|/
* fix for jump tablesv3.5_k1c_1.0David Monniaux2019-03-301-14/+18
* Merge remote-tracking branch 'origin/mppa-jumptable' into mppa-jumptableCyril SIX2019-03-291-2/+5
|\
| * Finition de la preuve de AsmblockgenproofCyril SIX2019-03-291-2/+5
* | Preuve de Jumptable dans Asmblockdeps.vCyril SIX2019-03-292-1/+24
* | Merge remote-tracking branch 'origin/mppa_postpass' into mppa-jumptableCyril SIX2019-03-297-23/+1120
|\ \ | |/ |/|
| * No more AdmittedCyril SIX2019-03-291-55/+102
| * Merge remote-tracking branch 'origin/mppa_vliw_essai_sylvain' into mppa_postpassDavid Monniaux2019-03-289-74/+1071
| |\
| | * Merge branch 'mppa_vliw_essai_sylvain' of gricad-gitlab.univ-grenoble-alpes.f...Sylvain Boulmé2019-03-272-67/+80
| | |\
| | | * 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-272-60/+70
| | * | dealing with permutationsSylvain Boulmé2019-03-272-29/+100
| | |/
| | * Avancement dans Asmblockdeps.vCyril SIX2019-03-272-91/+113
| | * 1 coup de pouce !Sylvain Boulmé2019-03-261-9/+29
| | * Un peu d'avancementCyril SIX2019-03-262-4/+287
| | * slight simplificationSylvain Boulmé2019-03-231-5/+4
| | * Avancement dans la preuve des bundlesCyril SIX2019-03-221-3/+51
| | * fix for Coq.8.8 ??Sylvain Boulmé2019-03-222-4/+3
| | * Décomposition de la preuve en une forward_simu_par_stuck et une forward_simu...Cyril SIX2019-03-222-1/+72
| | * simplification of the proofSylvain Boulmé2019-03-212-29/+70
| | * yet another step backwardSylvain Boulmé2019-03-201-18/+39
| | * one step further...Sylvain Boulmé2019-03-201-6/+28
| | * premier decoupageSylvain Boulmé2019-03-201-2/+56
| | * Integrating Asmvliw.v in the proof chainCyril SIX2019-03-203-16/+29
| | * Idée de preuve VLIWCyril SIX2019-03-181-2/+21
| | * fix the step_internal of AsmvliwSylvain Boulmé2019-03-141-19/+23
| | * definition of VLIW semanticsSylvain Boulmé2019-03-143-14/+342
generated by cgit (git 2.34.1) at 2024-07-07 05:59:11 +0000