diff options
Diffstat (limited to 'src/hls/RTLPargen.v')
-rw-r--r-- | src/hls/RTLPargen.v | 28 |
1 files changed, 22 insertions, 6 deletions
diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v index f745466..d592206 100644 --- a/src/hls/RTLPargen.v +++ b/src/hls/RTLPargen.v @@ -485,13 +485,13 @@ Get a sequence from the basic block. Fixpoint abstract_sequence (f : forest) (b : list instr) : forest := match b with | nil => f - | i :: l => abstract_sequence (update f i) l + | 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_par (abstract_sequence f i) l + | i :: l => abstract_sequence (abstract_sequence_par f l) i end. (*| @@ -507,9 +507,21 @@ We define the top-level oracle that will check if two basic blocks are equivalen transformation. |*) +Definition empty_trees (bb: RTLBlock.bblock_body) (bbt: RTLPar.bblock_body) : bool := + match bb with + | nil => + match bbt with + | nil => true + | _ => false + end + | _ => true + end. + 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_par empty (bb_body bbt)) && + check_control_flow_instr (bb_exit bb) (bb_exit bbt) && + empty_trees (bb_body bb) (bb_body bbt). Definition check_scheduled_trees := beq2 schedule_oracle. @@ -539,9 +551,13 @@ Proof. solve_scheduled_trees_correct. Qed. Parameter schedule : RTLBlock.function -> RTLPar.function. Definition transl_function (f: RTLBlock.function) : Errors.res RTLPar.function := - let tf := schedule f in - if check_scheduled_trees f.(RTLBlock.fn_code) tf.(fn_code) then - Errors.OK tf + let tfcode := fn_code (schedule f) in + if check_scheduled_trees f.(RTLBlock.fn_code) tfcode then + Errors.OK (mkfunction f.(RTLBlock.fn_sig) + f.(RTLBlock.fn_params) + f.(RTLBlock.fn_stacksize) + tfcode + f.(RTLBlock.fn_entrypoint)) else Errors.Error (Errors.msg "RTLPargen: Could not prove the blocks equivalent."). |