diff options
| -rw-r--r-- | src/hls/RTLBlockInstr.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v index 86f8eba..6b7c7ef 100644 --- a/src/hls/RTLBlockInstr.v +++ b/src/hls/RTLBlockInstr.v @@ -329,7 +329,8 @@ Section DEFINITION. Record bblock : Type := mk_bblock { bb_body: bblock_body; - bb_exit: cf_instr + bb_exit: cf_instr; + bb_parallel: bool; }. Definition code: Type := PTree.t bblock. |