Fix generation of RTLParFU

7 files changed, 30 insertions, 46 deletions

diff --git a/driver/VericertDriver.ml b/driver/VericertDriver.ml
index 467ae37..e89ff86 100644
--- a/driver/VericertDriver.ml
+++ b/driver/VericertDriver.ml
@@ -67,6 +67,7 @@ let compile_c_file sourcename ifile ofile =
   set_dest Vericert.PrintRTL.destination option_drtl ".rtl";
   set_dest Vericert.PrintRTLBlock.destination option_drtlblock ".rtlblock";
   set_dest Vericert.PrintRTLPar.destination option_drtlpar ".rtlpar";
+  set_dest Vericert.PrintRTLParFU.destination option_drtlparfu ".rtlparfu";
   set_dest Vericert.PrintHTL.destination option_dhtl ".htl";
   set_dest Vericert.Regalloc.destination_alloctrace option_dalloctrace ".alloctrace";
   set_dest Vericert.PrintLTL.destination option_dltl ".ltl";
@@ -393,6 +394,7 @@ let cmdline_actions =
   Exact "-drtl", Set option_drtl;
   Exact "-drtlblock", Set option_drtlblock;
   Exact "-drtlpar", Set option_drtlpar;
+  Exact "-drtlparfu", Set option_drtlparfu;
   Exact "-dhtl", Set option_dhtl;
   Exact "-dltl", Set option_dltl;
   Exact "-dalloctrace", Set option_dalloctrace;
@@ -407,6 +409,7 @@ let cmdline_actions =
     option_drtl := true;
     option_drtlblock := true;
     option_drtlpar := true;
+    option_drtlparfu := true;
     option_dhtl := true;
     option_dltl := true;
     option_dalloctrace := true;
diff --git a/src/Compiler.v b/src/Compiler.v
index ff0938e..0ac2b80 100644
--- a/src/Compiler.v
+++ b/src/Compiler.v
@@ -86,6 +86,7 @@ Parameter print_RTL: Z -> RTL.program -> unit.
 Parameter print_HTL: Z -> HTL.program -> unit.
 Parameter print_RTLBlock: Z -> RTLBlock.program -> unit.
 Parameter print_RTLPar: Z -> RTLPar.program -> unit.
+Parameter print_RTLParFU: Z -> RTLParFU.program -> unit.
 
 Definition print {A: Type} (printer: A -> unit) (prog: A) : A :=
   let unused := printer prog in prog.
@@ -249,6 +250,7 @@ Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program :=
   @@@ RTLPargen.transl_program
    @@ print (print_RTLPar 0)
   @@@ RTLParFUgen.transl_program
+   @@ print (print_RTLParFU 0)
   @@@ HTLPargen.transl_program
    @@ print (print_HTL 0)
    @@ Veriloggen.transl_program.
diff --git a/src/VericertClflags.ml b/src/VericertClflags.ml
index ab3c949..0402d49 100644
--- a/src/VericertClflags.ml
+++ b/src/VericertClflags.ml
@@ -6,6 +6,7 @@ let option_initial = ref false
 let option_dhtl = ref false
 let option_drtlblock = ref false
 let option_drtlpar = ref false
+let option_drtlparfu = ref false
 let option_hls_schedule = ref false
 let option_fif_conv = ref false
 let option_fram = ref true
diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v
index bca8fb5..aeefd2a 100644
--- a/src/extraction/Extraction.v
+++ b/src/extraction/Extraction.v
@@ -148,6 +148,7 @@ Extract Constant Compiler.print_RTLBlock => "PrintRTLBlock.print_if".
 Extract Constant Compiler.print_RTLPar => "PrintRTLPar.print_if".
 Extract Constant Compiler.print_HTL => "PrintHTL.print_if".
 Extract Constant Compiler.print_RTLPar => "PrintRTLPar.print_if".
+Extract Constant Compiler.print_RTLParFU => "PrintRTLParFU.print_if".
 Extract Constant Compiler.print_LTL => "PrintLTL.print_if".
 Extract Constant Compiler.print_Mach => "PrintMach.print_if".
 Extract Constant Compiler.print => "fun (f: 'a -> unit) (x: 'a) -> f x; x".
diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v
index b66a704..0695f07 100644
--- a/src/hls/HTLPargen.v
+++ b/src/hls/HTLPargen.v
@@ -392,10 +392,10 @@ Definition translate_instr (op : Op.operation) (args : list reg) : mon expr :=
   | Op.Omulimm n, r::nil => ret (boplit Vmul r n)
   | Op.Omulhs, r1::r2::nil => error (Errors.msg "Htlgen: Instruction not implemented: mulhs")
   | Op.Omulhu, r1::r2::nil => error (Errors.msg "Htlgen: Instruction not implemented: mulhu")
-  | Op.Odiv, r1::r2::nil => error (Errors.msg "Htlgen: Instruction not implemented: div")
-  | Op.Odivu, r1::r2::nil => error (Errors.msg "Htlgen: Instruction not implemented: divu")
-  | Op.Omod, r1::r2::nil => error (Errors.msg "Htlgen: Instruction not implemented: mod")
-  | Op.Omodu, r1::r2::nil => error (Errors.msg "Htlgen: Instruction not implemented: modu")
+  | Op.Odiv, r1::r2::nil => ret (bop Vdiv r1 r2)
+  | Op.Odivu, r1::r2::nil => ret (bop Vdivu r1 r2)
+  | Op.Omod, r1::r2::nil => ret (bop Vmod r1 r2)
+  | Op.Omodu, r1::r2::nil => ret (bop Vmodu r1 r2)
   | Op.Oand, r1::r2::nil => ret (bop Vand r1 r2)
   | Op.Oandimm n, r::nil => ret (boplit Vand r n)
   | Op.Oor, r1::r2::nil => ret (bop Vor r1 r2)
@@ -458,28 +458,6 @@ Definition add_branch_instr (e: expr) (n n1 n2: node) : mon unit :=
     | _ => Error (Errors.msg "Htlgen: add_branch_instr")
     end.
 
-Definition translate_arr_access (mem : AST.memory_chunk) (addr : Op.addressing)
-           (args : list reg) (stack : reg) : mon expr :=
-  match mem, addr, args with (* TODO: We should be more methodical here; what are the possibilities?*)
-  | Mint32, Op.Aindexed off, r1::nil =>
-    if (check_address_parameter_signed off)
-    then ret (Vvari stack (Vbinop Vdivu (boplitz Vadd r1 off) (Vlit (ZToValue 4))))
-    else error (Errors.msg "HTLgen: translate_arr_access address out of bounds")
-  | Mint32, Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *)
-    if (check_address_parameter_signed scale) && (check_address_parameter_signed offset)
-    then ret (Vvari stack
-                    (Vbinop Vdivu
-                            (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale))
-                            (Vlit (ZToValue 4))))
-    else error (Errors.msg "HTLgen: translate_arr_access address out of bounds")
-  | Mint32, Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *)
-    let a := Integers.Ptrofs.unsigned a in
-    if (check_address_parameter_unsigned a)
-    then ret (Vvari stack (Vlit (ZToValue (a / 4))))
-    else error (Errors.msg "HTLgen: eff_addressing out of bounds stack offset")
-  | _, _, _ => error (Errors.msg "HTLgen: translate_arr_access unsuported addressing")
-  end.
-
 Fixpoint enumerate (i : nat) (ns : list node) {struct ns} : list (nat * node) :=
   match ns with
   | n :: ns' => (i, n) :: enumerate (i+1) ns'
@@ -680,7 +658,7 @@ Definition translate_predicate (a : assignment)
     ret (a dst (Vternary (pred_expr preg pos) e dst))
   end.
 
-Definition translate_inst a (fin rtrn stack preg : reg) (n : node) (i : instr)
+Definition translate_inst a (fin rtrn preg : reg) (n : node) (i : instr)
   : mon stmnt :=
   match i with
   | FUnop =>
@@ -721,18 +699,18 @@ Definition create_new_state (p: node): mon node :=
                 s.(st_controllogic))
               (create_new_state_state_incr s p).
 
-Definition translate_inst_list (fin rtrn stack preg: reg) (ni : node * node * list (list instr)) :=
+Definition translate_inst_list (fin rtrn preg: reg) (ni : node * node * list (list instr)) :=
   match ni with
   | (n, p, li) =>
     do _ <- collectlist
           (fun l =>
-             do stmnt <- translate_inst Vblock fin rtrn stack preg n l;
+             do stmnt <- translate_inst Vblock fin rtrn preg n l;
              add_data_instr n stmnt) (concat li);
     do st <- get;
     add_control_instr n (state_goto st.(st_st) p)
   end.
 
-Fixpoint translate_cfi' (fin rtrn stack preg: reg) (cfi: cf_instr)
+Fixpoint translate_cfi' (fin rtrn preg: reg) (cfi: cf_instr)
   : mon (stmnt * stmnt) :=
   match cfi with
   | FUgoto n' =>
@@ -752,8 +730,8 @@ Fixpoint translate_cfi' (fin rtrn stack preg: reg) (cfi: cf_instr)
            Vskip)
     end
   | FUpred_cf p c1 c2 =>
-    do (tc1s, tc1c) <- translate_cfi' fin rtrn stack preg c1;
-    do (tc2s, tc2c) <- translate_cfi' fin rtrn stack preg c2;
+    do (tc1s, tc1c) <- translate_cfi' fin rtrn preg c1;
+    do (tc2s, tc2c) <- translate_cfi' fin rtrn preg c2;
     ret ((Vcond (pred_expr preg p) tc1s tc2s), (Vcond (pred_expr preg p) tc1c tc2c))
   | FUjumptable r tbl =>
     do s <- get;
@@ -766,23 +744,23 @@ Fixpoint translate_cfi' (fin rtrn stack preg: reg) (cfi: cf_instr)
     error (Errors.msg "HTLPargen: RPbuildin not supported.")
   end.
 
-Definition translate_cfi (fin rtrn stack preg: reg) (ni: node * cf_instr)
+Definition translate_cfi (fin rtrn preg: reg) (ni: node * cf_instr)
   : mon unit :=
   let (n, cfi) := ni in
-  do (s, c) <- translate_cfi' fin rtrn stack preg cfi;
+  do (s, c) <- translate_cfi' fin rtrn preg cfi;
   do _ <- add_control_instr n c;
   add_data_instr n s.
 
-Definition transf_bblock (fin rtrn stack preg: reg) (ni : node * bblock)
+Definition transf_bblock (fin rtrn preg: reg) (ni : node * bblock)
   : mon unit :=
   let (n, bb) := ni in
   do nstate <- create_new_state ((poslength bb.(bb_body)))%positive;
-  do _ <- collectlist (translate_inst_list fin rtrn stack preg)
+  do _ <- collectlist (translate_inst_list fin rtrn preg)
                       (prange n (nstate + poslength bb.(bb_body) - 1)%positive
                                   bb.(bb_body));
   match bb.(bb_body) with
-  | nil => translate_cfi fin rtrn stack preg (n, bb.(bb_exit))
-  | _ => translate_cfi fin rtrn stack preg (nstate, bb.(bb_exit))
+  | nil => translate_cfi fin rtrn preg (n, bb.(bb_exit))
+  | _ => translate_cfi fin rtrn preg (nstate, bb.(bb_exit))
   end.
 
 Definition decide_order a b c d e f g : {module_ordering a b c d e f g} + {True}.
@@ -806,10 +784,8 @@ Definition transf_module (f: function) : mon HTL.module.
   if stack_correct f.(fn_stacksize) then
     do fin <- create_reg (Some Voutput) 1;
     do rtrn <- create_reg (Some Voutput) 32;
-    do (stack, stack_len) <- create_arr None 32
-                                        (Z.to_nat (f.(fn_stacksize) / 4));
     do preg <- create_reg None 32;
-    do _ <- collectlist (transf_bblock fin rtrn stack preg)
+    do _ <- collectlist (transf_bblock fin rtrn 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/RTLParFUgen.v b/src/hls/RTLParFUgen.v
index 55fe4e7..65ddf74 100644
--- a/src/hls/RTLParFUgen.v
+++ b/src/hls/RTLParFUgen.v
@@ -57,7 +57,7 @@ Definition transl_instr (res: resources) (cycle: positive) (i: RTLBlockInstr.ins
                           :: 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)
+                          :: instr_list, update (Pos.pred cycle)
                                                 (add_instr (FUop po Op.Omove (ram_d_out r::nil) d))
                                                 d_tree)
       | _ => Errors.Error (Errors.msg "Could not find RAM")
diff --git a/src/hls/Schedule.ml b/src/hls/Schedule.ml
index 94225fa..b75465b 100644
--- a/src/hls/Schedule.ml
+++ b/src/hls/Schedule.ml
@@ -289,6 +289,7 @@ let comb_delay = function
   | _ -> 1
 
 let pipeline_stages = function
+  | RBload _ -> 2
   | RBop (_, op, _, _) ->
     (match op with
      | Odiv -> 32
@@ -743,7 +744,7 @@ let solve_constraints constr =
             |> drop 3
             |> List.fold_left parse_soln (IMap.empty, IMap.empty)
   in
-  Sys.remove fn; res
+  (*Sys.remove fn;*) res
 
 let subgraph dfg l =
   let dfg' = List.fold_left (fun g v -> DFG.add_vertex g v) DFG.empty l in
@@ -806,14 +807,14 @@ let transf_rtlpar c c' schedule =
       let body = IMap.to_seq i_sched_tree |> List.of_seq |> List.map snd
                  |> List.map (List.map (fun x -> (x, List.nth bb_body' x)))
       in
-      (*let body2 = List.fold_left (fun x b ->
+      let body2 = List.fold_left (fun x b ->
           match IMap.find_opt b i_sched_tree with
           | Some i -> i :: x
           | None -> [] :: x
         ) [] (range (fst bb_st_e) (snd bb_st_e + 1))
         |> List.map (List.map (fun x -> (x, List.nth bb_body' x)))
         |> List.rev
-      in*)
+      in
       (*let final_body = List.map (fun x -> subgraph dfg x |> order_instr) body in*)
       let final_body2 = List.map (fun x -> subgraph dfg x
                                            |> (fun x ->
@@ -821,7 +822,7 @@ let transf_rtlpar c c' schedule =
                                                |> List.map (subgraph x)
                                                |> List.map (fun y ->
                                                    TopoDFG.fold (fun i l -> snd i :: l) y []
-                                                   |> List.rev))) body
+                                                   |> List.rev))) body2
                                            (*|> (fun x -> TopoDFG.fold (fun i l -> snd i :: l) x [])
                                            |> List.rev) body2*)
       in