aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c/Asmvliw.v
Commit message (Collapse)AuthorAgeFilesLines
* Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-loadDavid Monniaux2019-09-101-13/+0
|\
| * Removing unused .all, .any, .nall and .none conditionsCyril SIX2019-09-051-13/+0
| |
* | asmblockgen worksDavid Monniaux2019-09-081-1/+1
| |
* | moving forward on K1CDavid Monniaux2019-09-071-16/+33
|/
* Merge remote-tracking branch 'origin/mppa-work-upstream-merge' into mppa-workCyril SIX2019-09-031-0/+19
|\ | | | | | | | | | | | | Conflicts: configure mppa_k1c/Archi.v mppa_k1c/Asmexpand.ml
| * fmaDavid Monniaux2019-08-301-0/+8
| |
| * add finvw ; not yet generatedDavid Monniaux2019-08-301-0/+2
| |
| * fmin/fmax/fminf/fmaxf non bien testésDavid Monniaux2019-08-291-0/+9
| |
* | (#156) - Un peu de cleaning et de docCyril SIX2019-07-301-21/+4
| |
* | (#139) - Quelques renommagesCyril SIX2019-07-301-4/+4
|/
* maj forward_simu_par_wio_bblock_aux en forward_simu_par_wioSylvain Boulmé2019-06-231-9/+9
| | | | avec une legere simplification (comme dans le papier)
* added immediate cmoveDavid Monniaux2019-06-041-32/+44
|
* standardize semantics, 1David Monniaux2019-05-121-6/+5
|
* apply .xs onto addx4 etcDavid Monniaux2019-05-111-1/+1
|
* add with shift, beginningDavid Monniaux2019-05-111-2/+2
|
* Oaddx -> PDavid Monniaux2019-05-111-2/+2
|
* begin generating Prevsub etc. from Oxxx to PxxxDavid Monniaux2019-05-111-12/+12
|
* use shift 1-4 in backendDavid Monniaux2019-05-101-43/+18
|
* new instructions at asm levelDavid Monniaux2019-05-101-1/+53
|
* simplification semantique+preuve des load_q+load_oSylvain Boulmé2019-05-061-7/+7
|
* big proofs for so / loDavid Monniaux2019-05-041-1/+83
|
* begin add PlqDavid Monniaux2019-05-031-9/+22
|
* use sq to save pairs of registersDavid Monniaux2019-05-031-3/+2
|
* Merge remote-tracking branch 'origin/mppa-work' into mppa-peepholeDavid Monniaux2019-05-031-12/+2
|\
| * rm Ofslow (résidu du Risc-V, inutilisé et complique les preuves)David Monniaux2019-05-031-12/+2
| |
* | getting stuck need to move offsetsDavid Monniaux2019-05-031-6/+21
| |
* | find consecutive writesDavid Monniaux2019-05-021-0/+51
|/
* does not yet work, arity mismatchDavid Monniaux2019-05-011-15/+1
|
* it compilesDavid Monniaux2019-05-011-6/+8
|
* translate load.xsDavid Monniaux2019-05-011-4/+4
|
* begin load.xsDavid Monniaux2019-05-011-0/+23
|
* removed fake ops for int32 -> doubleDavid Monniaux2019-04-291-4/+0
|
* Srsd / SrswDavid Monniaux2019-04-291-0/+8
|
* begin add bitfield insertionDavid Monniaux2019-04-271-2/+16
|
* moved operators to specific file instead of common fileDavid Monniaux2019-04-271-4/+5
|
* start of extfzl/extfslDavid Monniaux2019-04-251-0/+4
|
* progressDavid Monniaux2019-04-251-0/+2
|
* IT COMPILESDavid Monniaux2019-04-251-1/+1
|
* begin bitfieldsDavid Monniaux2019-04-241-1/+4
|
* improving comments on AsmvliwSylvain Boulmé2019-04-081-17/+29
|
* Merge remote-tracking branch 'origin/mppa-work' into mppa-refactorCyril SIX2019-04-081-1/+35
|\ | | | | | | | | | | Conflicts: mppa_k1c/Asm.v mppa_k1c/Asmblock.v
* | relecture sylvainSylvain Boulmé2019-04-051-298/+69
| | | | | | | | avec TODOs pour refactoring #90
* | #90 Asmvliw/Asmblock refactoring attemptCyril SIX2019-04-051-4/+1359
|/
* Merge remote-tracking branch 'origin/mppa_k1c' into mppa-workCyril SIX2019-04-031-20/+61
|\ | | | | | | | | Conflicts: mppa_k1c/Asmblockdeps.v
| * simpler parexec_wio_bblock_auxSylvain Boulmé2019-04-011-1/+0
| |
| * cleaning Asmvliw semanticsSylvain Boulmé2019-04-011-19/+61
| |
* | Load/Store reg-reg are now proven everywhereCyril SIX2019-04-031-24/+14
| |
* | Added definition of PLoadRRR and PStoreRRR - no Asmblockgen generation yetCyril SIX2019-04-021-14/+34
|/
* Preuve de Jumptable dans Asmblockdeps.vCyril SIX2019-03-291-1/+9
|
* Merge remote-tracking branch 'origin/mppa_vliw_essai_sylvain' into mppa_postpassDavid Monniaux2019-03-281-2/+4
|
generated by cgit (git 2.34.1) at 2024-07-12 08:24:36 +0000