aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* add some INLINE markersDavid Monniaux2019-03-281-36/+38
* picosat now uses the same Makefile system as the restDavid Monniaux2019-03-283-3/+49
* merge proof of VLIWDavid Monniaux2019-03-288-24/+1074
|\
| * Merge remote-tracking branch 'origin/mppa_vliw_essai_sylvain' into mppa_postpassDavid Monniaux2019-03-2810-75/+1072
| |\
| | * 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-204-17/+30
| | * 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
| * | check that gcc and ccomp compiled k1c code return the sameDavid Monniaux2019-03-221-2/+6
| * | improved testingDavid Monniaux2019-03-221-5/+16
| * | uses yarpgen random generatorDavid Monniaux2019-03-221-0/+37
| * | FIX BUG in TargetPrinter (nandd immediate wrongly printed as andd)David Monniaux2019-03-221-1/+1
* | | some more ternaryDavid Monniaux2019-03-241-6/+6
* | | experiments with ternary operatorDavid Monniaux2019-03-241-1/+6
* | | experiments with ternaryDavid Monniaux2019-03-244-1526/+36
* | | another ternary implementationDavid Monniaux2019-03-241-1/+7
* | | demo ternary opDavid Monniaux2019-03-242-0/+49
* | | mysteriously slow codeDavid Monniaux2019-03-242-0/+70
* | | encore un essai de creduceDavid Monniaux2019-03-233-0/+1561
* | | system for comparing speedsDavid Monniaux2019-03-231-0/+12
* | | bitsliced AES in one fileDavid Monniaux2019-03-231-10/+85
* | | Test in one file only.David Monniaux2019-03-231-0/+1467
* | | for testing with questDavid Monniaux2019-03-221-0/+24
* | | passage de structures en varargs (fonctionne avec une convention "passage par...David Monniaux2019-03-221-0/+3
* | | Merge branch 'mppa-mul' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCer...David Monniaux2019-03-223-2/+54
|\ \ \
| * | | check that gcc and ccomp compiled k1c code return the sameDavid Monniaux2019-03-221-2/+6
| * | | FIX BUG in TargetPrinter (nandd immediate wrongly printed as andd)David Monniaux2019-03-221-1/+1
| * | | improved testingDavid Monniaux2019-03-221-5/+16
| * | | some more testingDavid Monniaux2019-03-221-1/+1
| * | | uses yarpgen random generatorDavid Monniaux2019-03-221-0/+37
* | | | Merge branch 'mppa-mul' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCer...David Monniaux2019-03-22136-877/+595
|\| | |
| * | | Merge branch 'mppa-mul' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCer...David Monniaux2019-03-2285-17/+259
| |\ \ \
| | * | | Rajout de tests test/mppa pour division/moduloCyril SIX2019-03-226-0/+34
| | * | | Merge branch 'mppa_postpass' into mppa-mulCyril SIX2019-03-2282-30/+238
| | |\| |
| | | * | Reorganized the test/mppa/ tests to have fewer of themCyril SIX2019-03-2282-30/+238
generated by cgit (git 2.34.1) at 2024-07-06 15:27:40 +0000