From f77ef7aa3ecda17e3280846419223f24e4685f5f Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 12 Jan 2021 00:51:18 +0000 Subject: Add concat function to abstract_sequence --- src/hls/Scheduleoracle.v | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) (limited to 'src') diff --git a/src/hls/Scheduleoracle.v b/src/hls/Scheduleoracle.v index 11393ce..09b1355 100644 --- a/src/hls/Scheduleoracle.v +++ b/src/hls/Scheduleoracle.v @@ -483,14 +483,21 @@ Fixpoint abstract_sequence_block (f : forest) (b : list RTLBlock.instruction) : | i :: l => abstract_sequence_block (update_block f i) l end. -Fixpoint abstract_sequence_par (f : forest) (b : list RTLPar.instruction) : forest := +Fixpoint abstract_sequence_par' (f : forest) (b : list RTLPar.instruction) : forest := match b with | nil => f - | i :: l => abstract_sequence_par (update_par f i) l + | i :: l => abstract_sequence_par' (update_par f i) l + end. + +Fixpoint abstract_sequence_par (f : forest) (b : list (list RTLPar.instruction)) : forest := + match b with + | nil => f + | i :: l => abstract_sequence_par (abstract_sequence_par' f i) l 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. +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. |*) Definition check_control_flow_instr (c1 : RTLBlock.control_flow_inst) (c2 : RTLPar.control_flow_inst) : bool := @@ -503,4 +510,4 @@ transformation. Definition schedule_oracle (bb : RTLBlock.bblock) (bbt : RTLPar.bblock) : bool := check (abstract_sequence_block empty (RTLBlock.bb_body bb)) - (abstract_sequence_par empty (concat (RTLPar.bb_body bbt))). + (abstract_sequence_par empty (RTLPar.bb_body bbt)). -- cgit