Fix arguments to RBassign and piped

4 files changed, 10 insertions, 5 deletions

diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v
index a5b5f41..e1c7ec8 100644
--- a/src/hls/HTLPargen.v
+++ b/src/hls/HTLPargen.v
@@ -691,7 +691,7 @@ Definition translate_inst a (fin rtrn stack preg : reg) (n : node) (i : instr)
     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")
+  | RBassign p f src dst => error (Errors.msg "HTLPargen.translate_inst: assign")
   end.
 
 Lemma create_new_state_state_incr:
diff --git a/src/hls/PrintRTLBlockInstr.ml b/src/hls/PrintRTLBlockInstr.ml
index ba7241b..808d342 100644
--- a/src/hls/PrintRTLBlockInstr.ml
+++ b/src/hls/PrintRTLBlockInstr.ml
@@ -52,6 +52,11 @@ let print_bblock_body pp i =
     fprintf pp "%a = %a\n"
       pred p
       (PrintOp.print_condition reg) (c, args)
+  | RBpiped (p, fu, args) ->
+    fprintf pp "%a piped\n" print_pred_option p
+  | RBassign (p, fu, src, dst) ->
+    fprintf pp "%a %a = %a" print_pred_option p
+      reg src reg dst
 
 let rec print_bblock_exit pp i =
   fprintf pp "\t\t";
diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v
index 5ee9702..69cc709 100644
--- a/src/hls/RTLBlockInstr.v
+++ b/src/hls/RTLBlockInstr.v
@@ -252,7 +252,7 @@ Inductive instr : Type :=
 | 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
+| RBassign : option pred_op -> funct_node -> reg -> reg -> instr
 | RBsetpred : condition -> list reg -> predicate -> instr.
 
 Inductive cf_instr : Type :=
@@ -289,8 +289,8 @@ Definition max_reg_instr (m: positive) (i: instr) :=
     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
+  | RBassign p f src dst =>
+    Pos.max src (Pos.max dst m)
   | RBsetpred c args p =>
     fold_left Pos.max args m
   end.
diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v
index 97ec9aa..aaabe5d 100644
--- a/src/hls/RTLPargen.v
+++ b/src/hls/RTLPargen.v
@@ -577,7 +577,7 @@ Definition update (f : forest) (i : instr) : forest :=
     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
+  | RBassign p fu src dst => f
   end.
 
 (*|