From 4e3269bade36d2c2309a49c09b39c848689c28c0 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 3 Jul 2022 22:49:44 +0100 Subject: Add work on scheduling --- src/hls/GiblePargen.v | 46 +++++++++++++++++++++++----------------------- 1 file changed, 23 insertions(+), 23 deletions(-) (limited to 'src/hls/GiblePargen.v') diff --git a/src/hls/GiblePargen.v b/src/hls/GiblePargen.v index 778e0cd..da0567b 100644 --- a/src/hls/GiblePargen.v +++ b/src/hls/GiblePargen.v @@ -167,8 +167,6 @@ This is done by multiplying the predicates together, and assigning the negation of the expression to the other predicates. |*) -Definition forest_state : Type := forest * list (cf_instr * option pred_op * forest). - Definition upd_pred_forest (p: option pred_op) (f: forest) := match p with | Some p' => @@ -180,39 +178,42 @@ Definition upd_pred_forest (p: option pred_op) (f: forest) := | None => f end. -Definition update (flist : forest_state) (i : instr): forest_state := - let (f, fl) := flist in +Definition update (fop : option pred_op * forest) (i : instr): (option pred_op * forest) := + let (pred, f) := fop in match i with - | RBnop => flist + | RBnop => fop | RBop p op rl r => - (f # (Reg r) <- - (app_predicated p - (f # (Reg r)) - (map_predicated (pred_ret (Eop op)) (merge (list_translation rl f)))), fl) + (pred, f # (Reg r) <- + (app_predicated (combine_pred p pred) + (f # (Reg r)) + (map_predicated (pred_ret (Eop op)) (merge (list_translation rl f))))) | RBload p chunk addr rl r => - (f # (Reg r) <- - (app_predicated p + (pred, f # (Reg r) <- + (app_predicated (combine_pred p pred) (f # (Reg r)) (map_predicated (map_predicated (pred_ret (Eload chunk addr)) (merge (list_translation rl f))) - (f # Mem))), fl) + (f # Mem)))) | RBstore p chunk addr rl r => - (f # Mem <- - (app_predicated p + (pred, f # Mem <- + (app_predicated (combine_pred p pred) (f # Mem) (map_predicated (map_predicated (predicated_apply2 (map_predicated (pred_ret Estore) (f # (Reg r))) chunk addr) - (merge (list_translation rl f))) (f # Mem))), fl) + (merge (list_translation rl f))) (f # Mem)))) | RBsetpred p' c args p => - (f # (Pred p) <- - (app_predicated p' + (pred, f # (Pred p) <- + (app_predicated (combine_pred p' pred) (f # (Pred p)) (map_predicated (pred_ret (Esetpred c)) - (merge (list_translation args f)))), fl) - | RBexit p c => ((upd_pred_forest (option_map negate p) f), (c, p, upd_pred_forest p f) :: fl) + (merge (list_translation args f))))) + | RBexit p c => + (combine_pred (Option.map negate p) pred, + f # Exit <- + (app_predicated (combine_pred p pred) (f # Exit) (pred_ret (Eexit c)))) end. (*| @@ -223,7 +224,7 @@ code than in the RTLBlock code. Get a sequence from the basic block. |*) -Fixpoint abstract_sequence (f : forest_state) (b : list instr) : forest_state := +Fixpoint abstract_sequence (f : option pred_op * forest) (b : list instr) : option pred_op * forest := match b with | nil => f | i :: l => abstract_sequence (update f i) l @@ -254,9 +255,8 @@ Definition empty_trees (bb: SeqBB.t) (bbt: ParBB.t) : bool := end. Definition schedule_oracle (bb: SeqBB.t) (bbt: ParBB.t) : bool := - forallb (fun x => match x with ((_, _, f1), (_, _, f2)) => check f1 f2 end) - (combine (snd (abstract_sequence (empty, nil) bb)) - (snd (abstract_sequence (empty, nil) (concat (concat bbt))))) && + (check (snd (abstract_sequence (None, empty) bb)) + (snd (abstract_sequence (None, empty) (concat (concat bbt))))) && empty_trees bb bbt. Definition check_scheduled_trees := beq2 schedule_oracle. -- cgit