aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c
Commit message (Collapse)AuthorAgeFilesLines
* Possible fix pour l'issue #82 (mauvais calcul de taille de bundle pour les ↵Cyril SIX2019-04-051-1/+1
| | | | store)
* 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
|\ | | | | | | | | Conflicts: mppa_k1c/Asmblockdeps.v
| * 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
| | | | | | | | | | Resource -> PseudoReg macro -> inst
| * 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
| | | | | | | | in order to avoid to keep these files up-to-date here...
* | 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 ↵Cyril SIX2019-04-036-77/+196
| | | | | | | | preuves de Asmblockdeps
* | 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
|\ \ | |/ |/| | | | | | | Conflicts: mppa_k1c/Asmblock.v mppa_k1c/Asmblockdeps.v
| * 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 ↵Sylvain Boulmé2019-03-272-67/+80
| | |\ | | | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_vliw_essai_sylvain
| | | * 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 ↵Cyril SIX2019-03-222-1/+72
| | | | | | | | | | | | forward_simu_par
| | * 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
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - Actually, we want to show that the outcome is the same for any order of "writes" in the parallel execution. (ie we ask that bundles have a deterministic semantics for parallel execution) - we relax the condition that the outcome should be given for sequential execution instead, we ask that the it is given for the "in order" writes. In theory, the semantics would also accept bundles like "R1 := R2 R2 := R1" which are deterministic for parallel execution But, of course, in practice, we will also prove the sequential execution.
| | * definition of VLIW semanticsSylvain Boulmé2019-03-143-14/+342
| | |
generated by cgit (git 2.34.1) at 2024-07-14 09:15:23 +0000