aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c
Commit message (Expand)AuthorAgeFilesLines
...
| | * 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
| |\ \ | | |/ | |/|
| | * No more AdmittedCyril SIX2019-03-291-55/+102
| * | Avancement dans la preuve du MBjumptableCyril SIX2019-03-291-1/+21
| * | FIX BUG in TargetPrinter (nandd immediate wrongly printed as andd)David Monniaux2019-03-221-1/+1
| * | Merge branch 'mppa-mul' into mppa-jumptableDavid Monniaux2019-03-2214-719/+123
| |\ \
| * | | Jump tables now work. There is still an "Admitted" subcase in a proof.David Monniaux2019-03-223-5/+15
| * | | on avance sur la jumptableDavid Monniaux2019-03-222-3/+3
| * | | jumptable avanceDavid Monniaux2019-03-221-1/+8
| * | | Fixed proof of Asmblockdeps wrt PjumptableCyril SIX2019-03-221-25/+28
| * | | begin jumptables (does not work)David Monniaux2019-03-214-3/+57
* | | | 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
generated by cgit (git 2.34.1) at 2024-07-06 16:28:50 +0000