diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-02-22 18:42:11 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-02-22 18:42:11 +0000 |
| commit | 2243443c407a1e951265a9252bac3d3b9b830cbb (patch) | |
| tree | 80ad4560456aa30abc2c1a01b09a86c4ece7b6e9 /src/hls/RTLBlockInstr.v | |
| parent | 1a7f581dc4b67cbfe17936697aec8f85786c844d (diff) | |
| download | vericert-2243443c407a1e951265a9252bac3d3b9b830cbb.tar.gz vericert-2243443c407a1e951265a9252bac3d3b9b830cbb.zip | |
Fix arguments to RBassign and piped
Diffstat (limited to 'src/hls/RTLBlockInstr.v')
| -rw-r--r-- | src/hls/RTLBlockInstr.v | 6 |
1 files changed, 3 insertions, 3 deletions
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. |