Add predicated values and instructions

7 files changed, 92 insertions, 41 deletions

diff --git a/src/Compiler.v b/src/Compiler.v
index 2406dad..27cb80c 100644
--- a/src/Compiler.v
+++ b/src/Compiler.v
@@ -67,6 +67,7 @@ Require vericert.hls.RTLBlockgen.
 Require vericert.hls.RTLPargen.
 Require vericert.hls.HTLPargen.
 Require vericert.hls.Pipeline.
+Require vericert.hls.IfConversion.
 
 Require Import vericert.hls.HTLgenproof.
 
@@ -79,7 +80,7 @@ We then need to declare the external OCaml functions used to print out intermedi
 
 Parameter print_RTL: Z -> RTL.program -> unit.
 Parameter print_HTL: HTL.program -> unit.
-Parameter print_RTLBlock: RTLBlock.program -> unit.
+Parameter print_RTLBlock: Z -> RTLBlock.program -> unit.
 
 Definition print {A: Type} (printer: A -> unit) (prog: A) : A :=
   let unused := printer prog in prog.
@@ -233,7 +234,9 @@ Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program :=
   @@@ time "Unused globals" Unusedglob.transform_program
    @@ print (print_RTL 7)
   @@@ RTLBlockgen.transl_program
-   @@ print print_RTLBlock
+   @@ print (print_RTLBlock 1)
+   @@ IfConversion.transf_program
+   @@ print (print_RTLBlock 2)
   @@@ RTLPargen.transl_program
   @@@ HTLPargen.transl_program
    @@ print print_HTL
diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v
index 21f16b9..0508e6f 100644
--- a/src/hls/HTLPargen.v
+++ b/src/hls/HTLPargen.v
@@ -621,10 +621,19 @@ Definition add_control_instr (n : node) (st : stmnt) : mon unit :=
       Error (Errors.msg "HTLPargen.add_control_instr: control logic is not empty")
     end.
 
-Definition pred_expr (preg: reg) (p: predicate) :=
-  Vrange preg (Vlit (posToValue p)) (Vlit (posToValue p)).
+Fixpoint pred_expr (preg: reg) (p: pred_op) :=
+  match p with
+  | Pvar pred =>
+    Vrange preg (Vlit (posToValue pred)) (Vlit (posToValue pred))
+  | Pnot pred =>
+    Vunop Vnot (pred_expr preg pred)
+  | Pand p1 p2 =>
+    Vbinop Vand (pred_expr preg p1) (pred_expr preg p2)
+  | Por p1 p2 =>
+    Vbinop Vor (pred_expr preg p1) (pred_expr preg p2)
+  end.
 
-Definition translate_predicate (preg: reg) (p: option predicate) (dst e: expr) :=
+Definition translate_predicate (preg: reg) (p: option pred_op) (dst e: expr) :=
   match p with
   | None => ret (Vnonblock dst e)
   | Some pos =>
@@ -652,7 +661,7 @@ Definition translate_inst (fin rtrn stack preg : reg) (n : node) (i : instr)
     add_data_instr n pred
   | RBsetpred c args p =>
     do cond <- translate_condition c args;
-    add_data_instr n (Vnonblock (pred_expr preg p) cond)
+    add_data_instr n (Vnonblock (pred_expr preg (Pvar p)) cond)
   end.
 
 Definition translate_inst_list (fin rtrn stack preg: reg) (ni : node * list instr)
@@ -662,25 +671,29 @@ Definition translate_inst_list (fin rtrn stack preg: reg) (ni : node * list inst
   do st <- get;
   add_control_instr n (state_goto st.(st_st) (Pos.succ n)).
 
-Definition translate_cfi (fin rtrn stack: reg) (ni : node * cf_instr)
-  : mon unit :=
-  let (n, cfi) := ni in
+Fixpoint translate_cfi' (fin rtrn stack preg: reg) (cfi: cf_instr)
+  : mon (stmnt * stmnt) :=
   match cfi with
   | RBgoto n' =>
     do st <- get;
-    add_node_skip n (state_goto st.(st_st) n')
+    ret (Vskip, state_goto st.(st_st) n')
   | RBcond c args n1 n2 =>
+    do st <- get;
     do e <- translate_condition c args;
-    add_branch_instr e n n1 n2
+    ret (Vskip, state_cond st.(st_st) e n1 n2)
   | RBreturn r =>
     match r with
     | Some r' =>
-      add_instr_skip n (Vseq (block fin (Vlit (ZToValue 1%Z)))
-                             (block rtrn (Vvar r')))
+      ret ((Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vvar r'))),
+           Vskip)
     | None =>
-      add_instr_skip n (Vseq (block fin (Vlit (ZToValue 1%Z)))
-                             (block rtrn (Vlit (ZToValue 0%Z))))
+      ret ((Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vlit (ZToValue 0%Z)))),
+           Vskip)
     end
+  | RBpred_cf p c1 c2 =>
+    do (tc1s, tc1c) <- translate_cfi' fin rtrn stack preg c1;
+    do (tc2s, tc2c) <- translate_cfi' fin rtrn stack preg c2;
+    ret ((Vcond (pred_expr preg p) tc1s tc2s), (Vcond (pred_expr preg p) tc1c tc2c))
   | RBjumptable r ln =>
     error (Errors.msg "HTLPargen: RPjumptable not supported.")
   | RBcall sig ri rl r n =>
@@ -691,12 +704,19 @@ Definition translate_cfi (fin rtrn stack: reg) (ni : node * cf_instr)
     error (Errors.msg "HTLPargen: RPbuildin not supported.")
   end.
 
+Definition translate_cfi (fin rtrn stack preg: reg) (ni: node * cf_instr)
+  : mon unit :=
+  let (n, cfi) := ni in
+  do (s, c) <- translate_cfi' fin rtrn stack preg cfi;
+  do _ <- add_control_instr n c;
+  add_data_instr n s.
+
 Definition transf_bblock (fin rtrn stack preg: reg) (ni : node * bblock)
   : mon unit :=
   let (n, bb) := ni in
   do _ <- collectlist (translate_inst_list fin rtrn stack preg)
                       (penumerate n bb.(bb_body));
-  translate_cfi fin rtrn stack
+  translate_cfi fin rtrn stack preg
                 ((n + poslength bb.(bb_body))%positive, bb.(bb_exit)).
 
 Definition transf_module (f: function) : mon HTL.module :=
diff --git a/src/hls/PrintRTLBlock.ml b/src/hls/PrintRTLBlock.ml
index caf64ff..8fef401 100644
--- a/src/hls/PrintRTLBlock.ml
+++ b/src/hls/PrintRTLBlock.ml
@@ -63,10 +63,10 @@ let print_program pp (prog: program) =
 
 let destination : string option ref = ref None
 
-let print_if prog =
+let print_if passno prog =
   match !destination with
   | None -> ()
   | Some f ->
-     let oc = open_out f in
+     let oc = open_out (f ^ "." ^ Z.to_string passno) in
      print_program oc prog;
      close_out oc
diff --git a/src/hls/PrintRTLBlockInstr.ml b/src/hls/PrintRTLBlockInstr.ml
index a943aab..979ca38 100644
--- a/src/hls/PrintRTLBlockInstr.ml
+++ b/src/hls/PrintRTLBlockInstr.ml
@@ -9,6 +9,9 @@ open PrintAST
 let reg pp r =
   fprintf pp "x%d" (P.to_int r)
 
+let pred pp r =
+  fprintf pp "p%d" (P.to_int r)
+
 let rec regs pp = function
   | [] -> ()
   | [r] -> reg pp r
@@ -18,24 +21,39 @@ let ros pp = function
   | Coq_inl r -> reg pp r
   | Coq_inr s -> fprintf pp "\"%s\"" (extern_atom s)
 
+let rec print_pred_op pp = function
+  | Pvar p -> pred pp p
+  | Pnot p -> fprintf pp "(~ %a)" print_pred_op p
+  | Pand (p1, p2) -> fprintf pp "(%a & %a)" print_pred_op p1 print_pred_op p2
+  | Por (p1, p2) -> fprintf pp "(%a | %a)" print_pred_op p1 print_pred_op p2
+
+let print_pred_option pp = function
+  | Some x -> fprintf pp "(%a)" print_pred_op x
+  | None -> ()
+
 let print_bblock_body pp i =
   fprintf pp "\t\t";
   match i with
   | RBnop -> fprintf pp "nop\n"
-  | RBop(_, op, ls, dst) ->
-     fprintf pp "%a = %a\n"
-       reg dst (PrintOp.print_operation reg) (op, ls)
-  | RBload(_, chunk, addr, args, dst) ->
-     fprintf pp "%a = %s[%a]\n"
-       reg dst (name_of_chunk chunk)
+  | RBop(p, op, ls, dst) ->
+     fprintf pp "%a %a = %a\n"
+       print_pred_option p reg dst (PrintOp.print_operation reg) (op, ls)
+  | RBload(p, chunk, addr, args, dst) ->
+     fprintf pp "%a %a = %s[%a]\n"
+       print_pred_option p reg dst (name_of_chunk chunk)
        (PrintOp.print_addressing reg) (addr, args)
-  | RBstore(_, chunk, addr, args, src) ->
-     fprintf pp "%s[%a] = %a\n"
+  | RBstore(p, chunk, addr, args, src) ->
+     fprintf pp "%a %s[%a] = %a\n"
+       print_pred_option p
        (name_of_chunk chunk)
        (PrintOp.print_addressing reg) (addr, args)
        reg src
+  | RBsetpred (c, args, p) ->
+    fprintf pp "%a = %a\n"
+      pred p
+      (PrintOp.print_condition reg) (c, args)
 
-let print_bblock_exit pp i =
+let rec print_bblock_exit pp i =
   fprintf pp "\t\t";
   match i with
   | RBcall(_, fn, args, res, _) ->
@@ -65,3 +83,5 @@ let print_bblock_exit pp i =
       fprintf pp "return %a\n" reg arg
   | RBgoto n ->
      fprintf pp "goto %d\n" (P.to_int n)
+  | RBpred_cf (p, c1, c2) ->
+    fprintf pp "if %a then (%a) else (%a)\n" print_pred_op p print_bblock_exit c1 print_bblock_exit c2
diff --git a/src/hls/PrintVerilog.ml b/src/hls/PrintVerilog.ml
index 4a6c165..b2633ec 100644
--- a/src/hls/PrintVerilog.ml
+++ b/src/hls/PrintVerilog.ml
@@ -87,6 +87,7 @@ let rec pprint_expr = function
   | Vunop (u, e) -> concat ["("; unop u; pprint_expr e; ")"]
   | Vbinop (op, a, b) -> concat [pprint_binop (pprint_expr a) (pprint_expr b) op]
   | Vternary (c, t, f) -> concat ["("; pprint_expr c; " ? "; pprint_expr t; " : "; pprint_expr f; ")"]
+  | Vrange (r, e1, e2) -> concat [register r; "["; pprint_expr e1; ":"; pprint_expr e2; "]"]
 
 let rec pprint_stmnt i =
   let pprint_case (e, s) = concat [ indent (i + 1); pprint_expr e; ": begin\n"; pprint_stmnt (i + 2) s;
diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v
index c480d36..4d02998 100644
--- a/src/hls/RTLBlockInstr.v
+++ b/src/hls/RTLBlockInstr.v
@@ -33,11 +33,17 @@ Local Open Scope rtl.
 Definition node := positive.
 Definition predicate := positive.
 
+Inductive pred_op : Type :=
+| Pvar: predicate -> pred_op
+| Pnot: pred_op -> pred_op
+| Pand: pred_op -> pred_op -> pred_op
+| Por: pred_op -> pred_op -> pred_op.
+
 Inductive instr : Type :=
 | RBnop : instr
-| RBop : option predicate -> operation -> list reg -> reg -> instr
-| RBload : option predicate -> memory_chunk -> addressing -> list reg -> reg -> instr
-| RBstore : option predicate -> memory_chunk -> addressing -> list reg -> reg -> instr
+| RBop : option pred_op -> operation -> list reg -> reg -> instr
+| RBload : option pred_op -> memory_chunk -> addressing -> list reg -> reg -> instr
+| RBstore : option pred_op -> memory_chunk -> addressing -> list reg -> reg -> instr
 | RBsetpred : condition -> list reg -> predicate -> instr.
 
 Inductive cf_instr : Type :=
@@ -48,9 +54,10 @@ Inductive cf_instr : Type :=
 | RBcond : condition -> list reg -> node -> node -> cf_instr
 | RBjumptable : reg -> list node -> cf_instr
 | RBreturn : option reg -> cf_instr
-| RBgoto : node -> cf_instr.
+| RBgoto : node -> cf_instr
+| RBpred_cf : pred_op -> cf_instr -> cf_instr -> cf_instr.
 
-Definition successors_instr (i : cf_instr) : list node :=
+Fixpoint successors_instr (i : cf_instr) : list node :=
   match i with
   | RBcall sig ros args res s => s :: nil
   | RBtailcall sig ros args => nil
@@ -59,6 +66,7 @@ Definition successors_instr (i : cf_instr) : list node :=
   | RBjumptable arg tbl => tbl
   | RBreturn optarg => nil
   | RBgoto n => n :: nil
+  | RBpred_cf p c1 c2 => concat (successors_instr c1 :: successors_instr c2 :: nil)
   end.
 
 Definition max_reg_instr (m: positive) (i: instr) :=
@@ -74,7 +82,7 @@ Definition max_reg_instr (m: positive) (i: instr) :=
     fold_left Pos.max args 1%positive
   end.
 
-Definition max_reg_cfi (m : positive) (i : cf_instr) :=
+Fixpoint max_reg_cfi (m : positive) (i : cf_instr) :=
   match i with
   | RBcall sig (inl r) args res s =>
     fold_left Pos.max args (Pos.max r (Pos.max res m))
@@ -92,6 +100,7 @@ Definition max_reg_cfi (m : positive) (i : cf_instr) :=
   | RBreturn None => m
   | RBreturn (Some arg) => Pos.max arg m
   | RBgoto n => m
+  | RBpred_cf p c1 c2 => Pos.max (max_reg_cfi m c1) (max_reg_cfi m c2)
   end.
 
 Definition regset := Regmap.t val.
diff --git a/src/hls/Schedule.ml b/src/hls/Schedule.ml
index 128f0e1..ec130cb 100644
--- a/src/hls/Schedule.ml
+++ b/src/hls/Schedule.ml
@@ -279,8 +279,8 @@ let print_src_type i c =
 let print_data_dep_order c (i, j) =
   print_lt0 (gen_var_name_e i c) (gen_var_name_b j c)
 
-let rec gather_cfg_constraints (completed, (bvars, constraints, types)) c curr =
-  if List.exists (fun x -> P.eq x curr) completed then
+let gather_cfg_constraints (completed, (bvars, constraints, types)) c curr =
+  if List.exists (P.eq curr) completed then
     (completed, (bvars, constraints, types))
   else
     match PTree.get curr c with
@@ -309,11 +309,7 @@ let rec gather_cfg_constraints (completed, (bvars, constraints, types)) c curr =
                (List.init num_iters (fun x -> x)))
             bvars
         in
-        let next' = List.filter (fun x -> P.lt x curr) next in
-        List.fold_left
-          (fun compl curr' -> gather_cfg_constraints compl c curr')
-          (curr :: completed, (bvars', constraints', types'))
-          next'
+        (curr :: completed, (bvars', constraints', types'))
 
 let rec intersperse s = function
   | [] -> []
@@ -415,7 +411,9 @@ let schedule entry (c : RTLBlock.bb RTLBlockInstr.code) =
   let c' = PTree.map1 (gather_bb_constraints false) c in
   let _ = if debug then PTree.map (fun r o -> printf "##### %d #####\n%a\n\n" (P.to_int r) print_dfg (second o)) c' else PTree.empty in
   let _, (vars, constraints, types) =
-    gather_cfg_constraints ([], ([], "", "")) c' entry
+    List.map fst (PTree.elements c') |>
+    List.fold_left (fun compl ->
+        gather_cfg_constraints compl c') ([], ([], "", ""))
   in
   let schedule' = solve_constraints vars constraints types in
   IMap.iter (fun a b -> printf "##### %d #####\n%a\n\n" a (print_list print_tuple) b) schedule';