Finish generation of RTLParFU with RAM insertion

1 files changed, 92 insertions, 24 deletions

diff --git a/src/hls/RTLParFUgen.v b/src/hls/RTLParFUgen.v
index 0098f57..55fe4e7 100644
--- a/src/hls/RTLParFUgen.v
+++ b/src/hls/RTLParFUgen.v
@@ -28,40 +28,52 @@ Require Import vericert.common.Statemonad.
 Require Import vericert.common.Vericertlib.
 Require Import vericert.hls.AssocMap.
 Require Import vericert.hls.Predicate.
-Require Import vericert.hls.RTLParFU.
 Require Import vericert.hls.ValueInt.
 Require Import vericert.hls.Verilog.
 Require Import vericert.hls.RTLBlockInstr.
 Require Import vericert.hls.RTLPar.
+Require Import vericert.hls.RTLParFU.
 Require Import vericert.hls.FunctionalUnits.
 
 #[local] Open Scope error_monad_scope.
 
-Definition transl_instr (res: resources) (i: RTLBlockInstr.instr): Errors.res (list (Z * RTLParFU.instr)) :=
+Definition update {A: Type} (i: positive) (f: option A -> A) (pt: PTree.t A) :=
+  PTree.set i (f (pt ! i)) pt.
+
+Definition add_instr (instr_: instr) x :=
+  match x with Some i => instr_ :: i | None => instr_ :: nil end.
+
+Definition transl_instr (res: resources) (cycle: positive) (i: RTLBlockInstr.instr)
+           (li: Errors.res (list instr * PTree.t (list instr))):
+  Errors.res (list instr * PTree.t (list instr)) :=
+  do (instr_list, d_tree) <- li;
   match i with
-  | RBnop => Errors.OK ((0, FUnop)::nil)
-  | RBop po op args d => Errors.OK ((0, FUop po op args d)::nil)
+  | RBnop => Errors.OK (FUnop :: instr_list, d_tree)
+  | RBop po op args d => Errors.OK (FUop po op args d :: instr_list, d_tree)
   | RBload po chunk addr args d =>
       match get_ram 0 res with
       | Some (ri, r) =>
-          Errors.OK ((0, FUop po Op.Onot (ram_u_en r::nil) (ram_u_en r))
-                       :: (0, FUop po (Op.Ointconst (Int.repr 0)) nil (ram_wr_en r))
-                       :: (0, FUop po (Op.Olea addr) args (ram_addr r))
-                       :: (1, FUop po Op.Omove (ram_d_out r::nil) d)
-                       :: nil)
+          Errors.OK (FUop po Op.Onot (ram_u_en r::nil) (ram_u_en r)
+                          :: FUop po (Op.Ointconst (Int.repr 0)) nil (ram_wr_en r)
+                          :: FUop po (Op.Olea addr) args (ram_addr r)
+                          :: FUop po (Op.Oshruimm (Int.repr 2)) ((ram_addr r)::nil) (ram_addr r)
+                          :: instr_list, update (cycle+1)
+                                                (add_instr (FUop po Op.Omove (ram_d_out r::nil) d))
+                                                d_tree)
       | _ => Errors.Error (Errors.msg "Could not find RAM")
       end
   | RBstore po chunk addr args d =>
       match get_ram 0 res with
       | Some (ri, r) =>
-          Errors.OK ((0, FUop po Op.Onot (ram_u_en r::nil) (ram_u_en r))
-                       :: (0, FUop po (Op.Ointconst (Int.repr 1)) nil (ram_wr_en r))
-                       :: (0, FUop po Op.Omove (d::nil) (ram_d_in r))
-                       :: (0, FUop po (Op.Olea addr) args (ram_addr r))
-                       :: nil)
+          Errors.OK (FUop po Op.Onot (ram_u_en r::nil) (ram_u_en r)
+                          :: FUop po (Op.Ointconst (Int.repr 1)) nil (ram_wr_en r)
+                          :: FUop po Op.Omove (d::nil) (ram_d_in r)
+                          :: FUop po (Op.Olea addr) args (ram_addr r)
+                          :: FUop po (Op.Oshruimm (Int.repr 2)) ((ram_addr r)::nil) (ram_addr r)
+                          :: instr_list, d_tree)
       | _ => Errors.Error (Errors.msg "Could not find RAM")
       end
-  | RBsetpred op c args p => Errors.OK ((0, FUsetpred op c args p)::nil)
+  | RBsetpred op c args p => Errors.OK (FUsetpred op c args p :: instr_list, d_tree)
   end.
 
 Fixpoint transl_cf_instr (i: RTLBlockInstr.cf_instr): RTLParFU.cf_instr :=
@@ -89,19 +101,75 @@ Fixpoint map_error {A B : Type} (f : A -> res B) (l : list A) {struct l} : res (
     OK (y::ys)
   end.
 
-Definition transl_bb (res: resources) (bb: RTLPar.bb): RTLParFU.bblock_body :=
-  map_error (map_error (fold_right
-                          (fun c n => transl_instr res))) bb.
+Definition transl_op_chain_block (res: resources) (cycle: positive) (instrs: list RTLBlockInstr.instr)
+           (state: Errors.res (list (list instr) * PTree.t (list instr)))
+  : Errors.res (list (list instr) * PTree.t (list instr)) :=
+  do (li, tr) <- state;
+  do (li', tr') <- fold_right (transl_instr res cycle) (OK (nil, tr)) instrs;
+  OK (li' :: li, tr').
+
+(*Compute transl_op_chain_block initial_resources 10%nat (RBop None (Op.Ointconst (Int.repr 1)) nil 1%positive::RBnop::RBnop::RBnop::nil) (OK (nil, PTree.empty _)).*)
+
+Definition transl_par_block (res: resources) (cycle: positive) (instrs: list (list RTLBlockInstr.instr))
+           (state: Errors.res (list (list (list instr)) * PTree.t (list instr)))
+  : Errors.res (list (list (list instr)) * PTree.t (list instr)) :=
+  do (li, tr) <- state;
+  do (li', tr') <- fold_right (transl_op_chain_block res cycle) (OK (nil, tr)) instrs;
+  OK (li' :: li, tr').
+
+(*Compute transl_par_block initial_resources 10%nat ((RBop None (Op.Ointconst (Int.repr 1)) nil 1%positive::RBnop::nil)::(RBop None (Op.Ointconst (Int.repr 2)) nil 2%positive::RBnop::nil)::nil) (OK (((FUnop::nil)::nil)::nil, PTree.empty _)).*)
+
+Definition transl_seq_block (res: resources) (b: list (list RTLBlockInstr.instr))
+           (a: Errors.res (list (list (list instr)) * PTree.t (list instr) * positive)) :=
+  do (litr, n) <- a;
+  let (li, tr) := litr in
+  do (li', tr') <- transl_par_block res n b (OK (li, tr));
+  OK (li', tr', (n+1)%positive).
+
+Definition insert_extra (pt: PTree.t (list instr)) (curr: list (list instr))
+         (cycle_bb: (positive * list (list (list instr)))) :=
+  let (cycle, bb) := cycle_bb in
+  match pt ! cycle with
+  | Some instrs => ((cycle + 1)%positive, (curr ++ (map (fun x => x :: nil) instrs)) :: bb)
+  | None => ((cycle + 1)%positive, curr :: bb)
+  end.
+
+Definition transl_bb (res: resources) (bb: RTLPar.bb): Errors.res RTLParFU.bblock_body :=
+  do (litr, n) <- fold_right (transl_seq_block res) (OK (nil, PTree.empty _, 1%positive)) bb;
+  let (li, tr) := litr in
+  OK (snd (fold_right (insert_extra tr) (1%positive, nil) li)).
+
+Definition transl_bblock (res: resources) (bb: RTLPar.bblock): Errors.res bblock :=
+  do bb' <- transl_bb res (RTLBlockInstr.bb_body bb);
+  OK (mk_bblock bb' (transl_cf_instr (RTLBlockInstr.bb_exit bb))).
 
-Definition transl_bblock (bb: RTLPar.bblock): RTLParFU.bblock :=
-  RTLParFU.mk_bblock (transl_bb (bb_body bb)) (transl_cf_instr (bb_exit bb)).
+Definition error_map_ptree {A B: Type} (f: positive -> A -> res B) (pt: PTree.t A) :=
+  do ptl' <- map_error (fun x => do x' <- uncurry f x; OK (fst x, x')) (PTree.elements pt);
+  OK (PTree_Properties.of_list ptl').
 
-Definition transl_code (c: RTLPar.code): RTLParFU.code :=
-  PTree.map (fun _ => transl_bblock) c.
+Definition transl_code (fu: resources) (c: RTLPar.code): res code :=
+   error_map_ptree (fun _ => transl_bblock fu) c.
 
 Definition transl_function (f: RTLPar.function): Errors.res RTLParFU.function :=
-  Errors.OK (RTLParFU.mkfunction (fn_sig f) (fn_params f) (fn_stacksize f) (transl_code (fn_code f))
-                                 initial_resources (fn_entrypoint f)).
+  let max := RTLPar.max_reg_function f in
+  let fu := set_res (Ram (mk_ram
+                            (Z.to_nat (RTLBlockInstr.fn_stacksize f))
+                            (max+1)%positive
+                            (max+3)%positive
+                            (max+7)%positive
+                            (max+2)%positive
+                            (max+6)%positive
+                            (max+4)%positive
+                            (max+5)%positive
+                            ltac:(lia)
+                    )) initial_resources in
+  do c' <- transl_code fu (RTLBlockInstr.fn_code f);
+  Errors.OK (mkfunction (RTLBlockInstr.fn_sig f)
+                        (RTLBlockInstr.fn_params f)
+                        (RTLBlockInstr.fn_stacksize f)
+                        c'
+                        fu
+                        (RTLBlockInstr.fn_entrypoint f)).
 
 Definition transl_fundef p :=
   transf_partial_fundef transl_function p.