Fix state generation for if-conversion

4 files changed, 21 insertions, 14 deletions

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) :=