Add new instructions for pipelines

9 files changed, 33 insertions, 24 deletions

diff --git a/src/hls/FunctionalUnits.v b/src/hls/FunctionalUnits.v
index 019cf15..392b1ae 100644
--- a/src/hls/FunctionalUnits.v
+++ b/src/hls/FunctionalUnits.v
@@ -21,13 +21,15 @@ Require Import compcert.lib.Maps.
 
 Require Import vericert.common.Vericertlib.
 
+Definition funct_node := positive.
+
 Inductive funct_unit: Type :=
 | SignedDiv (size: positive) (numer denom quot rem: reg): funct_unit
 | UnsignedDiv (size: positive) (numer denom quot rem: reg): funct_unit.
 
 Record funct_units := mk_avail_funct_units {
-    avail_sdiv: option positive;
-    avail_udiv: option positive;
+    avail_sdiv: option funct_node;
+    avail_udiv: option funct_node;
     avail_units: PTree.t funct_unit;
   }.
 
diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v
index 01588f6..a5b5f41 100644
--- a/src/hls/HTLPargen.v
+++ b/src/hls/HTLPargen.v
@@ -392,7 +392,7 @@ Definition translate_eff_addressing (a: Op.addressing) (args: list reg)
   end.
 
 (** Translate an instruction to a statement. FIX mulhs mulhu *)
-Definition translate_instr (op : Op.operation) (args : list reg) : mon stmnt :=
+Definition translate_instr (op : Op.operation) (args : list reg) : mon expr :=
   match op, args with
   | Op.Omove, r::nil => ret (Vvar r)
   | Op.Ointconst n, _ => ret (Vlit (intToValue n))
@@ -402,22 +402,10 @@ Definition translate_instr (op : Op.operation) (args : list reg) : mon stmnt :=
   | 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 =>
-    do s <- get;
-    match sdiv_present s.(st_funct_units) 32%positive with
-    | SignedDiv s n d q r :: _ =>
-      ret (Vseq (Vnonblock (Vvar n) (Vvar r1)) (Vnonblock (Vvar d) (Vvar r2)))
-    | _ =>
-      do n <- create_reg None 32;
-      do d <- create_reg None 32;
-      do q <- create_reg None 32;
-      do r <- create_reg None 32;
-      do _ <- add_funct_unit (SignedDiv 32%positive n d q r);
-      ret (Vseq (Vnonblock (Vvar n) (Vvar r1)) (Vnonblock (Vvar d) (Vvar r2)))
-    end
-  | 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.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.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)
@@ -702,6 +690,8 @@ Definition translate_inst a (fin rtrn stack preg : reg) (n : node) (i : instr)
   | RBsetpred c args p =>
     do cond <- translate_condition c args;
     ret (a (pred_expr preg (Pvar p)) cond)
+  | RBpiped p f args => error (Errors.msg "HTLPargen.translate_inst: piped")
+  | RBassign p f dst => error (Errors.msg "HTLPargen.translate_inst: assign")
   end.
 
 Lemma create_new_state_state_incr:
@@ -828,7 +818,7 @@ Definition transf_module (f: function) : mon HTL.module :=
            start
            rst
            clk
-           nil
+           initial_funct_units
            current_state.(st_scldecls)
            current_state.(st_arrdecls)
            (conj (max_pc_wf _ LECTRL) (max_pc_wf _ LEDATA)))
diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v
index b323a65..76616fb 100644
--- a/src/hls/HTLgen.v
+++ b/src/hls/HTLgen.v
@@ -32,6 +32,7 @@ Require Import vericert.hls.AssocMap.
 Require Import vericert.hls.HTL.
 Require Import vericert.hls.ValueInt.
 Require Import vericert.hls.Verilog.
+Require Import vericert.hls.FunctionalUnits.
 
 Hint Resolve AssocMap.gempty : htlh.
 Hint Resolve AssocMap.gso : htlh.
@@ -610,7 +611,7 @@ Definition transf_module (f: function) : mon HTL.module :=
            start
            rst
            clk
-           nil
+           initial_funct_units
            current_state.(st_scldecls)
            current_state.(st_arrdecls)
            (conj (max_pc_wf _ LECTRL) (max_pc_wf _ LEDATA)))
diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v
index ae7917f..556e3cc 100644
--- a/src/hls/HTLgenspec.v
+++ b/src/hls/HTLgenspec.v
@@ -31,6 +31,7 @@ Require Import vericert.hls.ValueInt.
 Require Import vericert.hls.HTL.
 Require Import vericert.hls.HTLgen.
 Require Import vericert.hls.AssocMap.
+Require Import vericert.hls.FunctionalUnits.
 
 Hint Resolve Maps.PTree.elements_keys_norepet : htlspec.
 Hint Resolve Maps.PTree.elements_correct : htlspec.
@@ -183,7 +184,7 @@ Inductive tr_module (f : RTL.function) : module -> Prop :=
                         data
                         control
                         f.(RTL.fn_entrypoint)
-                        st stk stk_len fin rtrn start rst clk nil scldecls arrdecls wf) ->
+                        st stk stk_len fin rtrn start rst clk initial_funct_units scldecls arrdecls wf) ->
       (forall pc i, Maps.PTree.get pc f.(RTL.fn_code) = Some i ->
                tr_code f.(RTL.fn_code) pc i data control fin rtrn st stk) ->
       stk_len = Z.to_nat (f.(RTL.fn_stacksize) / 4) ->
diff --git a/src/hls/IfConversion.v b/src/hls/IfConversion.v
index 39d9fd2..e893578 100644
--- a/src/hls/IfConversion.v
+++ b/src/hls/IfConversion.v
@@ -113,7 +113,7 @@ Definition transf_function (f: function) : function :=
   let (_, c) := List.fold_left if_convert_code
                                (find_blocks_with_cond f.(fn_code))
                                (1%nat, f.(fn_code)) in
-  mkfunction f.(fn_sig) f.(fn_params) f.(fn_stacksize) c f.(fn_entrypoint).
+  mkfunction f.(fn_sig) f.(fn_params) f.(fn_stacksize) c f.(fn_funct_units) f.(fn_entrypoint).
 
 Definition transf_fundef (fd: fundef) : fundef :=
   transf_fundef transf_function fd.
diff --git a/src/hls/Partition.ml b/src/hls/Partition.ml
index 19c6048..270db14 100644
--- a/src/hls/Partition.ml
+++ b/src/hls/Partition.ml
@@ -118,6 +118,7 @@ let function_from_RTL f =
                 fn_stacksize = f.RTL.fn_stacksize;
                 fn_params = f.RTL.fn_params;
                 fn_entrypoint = f.RTL.fn_entrypoint;
+                fn_funct_units = FunctionalUnits.initial_funct_units;
                 fn_code = c
               }
 
diff --git a/src/hls/PrintVerilog.ml b/src/hls/PrintVerilog.ml
index 8c9f20e..824623e 100644
--- a/src/hls/PrintVerilog.ml
+++ b/src/hls/PrintVerilog.ml
@@ -257,7 +257,9 @@ let pprint_module debug i n m =
     concat [ indent i; "module "; (extern_atom n);
              "("; concat (intersperse ", " (List.map register (inputs @ outputs))); ");\n";
              fold_map (pprint_module_item (i+1)) m.mod_body;
-             concat (List.map (print_funct_units m.mod_clk) m.mod_funct_units);
+             concat (List.map (print_funct_units m.mod_clk)
+                       (Maps.PTree.elements m.mod_funct_units.avail_units
+                        |> List.map snd));
              if !option_initial then print_initial i (Nat.to_int m.mod_stk_len) m.mod_stk else "";
              if debug then debug_always_verbose i m.mod_clk m.mod_st else "";
              indent i; "endmodule\n\n"
diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v
index 86f8eba..5ee9702 100644
--- a/src/hls/RTLBlockInstr.v
+++ b/src/hls/RTLBlockInstr.v
@@ -30,6 +30,7 @@ Require Import compcert.verilog.Op.
 
 Require Import vericert.common.Vericertlib.
 Require Import vericert.hls.Sat.
+Require Import vericert.hls.FunctionalUnits.
 
 Local Open Scope rtl.
 
@@ -250,6 +251,8 @@ Inductive instr : Type :=
 | 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
+| RBpiped : option pred_op -> funct_node -> list reg -> instr
+| RBassign : option pred_op -> funct_node -> reg -> instr
 | RBsetpred : condition -> list reg -> predicate -> instr.
 
 Inductive cf_instr : Type :=
@@ -284,6 +287,10 @@ Definition max_reg_instr (m: positive) (i: instr) :=
     fold_left Pos.max args (Pos.max dst m)
   | RBstore p chunk addr args src =>
     fold_left Pos.max args (Pos.max src m)
+  | RBpiped p f args =>
+    fold_left Pos.max args m
+  | RBassign p f dst =>
+    Pos.max dst m
   | RBsetpred c args p =>
     fold_left Pos.max args m
   end.
@@ -339,6 +346,7 @@ Section DEFINITION.
     fn_params: list reg;
     fn_stacksize: Z;
     fn_code: code;
+    fn_funct_units: funct_units;
     fn_entrypoint: node
   }.
 
diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v
index e2e9a90..97ec9aa 100644
--- a/src/hls/RTLPargen.v
+++ b/src/hls/RTLPargen.v
@@ -576,6 +576,8 @@ Definition update (f : forest) (i : instr) : forest :=
   | 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
+  | RBpiped p fu args => f
+  | RBassign p fu dst => f
   end.
 
 (*|
@@ -673,6 +675,7 @@ Definition transl_function (f: RTLBlock.function) : Errors.res RTLPar.function :
                           f.(fn_params)
                           f.(fn_stacksize)
                           tfcode
+                          f.(fn_funct_units)
                           f.(fn_entrypoint))
   else
     Errors.Error (Errors.msg "RTLPargen: Could not prove the blocks equivalent.").
@@ -683,6 +686,7 @@ Definition transl_function_temp (f: RTLBlock.function) : Errors.res RTLPar.funct
                           f.(fn_params)
                           f.(fn_stacksize)
                           tfcode
+                          f.(fn_funct_units)
                           f.(fn_entrypoint)).
 
 Definition transl_fundef := transf_partial_fundef transl_function_temp.