diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2022-03-31 15:39:18 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2022-03-31 15:39:18 +0100 |
| commit | 2e232deb0aed4af2448eb9f1031e8084181174b7 (patch) | |
| tree | 6dd781e24a2a260047a8fc9e0a177d1b81bc3b5c /src/hls/RTLParFUgen.v | |
| parent | f3e95ff03f1dc9a9de57721eb1c9c93c19329613 (diff) | |
| download | vericert-2e232deb0aed4af2448eb9f1031e8084181174b7.tar.gz vericert-2e232deb0aed4af2448eb9f1031e8084181174b7.zip | |
Add list of bb to semantics
Diffstat (limited to 'src/hls/RTLParFUgen.v')
| -rw-r--r-- | src/hls/RTLParFUgen.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/hls/RTLParFUgen.v b/src/hls/RTLParFUgen.v index 49ee6e7..a104056 100644 --- a/src/hls/RTLParFUgen.v +++ b/src/hls/RTLParFUgen.v @@ -134,7 +134,7 @@ Definition insert_extra (pt: PTree.t (list instr)) (curr: list (list instr)) | None => ((cycle + 1)%positive, curr :: bb) end. -Definition transl_bb (res: resources) (bb: RTLPar.bb): Errors.res RTLParFU.bblock_body := +Definition transl_bb (res: resources) (bb: list RTLPar.bb): Errors.res RTLParFU.bblock_body := do (litr, n) <- fold_right (transl_seq_block res) (OK (nil, PTree.empty _, 1%positive)) bb; let (li, tr) := litr in OK (snd (fold_right (insert_extra tr) (1%positive, nil) li)). |