aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c/Asmblock.v
Commit message (Expand)AuthorAgeFilesLines
* it compiles!David Monniaux2019-05-041-0/+4
* begin add PlqDavid Monniaux2019-05-031-0/+2
* it compilesDavid Monniaux2019-05-031-0/+2
* rm Ofslow (résidu du Risc-V, inutilisé et complique les preuves)David Monniaux2019-05-031-2/+2
* it compilesDavid Monniaux2019-05-011-0/+2
* begin load.xsDavid Monniaux2019-05-011-0/+2
* Merge remote-tracking branch 'origin/mppa-refactor-reviewed' into mppa-refactorCyril SIX2019-04-081-128/+222
|\
| * relecture sylvainSylvain Boulmé2019-04-051-168/+244
* | #91 Removed completely the duplicated semantics in AsmblockCyril SIX2019-04-051-180/+9
|/
* #90 Asmvliw/Asmblock refactoring attemptCyril SIX2019-04-051-1341/+9
* Merge remote-tracking branch 'origin/mppa_k1c' into mppa-workCyril SIX2019-04-031-1/+4
|\
| * cleaning Asmvliw semanticsSylvain Boulmé2019-04-011-1/+4
* | Preuve des load/store registre registre. Reste des modifs mineures dans les p...Cyril SIX2019-04-031-24/+14
* | Small refactoring and renaming of Stores and LoadsCyril SIX2019-04-031-10/+10
* | Added definition of PLoadRRR and PStoreRRR - no Asmblockgen generation yetCyril SIX2019-04-021-14/+38
|/
* Merge remote-tracking branch 'origin/mppa_postpass' into mppa-jumptableCyril SIX2019-03-291-10/+11
|\
| * Merge remote-tracking branch 'origin/mppa_vliw_essai_sylvain' into mppa_postpassDavid Monniaux2019-03-281-22/+9
| |\
| | * definition of VLIW semanticsSylvain Boulmé2019-03-141-9/+9
* | | Merge branch 'mppa-mul' into mppa-jumptableDavid Monniaux2019-03-221-15/+1
|\ \ \
| * | | rm Pdiv / PdivuDavid Monniaux2019-03-221-15/+1
| |/ /
* / / begin jumptables (does not work)David Monniaux2019-03-211-0/+11
|/ /
* | Merge branch 'mppa-madd' into mppa_postpassDavid Monniaux2019-03-191-0/+45
|\ \
| * | mul immediate beginDavid Monniaux2019-03-191-0/+4
| * | maddw dans la générationDavid Monniaux2019-03-181-0/+3
| * | ça passe mais pas encore l'oracleDavid Monniaux2019-03-181-0/+38
* | | Pseudo instruction for 32 bits division, no code generation yetCyril SIX2019-03-191-3/+14
* | | Merge branch 'mppa_postpass' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/Co...Cyril SIX2019-03-181-0/+16
|\| |
| * | orn / andn in asmDavid Monniaux2019-03-181-0/+16
* | | The parent frame pointer is now R17 instead of R14Cyril SIX2019-03-181-2/+3
|/ /
* | long nand, nor, nxorDavid Monniaux2019-03-161-0/+12
* | nxorDavid Monniaux2019-03-161-0/+4
* | partial norwDavid Monniaux2019-03-161-3/+7
* | nand is implementedDavid Monniaux2019-03-161-0/+4
* | 32-bit rotate finishedDavid Monniaux2019-03-161-1/+2
|/
* Enlevé la dépendance mémoire de PcbuCyril SIX2019-03-131-2/+2
* Refactorisation des load et des storeCyril SIX2019-03-081-32/+32
* Refactorized Asmblock exec_basic_instrCyril SIX2019-03-081-104/+120
* axioms on pointer comparison removed !Sylvain Boulmé2019-03-071-11/+12
* remove dep of exec_arith_instr on memory.Sylvain Boulmé2019-03-071-18/+46
* Experiment Patch of Memory ModelSylvain Boulmé2019-03-071-9/+30
* Added double comparisonsCyril SIX2019-03-011-1/+14
* Implemented float comparisons (no branching yet, and no negation)Cyril SIX2019-03-011-0/+49
* Ointuofsingle doneCyril SIX2019-03-011-0/+2
* Float conversion fixes + some more conversionsCyril SIX2019-02-271-2/+14
* Proving the trans_block_header axiomsCyril SIX2019-02-271-0/+30
* Remove unnecessary and error prone FR constructor for pregsCyril SIX2019-02-201-5/+2
* Rajout d'opérateurs flottants, travail sur les tests --> à continuerCyril SIX2019-02-151-6/+33
* Added Olongoffloat, Ofloatoflong and doubleconv testCyril SIX2019-02-121-0/+4
* Added Ointofsingle + floatconv unit testCyril SIX2019-02-121-1/+3
* Added OsingleofintCyril SIX2019-02-121-0/+2
generated by cgit (git 2.34.1) at 2024-07-04 14:56:19 +0000