aboutsummaryrefslogtreecommitdiffstats
path: root/scheduling
Commit message (Expand)AuthorAgeFilesLines
* Merge branch 'riscv-work-rules' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy...Léo Gourdin2021-02-231-2/+52
|\
| * add target_cbranch_expanseSylvain Boulmé2021-02-231-2/+52
* | Separate target_op_simplify for riscVLéo Gourdin2021-02-231-19/+2
|/
* fix commentsSylvain Boulmé2021-02-231-2/+5
* starting an interface for target rewriting rules.Sylvain Boulmé2021-02-231-9/+130
* improved pre_output_regsSylvain Boulmé2021-02-221-5/+8
* a bit more cleaningSylvain Boulmé2021-02-225-44/+21
* quick fixcommentsLéo Gourdin2021-02-161-4/+1
* This commit gives a first try to compute pre_output_regs from the livenesss o...Léo Gourdin2021-02-151-10/+19
* [Broken version] Some TODO eliminatedLéo Gourdin2021-02-153-153/+15
* [Broken version] Proof of hsistate_simu_spec_correctLéo Gourdin2021-02-151-7/+10
* [Broken version] Intermediate local commit: pre_output_regs_correct provedLéo Gourdin2021-02-151-17/+28
* [Broken version] Intermediate local commit: proof of siexec_snone_por in sche...Léo Gourdin2021-02-122-18/+68
* [Broken version] Intermediate local commit: proof of inst_checker_eqlive OKLéo Gourdin2021-02-122-54/+131
* progress in pre_output_regs_correctSylvain Boulmé2021-02-121-5/+53
* improve the skeleton...Sylvain Boulmé2021-02-112-26/+107
* refactorize inst_checker for checking pre_output_regsSylvain Boulmé2021-02-112-31/+98
* specification of pre_output_regs for the simulation checkerSylvain Boulmé2021-02-116-125/+107
* factorize lazy_and_Some_* lemmasSylvain Boulmé2021-02-101-16/+3
* Checker for wellformed pathLéo Gourdin2021-02-081-2/+175
* intro RTLpathWFcheckSylvain Boulmé2021-02-082-4/+32
* Some comment clean on RTLpathCyril SIX2021-01-191-3/+2
* Merge branch 'kvx-work' into aarch64-peepholeSylvain Boulmé2021-01-072-169/+102
|\
| * Uniformizing a couple of debug print functionsCyril SIX2020-12-172-87/+28
| * Fixing too many loads being NOTRAPCyril SIX2020-12-171-3/+9
| * Flushing at each dprintfCyril SIX2020-12-161-1/+3
| * Partially fixing turning loads into non trapCyril SIX2020-12-161-22/+56
| * CleanupCyril SIX2020-12-161-83/+0
| * Turning loads into non-trapping when necessaryCyril SIX2020-12-151-1/+34
* | Val_cmp* -> Val.mxcmp*Sylvain Boulmé2021-01-071-21/+6
* | directory postpass_libSylvain Boulmé2021-01-075-0/+0
* | recreate abstractbb/Sylvain Boulmé2021-01-074-0/+0
* | cleaningSylvain Boulmé2021-01-072-1440/+0
* | Merge branch 'kvx-work' into aarch64-peepholeSylvain Boulmé2020-12-174-25/+28
|\|
* | Merge branch 'kvx-test-prepass' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy...David Monniaux2020-11-2711-0/+6216
|/
* prepass scheduling proof finished !Sylvain Boulmé2020-11-201-24/+56
* seval_builtin_sval_preservedDavid Monniaux2020-11-171-1/+4
* a little lemma on list of builtinsDavid Monniaux2020-11-171-2/+15
* there remains two tricky casesDavid Monniaux2020-11-161-3/+14
* disable debug printing in schedulerDavid Monniaux2020-11-041-4/+4
* simplify HSop (and merge hSop and hSop_Sinit)Sylvain Boulmé2020-10-172-42/+23
* fixing the move of the verified prepass scheduler into scheduling/ directorySylvain Boulmé2020-10-172-758/+872
* Merge remote-tracking branch 'origin/kvx-test-prepass' into mppa-RTLpathSE-verifCyril SIX2020-10-166-1458/+1452
* pour ARMDavid Monniaux2020-10-021-4/+4
* so that all architectures compileDavid Monniaux2020-10-021-473/+0
* attempt at separating the divisionsDavid Monniaux2020-09-291-1/+13
* attempt at "zigzag" scheduler; not quite testable due to issues in the duplic...David Monniaux2020-09-242-1/+36
* fix issue 210 in simu_checkSylvain Boulmé2020-09-211-11/+23
* more debug info for simu_checkSylvain Boulmé2020-09-211-6/+16
* just missing OpWeights for AARCH64David Monniaux2020-09-1614-0/+9446
generated by cgit (git 2.34.1) at 2024-07-12 03:18:58 +0000