aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c
Commit message (Expand)AuthorAgeFilesLines
* merge VLIW proofsDavid Monniaux2019-03-287-23/+1073
|\
| * 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
* | | | improvements on cmoved etc.David Monniaux2019-03-272-93/+7
* | | | match some 'and'David Monniaux2019-03-272-10/+34
* | | | selectl generationDavid Monniaux2019-03-266-14/+205
* | | | ternary unsignedDavid Monniaux2019-03-262-0/+47
* | | | rm cruftDavid Monniaux2019-03-262-167/+9
* | | | cmoved worksDavid Monniaux2019-03-261-4/+5
* | | | ternary / cmove demo now worksDavid Monniaux2019-03-261-2/+2
* | | | ternary begins workingDavid Monniaux2019-03-262-13/+11
* | | | some progressDavid Monniaux2019-03-262-19/+12
* | | | implemented ternary patternDavid Monniaux2019-03-262-1/+57
* | | | more on ternaryDavid Monniaux2019-03-262-6/+149
* | | | select basic operatorsDavid Monniaux2019-03-261-0/+24
* | | | selectlDavid Monniaux2019-03-252-0/+21
* | | | more on cmoveDavid Monniaux2019-03-254-66/+42
* | | | progress on cmoveDavid Monniaux2019-03-255-3/+17
* | | | draft commentDavid Monniaux2019-03-251-0/+3
* | | | some version of select/selectl that runs through ValueAOpDavid Monniaux2019-03-251-5/+32
* | | | NeedOp advancingDavid Monniaux2019-03-251-0/+43
* | | | better Op select/selectlDavid Monniaux2019-03-251-32/+24
* | | | progressing on select/selectlDavid Monniaux2019-03-252-0/+12
* | | | going forward with select/selectlDavid Monniaux2019-03-251-12/+26
* | | | begin ternaryDavid Monniaux2019-03-242-1/+49
|/ / /
* | | 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
generated by cgit (git 2.34.1) at 2024-07-04 00:28:25 +0000