diff options
-rw-r--r-- | src/hls/HTLPargen.v | 2 | ||||
-rw-r--r-- | src/hls/PrintRTLBlockInstr.ml | 5 | ||||
-rw-r--r-- | src/hls/RTLBlockInstr.v | 6 | ||||
-rw-r--r-- | src/hls/RTLPargen.v | 2 |
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. (*| |