Add proper functional unit generation

2 files changed, 98 insertions, 23 deletions

diff --git a/src/hls/RTLParFU.v b/src/hls/RTLParFU.v
index 3442ff0..b18aef6 100644
--- a/src/hls/RTLParFU.v
+++ b/src/hls/RTLParFU.v
@@ -37,8 +37,8 @@ Definition node := positive.
 Inductive instr : Type :=
 | FUnop : instr
 | FUop : option pred_op -> operation -> list reg -> reg -> instr
-| FUload : option pred_op -> memory_chunk -> addressing -> list reg -> reg -> instr
-| FUstore : option pred_op -> memory_chunk -> addressing -> list reg -> reg -> instr
+| FUread : positive -> positive -> reg -> instr
+| FUwrite : positive -> positive -> reg -> instr
 | FUsetpred : option pred_op -> condition -> list reg -> predicate -> instr.
 
 Inductive cf_instr : Type :=
@@ -69,10 +69,8 @@ Definition max_reg_instr (m: positive) (i: instr) :=
   | FUnop => m
   | FUop p op args res =>
       fold_left Pos.max args (Pos.max res m)
-  | FUload p chunk addr args dst =>
-      fold_left Pos.max args (Pos.max dst m)
-  | FUstore p chunk addr args src =>
-      fold_left Pos.max args (Pos.max src m)
+  | FUread p1 p2 r => Pos.max m r
+  | FUwrite p1 p2 r => Pos.max m r
   | FUsetpred p' c args p =>
       fold_left Pos.max args m
   end.
@@ -157,7 +155,7 @@ Record function: Type :=
       fn_params: list reg;
       fn_stacksize: Z;
       fn_code: code;
-      fn_funct_units: funct_unit;
+      fn_funct_units: resources;
       fn_entrypoint: node;
     }.
 
@@ -246,18 +244,6 @@ Section RELSEM.
       eval_operation ge sp op rs##args m = Some v ->
       eval_pred p (mk_instr_state rs pr m) (mk_instr_state (rs#res <- v) pr m) ist ->
       step_instr sp (mk_instr_state rs pr m) (FUop p op args res) ist
-  | exec_FUload:
-    forall addr rs args a chunk m v dst sp p pr ist,
-      eval_addressing ge sp addr rs##args = Some a ->
-      Mem.loadv chunk m a = Some v ->
-      eval_pred p (mk_instr_state rs pr m) (mk_instr_state (rs#dst <- v) pr m) ist ->
-      step_instr sp (mk_instr_state rs pr m) (FUload p chunk addr args dst) ist
-  | exec_FUstore:
-    forall addr rs args a chunk m src m' sp p pr ist,
-      eval_addressing ge sp addr rs##args = Some a ->
-      Mem.storev chunk m a rs#src = Some m' ->
-      eval_pred p (mk_instr_state rs pr m) (mk_instr_state rs pr m') ist ->
-      step_instr sp (mk_instr_state rs pr m) (FUstore p chunk addr args src) ist
   | exec_FUsetpred:
     forall sp rs pr m p c b args p' ist,
       Op.eval_condition c rs##args m = Some b ->
diff --git a/src/hls/RTLParFUgen.v b/src/hls/RTLParFUgen.v
index 389d76c..0098f57 100644
--- a/src/hls/RTLParFUgen.v
+++ b/src/hls/RTLParFUgen.v
@@ -1,21 +1,110 @@
+(*
+ * Vericert: Verified high-level synthesis.
+ * Copyright (C) 2021 Yann Herklotz <yann@yannherklotz.com>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ *)
+
 Require Import Coq.micromega.Lia.
 
 Require Import compcert.common.AST.
-Require compcert.common.Errors.
+Require Import compcert.common.Errors.
 Require compcert.common.Globalenvs.
-Require compcert.lib.Integers.
+Require Import compcert.lib.Integers.
 Require Import compcert.lib.Maps.
 
 Require Import vericert.common.Statemonad.
 Require Import vericert.common.Vericertlib.
 Require Import vericert.hls.AssocMap.
-Require Import vericert.hls.HTL.
 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.FunctionalUnits.
+
+#[local] Open Scope error_monad_scope.
+
+Definition transl_instr (res: resources) (i: RTLBlockInstr.instr): Errors.res (list (Z * RTLParFU.instr)) :=
+  match i with
+  | RBnop => Errors.OK ((0, FUnop)::nil)
+  | RBop po op args d => Errors.OK ((0, FUop po op args d)::nil)
+  | 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.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.Error (Errors.msg "Could not find RAM")
+      end
+  | RBsetpred op c args p => Errors.OK ((0, FUsetpred op c args p)::nil)
+  end.
+
+Fixpoint transl_cf_instr (i: RTLBlockInstr.cf_instr): RTLParFU.cf_instr :=
+  match i with
+  | RBcall sig r args d n => FUcall sig r args d n
+  | RBtailcall sig r args => FUtailcall sig r args
+  | RBbuiltin ef args r n => FUbuiltin ef args r n
+  | RBcond c args n1 n2 => FUcond c args n1 n2
+  | RBjumptable r ns => FUjumptable r ns
+  | RBreturn r => FUreturn r
+  | RBgoto n => FUgoto n
+  | RBpred_cf po c1 c2 => FUpred_cf po (transl_cf_instr c1) (transl_cf_instr c2)
+  end.
+
+Definition list_split {A:Type} (l: list (Z * A)) : (list (Z * A)) * (list (Z * A)) :=
+  (filter (fun x => Z.eqb 0 (fst x)) l,
+    map (fun x => (Z.pred (fst x), snd x)) (filter (fun x => negb (Z.eqb 0 (fst x))) l)).
+
+Fixpoint map_error {A B : Type} (f : A -> res B) (l : list A) {struct l} : res (list B) :=
+  match l with
+  | nil => OK nil
+  | x::xs =>
+    do y <- f x ;
+    do ys <- map_error f xs ;
+    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_bblock (bb: RTLPar.bblock): RTLParFU.bblock :=
+  RTLParFU.mk_bblock (transl_bb (bb_body bb)) (transl_cf_instr (bb_exit bb)).
+
+Definition transl_code (c: RTLPar.code): RTLParFU.code :=
+  PTree.map (fun _ => transl_bblock) 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)).
+
+Definition transl_fundef p :=
+  transf_partial_fundef transl_function p.
 
-Definition transl_program (p : RTLParFU.program) : Errors.res HTL.program :=
+Definition transl_program (p : RTLPar.program) : Errors.res RTLParFU.program :=
   transform_partial_program transl_fundef p.