From 8d5047ca436ba42e9253d24d6b5b2c0c62dd7437 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 3 Feb 2021 01:05:32 +0000 Subject: Fix state generation for if-conversion --- src/hls/HTLPargen.v | 9 +++++---- src/hls/IfConversion.v | 12 ++++++------ src/hls/PrintVerilog.ml | 12 +++++++++--- src/hls/RTLBlockInstr.v | 2 +- 4 files changed, 21 insertions(+), 14 deletions(-) (limited to 'src') diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v index 0508e6f..0804b0e 100644 --- a/src/hls/HTLPargen.v +++ b/src/hls/HTLPargen.v @@ -77,7 +77,8 @@ Module HTLState <: State. Definition st_prop := st_incr. Hint Unfold st_prop : htlh. - Lemma st_refl : forall s, st_prop s s. Proof. auto with htlh. Qed. + Lemma st_refl : forall s, st_prop s s. + Proof. auto with htlh. Qed. Lemma st_trans : forall s1 s2 s3, st_prop s1 s2 -> st_prop s2 s3 -> st_prop s1 s3. @@ -552,7 +553,7 @@ Definition poslength {A : Type} (l : list A) : positive := Fixpoint penumerate {A : Type} (p : positive) (l : list A) {struct l} : list (positive * A) := match l with - | x :: xs => (p, x) :: penumerate (Pos.succ p) xs + | x :: xs => (p, x) :: penumerate (Pos.pred p) xs | nil => nil end. @@ -669,7 +670,7 @@ Definition translate_inst_list (fin rtrn stack preg: reg) (ni : node * list inst let (n, li) := ni in do _ <- collectlist (translate_inst fin rtrn stack preg n) li; do st <- get; - add_control_instr n (state_goto st.(st_st) (Pos.succ n)). + add_control_instr n (state_goto st.(st_st) (Pos.pred n)). Fixpoint translate_cfi' (fin rtrn stack preg: reg) (cfi: cf_instr) : mon (stmnt * stmnt) := @@ -717,7 +718,7 @@ Definition transf_bblock (fin rtrn stack preg: reg) (ni : node * bblock) do _ <- collectlist (translate_inst_list fin rtrn stack preg) (penumerate n bb.(bb_body)); translate_cfi fin rtrn stack preg - ((n + poslength bb.(bb_body))%positive, bb.(bb_exit)). + ((n - poslength bb.(bb_body))%positive, bb.(bb_exit)). Definition transf_module (f: function) : mon HTL.module := if stack_correct f.(fn_stacksize) then diff --git a/src/hls/IfConversion.v b/src/hls/IfConversion.v index 9e600af..943e1a8 100644 --- a/src/hls/IfConversion.v +++ b/src/hls/IfConversion.v @@ -51,16 +51,16 @@ Definition map_if_convert (p: pred_op) (i: instr) := | _ => i end. -Definition if_convert_block (c: code) (p: pred_op) (bb: bblock) : bblock := +Definition if_convert_block (c: code) (p: predicate) (bb: bblock) : bblock := let cfi := bb_exit bb in match cfi with | 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 p) bb1.(bb_body) in - let bb2' := List.map (map_if_convert (Pnot p)) bb2.(bb_body) in - mk_bblock (List.concat (bb.(bb_body) :: bb1' :: bb2' :: nil)) - (RBpred_cf p bb1.(bb_exit) bb2.(bb_exit)) + let bb1' := List.map (map_if_convert (Pvar p)) bb1.(bb_body) in + let bb2' := List.map (map_if_convert (Pnot (Pvar p))) bb2.(bb_body) in + mk_bblock (List.concat (bb.(bb_body) :: ((RBsetpred cond args p) :: bb1') :: bb2' :: nil)) + (RBpred_cf (Pvar p) bb1.(bb_exit) bb2.(bb_exit)) | _, _ => bb end | _ => bb @@ -81,7 +81,7 @@ Definition find_block_with_cond (c: code) : option (node * bblock) := Definition transf_function (f: function) : function := match find_block_with_cond f.(fn_code) with | Some (n, bb) => - let nbb := if_convert_block f.(fn_code) (Pvar 1%positive) bb in + let nbb := if_convert_block f.(fn_code) 1%positive bb in mkfunction f.(fn_sig) f.(fn_params) f.(fn_stacksize) (PTree.set n nbb f.(fn_code)) f.(fn_entrypoint) | None => f diff --git a/src/hls/PrintVerilog.ml b/src/hls/PrintVerilog.ml index b2633ec..e40b051 100644 --- a/src/hls/PrintVerilog.ml +++ b/src/hls/PrintVerilog.ml @@ -79,6 +79,11 @@ let literal l = then sprintf "(- 32'd%ld)" (Int32.neg l') else sprintf "32'd%ld" l' +let compare_expr es1 es2 = + match es1, es2 with + | (Vlit p1, _), (Vlit p2, _) -> compare (camlint_of_coqint p1) (camlint_of_coqint p2) + | _, _ -> -1 + let rec pprint_expr = function | Vlit l -> literal l | Vvar s -> register s @@ -102,9 +107,10 @@ let rec pprint_stmnt i = indent i; "end\n" ] | Vcase (e, es, d) -> concat [ indent i; "case ("; pprint_expr e; ")\n"; - fold_map pprint_case es; indent (i+1); "default:;\n"; - indent i; "endcase\n" - ] + fold_map pprint_case (List.sort compare_expr es |> List.rev); + indent (i+1); "default:;\n"; + indent i; "endcase\n" + ] | Vblock (a, b) -> concat [indent i; pprint_expr a; " = "; pprint_expr b; ";\n"] | Vnonblock (a, b) -> concat [indent i; pprint_expr a; " <= "; pprint_expr b; ";\n"] diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v index 4d02998..345e73e 100644 --- a/src/hls/RTLBlockInstr.v +++ b/src/hls/RTLBlockInstr.v @@ -79,7 +79,7 @@ Definition max_reg_instr (m: positive) (i: instr) := | RBstore p chunk addr args src => fold_left Pos.max args (Pos.max src m) | RBsetpred c args p => - fold_left Pos.max args 1%positive + fold_left Pos.max args m end. Fixpoint max_reg_cfi (m : positive) (i : cf_instr) := -- cgit