Add operation pipelining

2 files changed, 137 insertions, 8 deletions

diff --git a/src/Compiler.v b/src/Compiler.v
index e837e9d..e9d76dc 100644
--- a/src/Compiler.v
+++ b/src/Compiler.v
@@ -68,6 +68,7 @@ Require vericert.hls.RTLPargen.
 Require vericert.hls.HTLPargen.
 Require vericert.hls.Pipeline.
 Require vericert.hls.IfConversion.
+Require vericert.hls.PipelineOp.
 Require vericert.HLSOpts.
 
 Require Import vericert.hls.HTLgenproof.
@@ -240,6 +241,9 @@ Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program :=
    @@ total_if HLSOpts.optim_if_conversion IfConversion.transf_program
    @@ print (print_RTLBlock 2)
   @@@ RTLPargen.transl_program
+   @@ print (print_RTLPar 1)
+   @@ PipelineOp.transf_program
+   @@ print (print_RTLPar 2)
   @@@ HTLPargen.transl_program
    @@ print print_HTL
    @@ Veriloggen.transl_program.
diff --git a/src/hls/PipelineOp.v b/src/hls/PipelineOp.v
index 0783e4e..793b752 100644
--- a/src/hls/PipelineOp.v
+++ b/src/hls/PipelineOp.v
@@ -16,6 +16,9 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
+Require Import Coq.Lists.List.
+
+Require Import compcert.backend.Registers.
 Require Import compcert.common.AST.
 Require Import compcert.common.Errors.
 Require Import compcert.common.Globalenvs.
@@ -23,12 +26,15 @@ Require Import compcert.lib.Integers.
 Require Import compcert.lib.Maps.
 Require Import compcert.verilog.Op.
 
+
 Require Import vericert.common.Vericertlib.
 Require Import vericert.hls.RTLBlockInstr.
 Require Import vericert.hls.RTLPar.
 Require Import vericert.hls.FunctionalUnits.
 
-Definition state : Type := code * funct_units.
+Import Option.Notation.
+
+Local Open Scope positive.
 
 Definition div_pos (il: nat * list nat) x :=
   let (i, l) := il in
@@ -40,24 +46,143 @@ Definition div_pos (il: nat * list nat) x :=
   | _ => (S i, l)
   end.
 
-Definition find_divs (bb: bblock) : list nat :=
-  snd (List.fold_left div_pos bb.(bb_body) (1%nat, nil)).
+Definition div_pos_in_list (il: nat * list (nat * nat)) bb :=
+  let (i, l) := il in
+  let dp := snd (List.fold_left div_pos bb (0%nat, nil)) in
+  (S i, (List.map (fun x => (i, x)) dp) ++ l).
+
+Definition div_pos_in_block (il: nat * list (nat * nat * nat)) bb :=
+  let (i, l) := il in
+  let dp := snd (List.fold_left div_pos_in_list bb (0%nat, nil)) in
+  (S i, (List.map (fun (yx : nat * nat) => let (y, x) := yx in (i, y, x)) dp) ++ l).
+
+Definition find_divs (bb: bblock) :=
+  snd (List.fold_left div_pos_in_block bb.(bb_body) (0%nat, nil)).
+
+Fixpoint mapi' {A B: Type} (n: nat) (f: nat -> A -> B) (l: list A): list B :=
+  match l with
+  | nil => nil
+  | a :: b => f n a :: mapi' (S n) f b
+  end.
+
+Definition mapi {A B: Type} := @mapi' A B 0.
+
+Definition map_at {A: Type} (n: nat) (f: A -> A) (l: list A): list A :=
+  mapi (fun i il =>
+          if Nat.eqb n i
+          then f il
+          else il
+       ) l.
+
+Definition map_at_err {A: Type} (n: nat) (f: A -> A) (l: list A): option (list A) :=
+  if (Datatypes.length l <=? n)%nat
+  then None
+  else Some (map_at n f l).
+
+Definition replace_div' sdiv udiv (d: instr) :=
+  match d with
+  | RBop op Odiv args dst => RBpiped op sdiv args
+  | RBop op Odivu args dst => RBpiped op udiv args
+  | RBop op Omod args dst => RBpiped op sdiv args
+  | RBop op Omodu args dst => RBpiped op udiv args
+  | _ => d
+  end.
+
+Definition get_sdiv (fu: funct_unit) : option (reg * reg * reg) :=
+  match fu with
+  | SignedDiv s a b d _ => Some (a, b, d)
+  | _ => None
+  end.
 
-Definition transf_code (i: state) (bbn: node * bblock) : state :=
+Definition get_udiv (fu: funct_unit) : option (reg * reg * reg) :=
+  match fu with
+  | UnsignedDiv s a b d _ => Some (a, b, d)
+  | _ => None
+  end.
+
+Definition get_smod (fu: funct_unit) : option (reg * reg * reg) :=
+  match fu with
+  | SignedDiv s a b _ d => Some (a, b, d)
+  | _ => None
+  end.
+
+Definition get_umod (fu: funct_unit) : option (reg * reg * reg) :=
+  match fu with
+  | UnsignedDiv s a b _ d => Some (a, b, d)
+  | _ => None
+  end.
+
+Definition bind3 {A B C D: Type}
+           (f: option (A * B * C))
+           (g: A -> B -> C -> option D) : option D :=
+  match f with
+  | Some (a, b, c) => g a b c
+  | None => None
+  end.
+
+Notation "'do' ( X , Y , Z ) <- A ; B" := (bind3 A (fun X Y Z => B))
+   (at level 200, X ident, Y ident, Z ident, A at level 100, B at level 200).
+
+Definition replace_div_error (fu: funct_units) (bb: bb) (loc: nat * nat * nat) :=
+  match loc with
+  | (z, y, x) =>
+    do sdiv <- fu.(avail_sdiv);
+    do udiv <- fu.(avail_udiv);
+    do sfu <- PTree.get sdiv fu.(avail_units);
+    do ufu <- PTree.get udiv fu.(avail_units);
+    do z' <- List.nth_error bb z;
+    do y' <- List.nth_error z' y;
+    do x' <- List.nth_error y' x;
+    let transf := map_at z (map_at y (map_at x (replace_div' sdiv udiv))) bb in
+    match x' with
+    | RBop op Odiv args dst =>
+      do (s1, s2, src) <- get_sdiv sfu;
+      map_at_err (z + 32)%nat (fun x => (RBassign op sdiv src dst :: nil) :: x) transf
+    | RBop op Odivu args dst =>
+      do (s1, s2, src) <- get_udiv ufu;
+      map_at_err (z + 32)%nat (fun x => (RBassign op sdiv src dst :: nil) :: x) transf
+    | RBop op Omod args dst =>
+      do (s1, s2, src) <- get_smod sfu;
+      map_at_err (z + 32)%nat (fun x => (RBassign op sdiv src dst :: nil) :: x) transf
+    | RBop op Omodu args dst =>
+      do (s1, s2, src) <- get_umod ufu;
+      map_at_err (z + 32)%nat (fun x => (RBassign op sdiv src dst :: nil) :: x) transf
+    | _ => None
+    end
+  end.
+
+Definition replace_div (fu: funct_units) (bb: bb) loc :=
+  match replace_div_error fu bb loc with
+  | Some bb' => bb'
+  | _ => bb
+  end.
+
+Definition transf_code (i: code * funct_units) (bbn: node * bblock) :=
   let (c, fu) := i in
   let (n, bb) := bbn in
-  (PTree.set n bb c, fu).
+  let divs := find_divs bb in
+  match divs with
+  | nil => (PTree.set n bb c, fu)
+  | _ =>
+    (PTree.set n (mk_bblock (List.fold_left (replace_div fu) divs bb.(bb_body)) bb.(bb_exit)) c, fu)
+  end.
+
+Definition create_fu (r: reg) :=
+  let fu := PTree.set 2 (UnsignedDiv 32 (r+5) (r+6) (r+7) (r+8))
+      (PTree.set 1 (SignedDiv 32 (r+1) (r+2) (r+3) (r+4)) (PTree.empty _)) in
+  mk_avail_funct_units (Some 1) (Some 2) fu.
 
 Definition transf_function (f: function) : function :=
-  let (c, fu) := List.fold_left transf_code
+  let fu := create_fu (max_reg_function f) in
+  let (c, fu') := List.fold_left transf_code
                                 (PTree.elements f.(fn_code))
-                                (PTree.empty bblock, f.(fn_funct_units)) in
+                                (PTree.empty bblock, fu) in
   mkfunction
     f.(fn_sig)
     f.(fn_params)
     f.(fn_stacksize)
     c
-    fu
+    fu'
     f.(fn_entrypoint).
 
 Definition transf_fundef (fd: fundef) : fundef :=