aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c
Commit message (Expand)AuthorAgeFilesLines
* merge proof of VLIWDavid Monniaux2019-03-287-23/+1073
|\
| * 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
| * | FIX BUG in TargetPrinter (nandd immediate wrongly printed as andd)David Monniaux2019-03-221-1/+1
* | | Merge branch 'mppa-mul' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCer...David Monniaux2019-03-221-1/+1
|\ \ \
| * | | FIX BUG in TargetPrinter (nandd immediate wrongly printed as andd)David Monniaux2019-03-221-1/+1
* | | | Merge branch 'mppa-mul' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCer...David Monniaux2019-03-2213-783/+14
|\| | |
| * | | rm Pdiv / PdivuDavid Monniaux2019-03-226-66/+1
| * | | restructuration pour compilation toute archiDavid Monniaux2019-03-223-1/+5
| * | | ça recompile sur x86David Monniaux2019-03-222-103/+1
| * | | Merge branch 'mppa_postpass' into mppa-mulDavid Monniaux2019-03-223-613/+7
| |\| |
| | * | I think it should now compile for all architectures.David Monniaux2019-03-221-613/+0
| | * | try to be portable across archsDavid Monniaux2019-03-212-0/+7
* | | | rm tests inherited from Risc-VDavid Monniaux2019-03-201-30/+5
|/ / /
* | | Merge branch 'mppa_postpass' into mppa-mulDavid Monniaux2019-03-201-2/+2
|\| |
| * | XLeroy's suggested fix for shared float/int register file.David Monniaux2019-03-201-2/+2
* | | Proof of div32/mod32/divf32/divf64 lemmasCyril SIX2019-03-201-6/+21
* | | la division flottante fonctionneDavid Monniaux2019-03-202-2/+27
* | | begin float divisionDavid Monniaux2019-03-201-0/+4
* | | Merge branch 'mppa-mul' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCer...David Monniaux2019-03-201-6/+47
|\ \ \
| * | | Proving eval_divs_baseCyril SIX2019-03-201-6/+47
* | | | les divisions entieres passentDavid Monniaux2019-03-202-9/+11
* | | | Merge branch 'mppa_postpass' into mppa-mulDavid Monniaux2019-03-2020-1449/+461
|\ \ \ \ | |/ / / |/| / / | |/ /
| * | Merge branch 'mppa-madd' into mppa_postpassDavid Monniaux2019-03-207-20/+65
| |\ \
| | * | maddl / maddlim are synthesized (but not for pointers it seems)David Monniaux2019-03-203-1/+13
| | * | maddl gets to assemblyDavid Monniaux2019-03-201-2/+0
| | * | maddl declaredDavid Monniaux2019-03-203-17/+52
| * | | Merge branch 'mppa-madd' into mppa_postpassDavid Monniaux2019-03-1914-1357/+307
| |\| |
| | * | mul+madd immediateDavid Monniaux2019-03-194-3/+28
| | * | mul immediateDavid Monniaux2019-03-196-3/+18
| | * | mul immediate beginDavid Monniaux2019-03-198-4/+28
| | * | fix classes for maddDavid Monniaux2019-03-191-4/+4
generated by cgit (git 2.34.1) at 2024-07-04 01:50:32 +0000