diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-08-31 22:37:44 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-08-31 22:37:44 +0100 |
| commit | b431bdeb59e69df41cd98fadea49968d224493ee (patch) | |
| tree | 2432959ca65908e7c5573d1c87a43be2e8d2d4b4 /src/hls/RTLBlock.v | |
| parent | 6cb38f39f5609651691419c6a299b09695a4623c (diff) | |
| download | vericert-kvx-b431bdeb59e69df41cd98fadea49968d224493ee.tar.gz vericert-kvx-b431bdeb59e69df41cd98fadea49968d224493ee.zip | |
Add working partitioning algorithm
Diffstat (limited to 'src/hls/RTLBlock.v')
| -rw-r--r-- | src/hls/RTLBlock.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/hls/RTLBlock.v b/src/hls/RTLBlock.v index 2aaa010..a1c3f25 100644 --- a/src/hls/RTLBlock.v +++ b/src/hls/RTLBlock.v @@ -41,7 +41,8 @@ Inductive control_flow_inst : Type := builtin_res reg -> node -> control_flow_inst | RBcond : condition -> list reg -> node -> node -> control_flow_inst | RBjumptable : reg -> list node -> control_flow_inst -| RBreturn : option reg -> control_flow_inst. +| RBreturn : option reg -> control_flow_inst +| RBgoto : node -> control_flow_inst. Record bblock : Type := mk_bblock { bb_body: bblock_body; @@ -76,4 +77,5 @@ Definition successors_instr (i : control_flow_inst) : list node := | RBcond cond args ifso ifnot => ifso :: ifnot :: nil | RBjumptable arg tbl => tbl | RBreturn optarg => nil + | RBgoto n => n :: nil end. |