aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c/PostpassScheduling.v
Commit message (Collapse)AuthorAgeFilesLines
* Added a simple postpass oracle that splits a bblock into single instruction ↵Cyril SIX2018-12-171-0/+2
| | | | bundles
* Generalizing PostpassScheduling to include bblock splittingCyril SIX2018-12-051-12/+18
|
* Added definitions and proof sketch for PostpassSchedulingCyril SIX2018-12-041-15/+19
|
* Tout début de développement d'un postpass Asmblock en CoqCyril SIX2018-12-031-0/+38