diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-02-21 16:33:04 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-02-21 16:33:04 +0000 |
| commit | fa71365709883b845eb01822ae8d929fbbb38f71 (patch) | |
| tree | 057c55201d6981b06a98adb03cdfdf9895127393 | |
| parent | 71fee63bcd943d33c761f228227b1bf8c60c1aac (diff) | |
| download | vericert-kvx-dev/cond-const-prop.tar.gz vericert-kvx-dev/cond-const-prop.zip | |
Add parallel blockdev/cond-const-prop
| -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. |