From 00ebd4125f46e4b21e18f907fc0498c078f38e95 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 16 Feb 2021 13:02:04 +0000 Subject: Fix RTLPar to use instr list list list --- src/hls/RTLPargen.v | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) (limited to 'src/hls/RTLPargen.v') 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). -- cgit