aboutsummaryrefslogtreecommitdiffstats
path: root/scheduling/RTLpathSE_impl.v
Commit message (Collapse)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 ↵Léo Gourdin2021-02-231-2/+52
| |\ | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into riscv-work-rules
| | * 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
| | | | | | | | bugfix in the expansion liveness modification
* | 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-07-04 10:30:24 +0000