diff options
author | Yann Herklotz <git@yannherklotz.com> | 2021-02-16 13:02:04 +0000 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2021-02-16 13:02:04 +0000 |
commit | 00ebd4125f46e4b21e18f907fc0498c078f38e95 (patch) | |
tree | 03eb9d901aaa177ce2ef21e277121ce15e68bc87 /src/hls/RTLPargen.v | |
parent | db2bdf8563bbb89fc953b758f53d8861dcf5c831 (diff) | |
download | vericert-00ebd4125f46e4b21e18f907fc0498c078f38e95.tar.gz vericert-00ebd4125f46e4b21e18f907fc0498c078f38e95.zip |
Fix RTLPar to use instr list list list
Diffstat (limited to 'src/hls/RTLPargen.v')
-rw-r--r-- | src/hls/RTLPargen.v | 8 |
1 files changed, 1 insertions, 7 deletions
diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v index 39c57df..e2e9a90 100644 --- a/src/hls/RTLPargen.v +++ b/src/hls/RTLPargen.v @@ -591,12 +591,6 @@ Fixpoint abstract_sequence (f : forest) (b : list instr) : forest := | i :: l => update (abstract_sequence f l) i end. -Fixpoint abstract_sequence_par (f : forest) (b : list (list instr)) : forest := - match b with - | nil => f - | i :: l => abstract_sequence (abstract_sequence_par f l) i - end. - (*| Check equivalence of control flow instructions. As none of the basic blocks should have been moved, none of the labels should be different, meaning the control-flow instructions should match exactly. @@ -622,7 +616,7 @@ Definition empty_trees (bb: RTLBlock.bb) (bbt: RTLPar.bb) : bool := Definition schedule_oracle (bb: RTLBlock.bblock) (bbt: RTLPar.bblock) : bool := check (abstract_sequence empty (bb_body bb)) - (abstract_sequence_par empty (bb_body bbt)) && + (abstract_sequence empty (concat (concat (bb_body bbt)))) && check_control_flow_instr (bb_exit bb) (bb_exit bbt) && empty_trees (bb_body bb) (bb_body bbt). |