From d815eadb7027e11fb042cdef25c3952f3a947b64 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 24 Oct 2021 19:59:22 +0100 Subject: Fix if-conversion and translation with Plit --- src/hls/HTLPargen.v | 4 ++-- src/hls/IfConversion.v | 6 +++--- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v index e8b18dc..6058f62 100644 --- a/src/hls/HTLPargen.v +++ b/src/hls/HTLPargen.v @@ -658,7 +658,7 @@ Definition add_control_instr_force (n : node) (st : stmnt) : mon unit := Fixpoint pred_expr (preg: reg) (p: pred_op) := match p with - | Pvar (b, pred) => + | Plit (b, pred) => if b then Vrange preg (Vlit (posToValue pred)) (Vlit (posToValue pred)) else Vunop Vnot (Vrange preg (Vlit (posToValue pred)) (Vlit (posToValue pred))) @@ -696,7 +696,7 @@ Definition translate_inst a (fin rtrn stack preg : reg) (n : node) (i : instr) translate_predicate a preg p dst (Vvar src) | RBsetpred c args p => do cond <- translate_condition c args; - ret (a (pred_expr preg (Pvar (true, p))) cond) + ret (a (pred_expr preg (Plit (true, p))) cond) end. Lemma create_new_state_state_incr: diff --git a/src/hls/IfConversion.v b/src/hls/IfConversion.v index 205506c..67bd2a8 100644 --- a/src/hls/IfConversion.v +++ b/src/hls/IfConversion.v @@ -58,10 +58,10 @@ Definition if_convert_block (c: code) (p: predicate) (bb: bblock) : bblock := | RBcond cond args n1 n2 => match PTree.get n1 c, PTree.get n2 c with | Some bb1, Some bb2 => - let bb1' := List.map (map_if_convert (Pvar (true, p))) bb1.(bb_body) in - let bb2' := List.map (map_if_convert (Pvar (false, p))) bb2.(bb_body) in + let bb1' := List.map (map_if_convert (Plit (true, p))) bb1.(bb_body) in + let bb2' := List.map (map_if_convert (Plit (false, p))) bb2.(bb_body) in mk_bblock (List.concat (bb.(bb_body) :: ((RBsetpred cond args p) :: bb1') :: bb2' :: nil)) - (RBpred_cf (Pvar (true, p)) bb1.(bb_exit) bb2.(bb_exit)) + (RBpred_cf (Plit (true, p)) bb1.(bb_exit) bb2.(bb_exit)) | _, _ => bb end | _ => bb -- cgit