aboutsummaryrefslogtreecommitdiffstats
path: root/scheduling/RTLpathSE_impl.v
Commit message (Expand)AuthorAgeFilesLines
* Adding a mini CSE pass in the expansion oracleLéo Gourdin2021-03-061-1/+1
* Proofs finished for expansionLéo Gourdin2021-03-011-22/+6
* Debugging fake values finishedLéo Gourdin2021-03-011-10/+19
* proof of fsval_proj_correctSylvain Boulmé2021-03-011-7/+27
* Merge remote-tracking branch 'origin/riscv-work-rules' into riscv-workLéo Gourdin2021-03-011-4/+4
|\
| * bug fix ?Sylvain Boulmé2021-03-011-4/+4
* | Proof of fsval condition cmp okLéo Gourdin2021-03-011-968/+18
* | [Admitted checker] Some more proof, version with buggy addirw0Léo Gourdin2021-02-251-18/+2
* | some more proof for fake hsval checker expansionsLéo Gourdin2021-02-251-324/+1
* | [Intermediate] Adding fake hsval for Ccomp expansionLéo Gourdin2021-02-231-164/+7
* | Fix importsLéo Gourdin2021-02-231-1/+1
* | Merge remote-tracking branch 'origin/riscv-work-rules' into riscv-workLéo Gourdin2021-02-231-27/+173
|\|
| * 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
| * a bit more cleaningSylvain Boulmé2021-02-221-1/+1
* | others case for ccompimmLéo Gourdin2021-02-231-53/+51
* | Some more proofs on branch expansion, using make_immed32_soundLéo Gourdin2021-02-231-59/+221
* | Branch expansions activated and configured in the checker (but admitted) and ...Léo Gourdin2021-02-191-49/+146
* | Proof of Ocmp expansions without immediate and some drafts in commentLéo Gourdin2021-02-181-46/+471
* | Merge remote-tracking branch 'origin/CompCert_RTLpath_simuX' into riscv-workLéo Gourdin2021-02-161-30/+16
|\|
| * specification of pre_output_regs for the simulation checkerSylvain Boulmé2021-02-111-30/+16
* | [Admitted checker] Some more proof draftLéo Gourdin2021-02-111-97/+272
* | [Admitted checker] Duplicating Asm Ceq/Cne and draft checker proofLéo Gourdin2021-02-111-55/+320
* | [Admitted checker] Adding cbranch expansions (without scratch) to the checkerLéo Gourdin2021-02-101-3/+93
* | [Admitted checker] Checker expansion for reg Ocmp (without scratch)Léo Gourdin2021-02-101-17/+261
|/
* simplify HSop (and merge hSop and hSop_Sinit)Sylvain Boulmé2020-10-171-40/+20
* Merge remote-tracking branch 'origin/kvx-test-prepass' into mppa-RTLpathSE-verifCyril SIX2020-10-161-1380/+1278
* just missing OpWeights for AARCH64David Monniaux2020-09-161-0/+1631
generated by cgit (git 2.34.1) at 2024-06-02 17:54:41 +0000