diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-12-17 15:43:37 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-12-17 15:43:37 +0100 |
| commit | ff1a4a32676fad3a78aad69d963f9f94bb07615c (patch) | |
| tree | 1be819074805478c2982ffefd44e060d543e2cd4 /mppa_k1c/PostpassScheduling.v | |
| parent | f9de154cde1974a8fa9afec9ad83653384ec912f (diff) | |
| download | compcert-kvx-ff1a4a32676fad3a78aad69d963f9f94bb07615c.tar.gz compcert-kvx-ff1a4a32676fad3a78aad69d963f9f94bb07615c.zip | |
Added a simple postpass oracle that splits a bblock into single instruction bundles
Diffstat (limited to 'mppa_k1c/PostpassScheduling.v')
| -rw-r--r-- | mppa_k1c/PostpassScheduling.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/mppa_k1c/PostpassScheduling.v b/mppa_k1c/PostpassScheduling.v index 5232f903..1483a5d7 100644 --- a/mppa_k1c/PostpassScheduling.v +++ b/mppa_k1c/PostpassScheduling.v @@ -19,6 +19,8 @@ Local Open Scope error_monad_scope. returns a schedule expressed as a list of bundles *) Axiom schedule: bblock -> list bblock. +Extract Constant schedule => "PostpassSchedulingOracle.schedule". + (* TODO - implement the verificator *) Definition verified_schedule (bb : bblock) : res (list bblock) := OK (schedule bb). |