diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-02-21 21:35:34 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-02-21 21:35:34 +0000 |
| commit | 359194617de51adcc451b45b6c1b0a9332820906 (patch) | |
| tree | 7b1fce73244ebbb1195c37dd986de0bf1d081a0c /src/hls/RTLBlockInstr.v | |
| parent | a47cfd17f0e1fc6aca5e10de9362a4be2d4af468 (diff) | |
| download | vericert-359194617de51adcc451b45b6c1b0a9332820906.tar.gz vericert-359194617de51adcc451b45b6c1b0a9332820906.zip | |
Add new instructions for pipelines
Diffstat (limited to 'src/hls/RTLBlockInstr.v')
| -rw-r--r-- | src/hls/RTLBlockInstr.v | 8 |
1 files changed, 8 insertions, 0 deletions
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 }. |