Add Vrange and predicates

8 files changed, 95 insertions, 66 deletions

diff --git a/src/Compiler.v b/src/Compiler.v
index 0578f57..2406dad 100644
--- a/src/Compiler.v
+++ b/src/Compiler.v
@@ -232,8 +232,6 @@ Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program :=
    @@ print (print_RTL 6)
   @@@ time "Unused globals" Unusedglob.transform_program
    @@ print (print_RTL 7)
-   @@ Pipeline.transf_program
-   @@ print (print_RTL 8)
   @@@ RTLBlockgen.transl_program
    @@ print print_RTLBlock
   @@@ RTLPargen.transl_program
diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v
index 2014c0e..21f16b9 100644
--- a/src/hls/HTLPargen.v
+++ b/src/hls/HTLPargen.v
@@ -40,7 +40,7 @@ Hint Resolve Ple_refl : htlh.
 Hint Resolve Ple_succ : htlh.
 
 Record state: Type := mkstate {
-  st_st : reg;
+  st_st: reg;
   st_freshreg: reg;
   st_freshstate: node;
   st_scldecls: AssocMap.t (option io * scl_decl);
@@ -621,32 +621,48 @@ Definition add_control_instr (n : node) (st : stmnt) : mon unit :=
       Error (Errors.msg "HTLPargen.add_control_instr: control logic is not empty")
     end.
 
-Definition translate_inst (fin rtrn stack : reg) (n : node) (i : instr)
+Definition pred_expr (preg: reg) (p: predicate) :=
+  Vrange preg (Vlit (posToValue p)) (Vlit (posToValue p)).
+
+Definition translate_predicate (preg: reg) (p: option predicate) (dst e: expr) :=
+  match p with
+  | None => ret (Vnonblock dst e)
+  | Some pos =>
+    ret (Vnonblock dst (Vternary (pred_expr preg pos) e dst))
+  end.
+
+Definition translate_inst (fin rtrn stack preg : reg) (n : node) (i : instr)
   : mon unit :=
   match i with
   | RBnop =>
     add_data_instr n Vskip
-  | RBop op args dst =>
+  | RBop p op args dst =>
     do instr <- translate_instr op args;
     do _ <- declare_reg None dst 32;
-    add_data_instr n (nonblock dst instr)
-  | RBload chunk addr args dst =>
+    do pred <- translate_predicate preg p (Vvar dst) instr;
+    add_data_instr n pred
+  | RBload p chunk addr args dst =>
     do src <- translate_arr_access chunk addr args stack;
     do _ <- declare_reg None dst 32;
-    add_data_instr n (nonblock dst src)
-  | RBstore chunk addr args src =>
+    do pred <- translate_predicate preg p (Vvar dst) src;
+    add_data_instr n pred
+  | RBstore p chunk addr args src =>
     do dst <- translate_arr_access chunk addr args stack;
-    add_data_instr n (Vnonblock dst (Vvar src))
+    do pred <- translate_predicate preg p dst (Vvar src);
+    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)
   end.
 
-Definition translate_inst_list (fin rtrn stack : reg) (ni : node * list instr)
+Definition translate_inst_list (fin rtrn stack preg: reg) (ni : node * list instr)
   : mon unit :=
   let (n, li) := ni in
-  do _ <- collectlist (translate_inst fin rtrn stack n) li;
+  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)).
 
-Definition translate_cfi (fin rtrn stack : reg) (ni : node * cf_instr)
+Definition translate_cfi (fin rtrn stack: reg) (ni : node * cf_instr)
   : mon unit :=
   let (n, cfi) := ni in
   match cfi with
@@ -675,10 +691,10 @@ Definition translate_cfi (fin rtrn stack : reg) (ni : node * cf_instr)
     error (Errors.msg "HTLPargen: RPbuildin not supported.")
   end.
 
-Definition transf_bblock (fin rtrn stack : reg) (ni : node * bblock)
+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)
+  do _ <- collectlist (translate_inst_list fin rtrn stack preg)
                       (penumerate n bb.(bb_body));
   translate_cfi fin rtrn stack
                 ((n + poslength bb.(bb_body))%positive, bb.(bb_exit)).
@@ -689,7 +705,8 @@ Definition transf_module (f: function) : mon HTL.module :=
     do rtrn <- create_reg (Some Voutput) 32;
     do (stack, stack_len) <- create_arr None 32
                                         (Z.to_nat (f.(fn_stacksize) / 4));
-    do _ <- collectlist (transf_bblock fin rtrn stack)
+    do preg <- create_reg None 32;
+    do _ <- collectlist (transf_bblock fin rtrn stack preg)
                         (Maps.PTree.elements f.(fn_code));
     do _ <- collectlist (fun r => declare_reg (Some Vinput) r 32)
                         f.(fn_params);
diff --git a/src/hls/Partition.ml b/src/hls/Partition.ml
index d0b5a1b..19c6048 100644
--- a/src/hls/Partition.ml
+++ b/src/hls/Partition.ml
@@ -45,9 +45,9 @@ let prepend_instr i = function
 
 let translate_inst = function
   | RTL.Inop _ -> Some RBnop
-  | RTL.Iop (op, ls, dst, _) -> Some (RBop (op, ls, dst))
-  | RTL.Iload (m, addr, ls, dst, _) -> Some (RBload (m, addr, ls, dst))
-  | RTL.Istore (m, addr, ls, src, _) -> Some (RBstore (m, addr, ls, src))
+  | RTL.Iop (op, ls, dst, _) -> Some (RBop (None, op, ls, dst))
+  | RTL.Iload (m, addr, ls, dst, _) -> Some (RBload (None, m, addr, ls, dst))
+  | RTL.Istore (m, addr, ls, src, _) -> Some (RBstore (None, m, addr, ls, src))
   | _ -> None
 
 let translate_cfi = function
diff --git a/src/hls/PrintRTLBlockInstr.ml b/src/hls/PrintRTLBlockInstr.ml
index 3709e04..a943aab 100644
--- a/src/hls/PrintRTLBlockInstr.ml
+++ b/src/hls/PrintRTLBlockInstr.ml
@@ -22,14 +22,14 @@ let print_bblock_body pp i =
   fprintf pp "\t\t";
   match i with
   | RBnop -> fprintf pp "nop\n"
-  | RBop(op, ls, dst) ->
+  | RBop(_, op, ls, dst) ->
      fprintf pp "%a = %a\n"
        reg dst (PrintOp.print_operation reg) (op, ls)
-  | RBload(chunk, addr, args, dst) ->
+  | RBload(_, chunk, addr, args, dst) ->
      fprintf pp "%a = %s[%a]\n"
        reg dst (name_of_chunk chunk)
        (PrintOp.print_addressing reg) (addr, args)
-  | RBstore(chunk, addr, args, src) ->
+  | RBstore(_, chunk, addr, args, src) ->
      fprintf pp "%s[%a] = %a\n"
        (name_of_chunk chunk)
        (PrintOp.print_addressing reg) (addr, args)
diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v
index 90edc2e..c480d36 100644
--- a/src/hls/RTLBlockInstr.v
+++ b/src/hls/RTLBlockInstr.v
@@ -31,12 +31,14 @@ Require Import vericert.common.Vericertlib.
 Local Open Scope rtl.
 
 Definition node := positive.
+Definition predicate := positive.
 
 Inductive instr : Type :=
 | RBnop : instr
-| RBop : operation -> list reg -> reg -> instr
-| RBload : memory_chunk -> addressing -> list reg -> reg -> instr
-| RBstore : memory_chunk -> addressing -> list reg -> reg -> 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
+| RBsetpred : condition -> list reg -> predicate -> instr.
 
 Inductive cf_instr : Type :=
 | RBcall : signature -> reg + ident -> list reg -> reg -> node -> cf_instr
@@ -62,17 +64,26 @@ Definition successors_instr (i : cf_instr) : list node :=
 Definition max_reg_instr (m: positive) (i: instr) :=
   match i with
   | RBnop => m
-  | RBop op args res => fold_left Pos.max args (Pos.max res m)
-  | RBload chunk addr args dst => fold_left Pos.max args (Pos.max dst m)
-  | RBstore chunk addr args src => fold_left Pos.max args (Pos.max src m)
+  | RBop p op args res =>
+    fold_left Pos.max args (Pos.max res m)
+  | RBload p chunk addr args dst =>
+    fold_left Pos.max args (Pos.max dst m)
+  | 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
   end.
 
 Definition 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))
-  | RBcall sig (inr id) args res s => fold_left Pos.max args (Pos.max res m)
-  | RBtailcall sig (inl r) args => fold_left Pos.max args (Pos.max r m)
-  | RBtailcall sig (inr id) args => fold_left Pos.max args m
+  | RBcall sig (inl r) args res s =>
+    fold_left Pos.max args (Pos.max r (Pos.max res m))
+  | RBcall sig (inr id) args res s =>
+    fold_left Pos.max args (Pos.max res m)
+  | RBtailcall sig (inl r) args =>
+    fold_left Pos.max args (Pos.max r m)
+  | RBtailcall sig (inr id) args =>
+    fold_left Pos.max args m
   | RBbuiltin ef args res s =>
       fold_left Pos.max (params_of_builtin_args args)
         (fold_left Pos.max (params_of_builtin_res res) m)
@@ -102,9 +113,9 @@ Section DEFINITION.
   Context {bblock_body: Type}.
 
   Record bblock : Type := mk_bblock {
-                          bb_body: bblock_body;
-                          bb_exit: cf_instr
-                          }.
+    bb_body: bblock_body;
+    bb_exit: cf_instr
+  }.
 
   Definition code: Type := PTree.t bblock.
 
@@ -182,24 +193,24 @@ Section RELSEM.
       forall rs m sp,
       step_instr sp (InstrState rs m) RBnop (InstrState rs m)
   | exec_RBop:
-      forall op v res args rs m sp,
+      forall op v res args rs m sp p,
       eval_operation ge sp op rs##args m = Some v ->
       step_instr sp (InstrState rs m)
-                 (RBop op args res)
+                 (RBop p op args res)
                  (InstrState (rs#res <- v) m)
   | exec_RBload:
-      forall addr rs args a chunk m v dst sp,
+      forall addr rs args a chunk m v dst sp p,
       eval_addressing ge sp addr rs##args = Some a ->
       Mem.loadv chunk m a = Some v ->
       step_instr sp (InstrState rs m)
-                 (RBload chunk addr args dst)
+                 (RBload p chunk addr args dst)
                  (InstrState (rs#dst <- v) m)
   | exec_RBstore:
-      forall addr rs args a chunk m src m' sp,
+      forall addr rs args a chunk m src m' sp p,
       eval_addressing ge sp addr rs##args = Some a ->
       Mem.storev chunk m a rs#src = Some m' ->
       step_instr sp (InstrState rs m)
-                 (RBstore chunk addr args src)
+                 (RBstore p chunk addr args src)
                  (InstrState rs m').
 
   Inductive step_cf_instr: state -> cf_instr -> trace -> state -> Prop :=
diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v
index 0b79d2d..8ff701f 100644
--- a/src/hls/RTLPargen.v
+++ b/src/hls/RTLPargen.v
@@ -148,7 +148,7 @@ Proof.
   generalize list_operation_eq; intro.
   generalize list_reg_eq; intro.
   generalize AST.ident_eq; intro.
-  decide equality.
+  repeat decide equality.
 Defined.
 
 Lemma cf_instr_eq: forall (x y : cf_instr), {x = y} + {x <> y}.
@@ -569,12 +569,13 @@ Fixpoint list_translation (l : list reg) (f : forest) {struct l} : expression_li
 Definition update (f : forest) (i : instr) : forest :=
   match i with
   | RBnop => f
-  | RBop op rl r =>
+  | RBop p op rl r =>
     f # (Reg r) <- (Eop op (list_translation rl f))
-  | RBload chunk addr rl r =>
+  | RBload p chunk addr rl r =>
     f # (Reg r) <- (Eload chunk addr (list_translation rl f) (f # Mem))
-  | RBstore chunk addr rl r =>
+  | RBstore p chunk addr rl r =>
     f # Mem <- (Estore (f # Mem) chunk addr (list_translation rl f) (f # (Reg r)))
+  | RBsetpred c addr p => f
   end.
 
 (*|
diff --git a/src/hls/Schedule.ml b/src/hls/Schedule.ml
index 9865690..128f0e1 100644
--- a/src/hls/Schedule.ml
+++ b/src/hls/Schedule.ml
@@ -99,9 +99,9 @@ let accumulate_RAW_deps dfg curr =
       } )
   in
   match curr with
-  | RBop (_, rs, dst) -> acc_dep_instruction rs dst
-  | RBload (_mem, _addr, rs, dst) -> acc_dep_instruction rs dst
-  | RBstore (_mem, _addr, rs, src) -> acc_dep_instruction_nodst (src :: rs)
+  | RBop (op, _, rs, dst) -> acc_dep_instruction rs dst
+  | RBload (op, _mem, _addr, rs, dst) -> acc_dep_instruction rs dst
+  | RBstore (op, _mem, _addr, rs, src) -> acc_dep_instruction_nodst (src :: rs)
   | _ -> (i + 1, dst_map, { edges; nodes })
 
 (** Finds the next write to the [dst] register.  This is a small optimisation so that only one
@@ -113,8 +113,8 @@ let rec find_next_dst_write i dst i' curr =
   in
   match curr with
   | [] -> None
-  | RBop (_, _, dst') :: curr' -> check_dst dst' curr'
-  | RBload (_, _, _, dst') :: curr' -> check_dst dst' curr'
+  | RBop (_, _, _, dst') :: curr' -> check_dst dst' curr'
+  | RBload (_, _, _, _, dst') :: curr' -> check_dst dst' curr'
   | _ :: curr' -> find_next_dst_write i dst (i' + 1) curr'
 
 let rec find_all_next_dst_read i dst i' curr =
@@ -125,9 +125,9 @@ let rec find_all_next_dst_read i dst i' curr =
   in
   match curr with
   | [] -> []
-  | RBop (_, rs, _) :: curr' -> check_dst rs curr'
-  | RBload (_, _, rs, _) :: curr' -> check_dst rs curr'
-  | RBstore (_, _, rs, src) :: curr' -> check_dst (src :: rs) curr'
+  | RBop (_, _, rs, _) :: curr' -> check_dst rs curr'
+  | RBload (_, _, _, rs, _) :: curr' -> check_dst rs curr'
+  | RBstore (_, _, _, rs, src) :: curr' -> check_dst (src :: rs) curr'
   | RBnop :: curr' -> find_all_next_dst_read i dst (i' + 1) curr'
 
 let drop i lst =
@@ -148,18 +148,18 @@ let take i lst =
 
 let rec next_store i = function
   | [] -> None
-  | RBstore (_, _, _, _) :: _ -> Some i
+  | RBstore (_, _, _, _, _) :: _ -> Some i
   | _ :: rst -> next_store (i + 1) rst
 
 let rec next_load i = function
   | [] -> None
-  | RBload (_, _, _, _) :: _ -> Some i
+  | RBload (_, _, _, _, _) :: _ -> Some i
   | _ :: rst -> next_load (i + 1) rst
 
 let accumulate_RAW_mem_deps dfg curr =
   let i, { nodes; edges } = dfg in
   match curr with
-  | RBload (_, _, _, _) -> (
+  | RBload (_, _, _, _, _) -> (
       match next_store 0 (take i nodes |> List.rev) with
       | None -> (i + 1, { nodes; edges })
       | Some d -> (i + 1, { nodes; edges = (i - d - 1, i) :: edges }) )
@@ -168,7 +168,7 @@ let accumulate_RAW_mem_deps dfg curr =
 let accumulate_WAR_mem_deps dfg curr =
   let i, { nodes; edges } = dfg in
   match curr with
-  | RBstore (_, _, _, _) -> (
+  | RBstore (_, _, _, _, _) -> (
       match next_load 0 (take i nodes |> List.rev) with
       | None -> (i + 1, { nodes; edges })
       | Some d -> (i + 1, { nodes; edges = (i - d - 1, i) :: edges }) )
@@ -177,7 +177,7 @@ let accumulate_WAR_mem_deps dfg curr =
 let accumulate_WAW_mem_deps dfg curr =
   let i, { nodes; edges } = dfg in
   match curr with
-  | RBstore (_, _, _, _) -> (
+  | RBstore (_, _, _, _, _) -> (
       match next_store 0 (take i nodes |> List.rev) with
       | None -> (i + 1, { nodes; edges })
       | Some d -> (i + 1, { nodes; edges = (i - d - 1, i) :: edges }) )
@@ -194,9 +194,9 @@ let accumulate_WAW_deps dfg curr =
     | _ -> (i + 1, { nodes; edges })
   in
   match curr with
-  | RBop (_, _, dst) -> dst_dep dst
-  | RBload (_, _, _, dst) -> dst_dep dst
-  | RBstore (_, _, _, _) -> (
+  | RBop (_, _, _, dst) -> dst_dep dst
+  | RBload (_, _, _, _, dst) -> dst_dep dst
+  | RBstore (_, _, _, _, _) -> (
       match next_store (i + 1) (drop (i + 1) nodes) with
       | None -> (i + 1, { nodes; edges })
       | Some i' -> (i + 1, { nodes; edges = (i, i') :: edges }) )
@@ -211,15 +211,15 @@ let accumulate_WAR_deps dfg curr =
     (i + 1, { nodes; edges = List.append dep_list edges })
   in
   match curr with
-  | RBop (_, _, dst) -> dst_dep dst
-  | RBload (_, _, _, dst) -> dst_dep dst
+  | RBop (_, _, _, dst) -> dst_dep dst
+  | RBload (_, _, _, _, dst) -> dst_dep dst
   | _ -> (i + 1, { nodes; edges })
 
 let assigned_vars vars = function
   | RBnop -> vars
-  | RBop (_, _, dst) -> dst :: vars
-  | RBload (_, _, _, dst) -> dst :: vars
-  | RBstore (_, _, _, _) -> vars
+  | RBop (_, _, _, dst) -> dst :: vars
+  | RBload (_, _, _, _, dst) -> dst :: vars
+  | RBstore (_, _, _, _, _) -> vars
 
 (** All the nodes in the DFG have to come after the source of the basic block, and should terminate
    before the sink of the basic block.  After that, there should be constraints for data
diff --git a/src/hls/Verilog.v b/src/hls/Verilog.v
index ea9749d..a7db3ba 100644
--- a/src/hls/Verilog.v
+++ b/src/hls/Verilog.v
@@ -159,6 +159,7 @@ Inductive expr : Type :=
 | Vlit : value -> expr
 | Vvar : reg -> expr
 | Vvari : reg -> expr -> expr
+| Vrange : reg -> expr -> expr -> expr
 | Vinputvar : reg -> expr
 | Vbinop : binop -> expr -> expr -> expr
 | Vunop : unop -> expr -> expr
@@ -780,6 +781,7 @@ Proof.
               | [ H : expr_runp _ _ _ (Vbinop _ _ _) _ |- _ ] => invert H
               | [ H : expr_runp _ _ _ (Vunop _ _) _ |- _ ] => invert H
               | [ H : expr_runp _ _ _ (Vternary _ _ _) _ |- _ ] => invert H
+              | [ H : expr_runp _ _ _ (Vrange _ _ _) _ |- _ ] => invert H
 
               | [ H1 : forall asr asa v, expr_runp _ asr asa ?e v -> _,
                   H2 : expr_runp _ _ _ ?e _ |- _ ] =>