diff options
Diffstat (limited to 'src/hls')
| -rw-r--r-- | src/hls/HTLgen.v | 7 | ||||
| -rw-r--r-- | src/hls/HTLgenproof.v | 10 | ||||
| -rw-r--r-- | src/hls/HTLgenspec.v | 3 |
3 files changed, 14 insertions, 6 deletions
diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v index 39146ff..908c627 100644 --- a/src/hls/HTLgen.v +++ b/src/hls/HTLgen.v @@ -490,8 +490,9 @@ Definition fork (rst : reg) (params : list (reg * reg)) : datapath_stmnt := let assign_params := nonblock_all params in Vseq reset_mod assign_params. -Definition join (fn_rtrn fn_rst fn_dst : reg) : datapath_stmnt := - let set_result := Vnonblock (Vvar fn_dst) (Vvar fn_rtrn) in +Definition join (fn_fin fn_rst fn_rtrn fn_dst : reg) : datapath_stmnt := + let set_result := Vcond (boplitz Veq fn_fin 1) + (Vnonblock (Vvar fn_dst) (Vvar fn_rtrn)) Vskip in let stop_reset := Vnonblock (Vvar fn_rst) (Vlit (ZToValue 0)) in Vseq stop_reset set_result. @@ -558,7 +559,7 @@ Definition transf_instr (ge : RTL.genv) (fin rtrn stack: reg) (ni: node * instru do return_reg <- map_externctrl fn ctrl_return; let fork_instr := fork reset_reg params in - let join_instr := join return_reg reset_reg dst in + let join_instr := join finish_reg reset_reg return_reg dst in do _ <- add_instr n join_state fork_instr; add_instr_wait finish_reg join_state n' join_instr diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v index 5b1dc1b..ae9967f 100644 --- a/src/hls/HTLgenproof.v +++ b/src/hls/HTLgenproof.v @@ -139,7 +139,7 @@ Inductive match_frames (ge : RTL.genv) (current_id : HTL.ident) (mem : Memory.me (CONST : match_constants m asr) (EXTERN_CALLER : has_externctrl m current_id ret rst fin) (JOIN_CTRL : (HTL.mod_controllogic m)!st = Some (state_wait (HTL.mod_st m) fin pc)) - (JOIN_DATA : (HTL.mod_datapath m)!st = Some (join ret rst dst)) + (JOIN_DATA : (HTL.mod_datapath m)!st = Some (join fin rst ret dst)) (TAILS : match_frames ge mid mem rtl_tl htl_tl) (DST : Ple dst (RTL.max_reg_function f)) (PC : (Z.pos pc <= Int.max_unsigned)), @@ -1566,7 +1566,13 @@ Section CORRECTNESS. rewrite assign_all_out by admit. rewrite AssocMap.gso by not_control_reg. apply AssocMap.gss. - * repeat econstructor. + * unfold join. + econstructor. + -- repeat econstructor. + -- eapply Verilog.stmnt_runp_Vcond_false. + ++ repeat econstructor. + ++ big_tac. admit. (* TODO: Externctrl finish is false *) + ++ repeat econstructor. * constructor. * simpl. apply AssocMapExt.merge_correct_2. diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v index b46fd3b..dbdc8bf 100644 --- a/src/hls/HTLgenspec.v +++ b/src/hls/HTLgenspec.v @@ -102,7 +102,7 @@ Inductive tr_code (ge : RTL.genv) (c : RTL.code) (pc : RTL.node) (stmnts : datap Z.pos pc2 <= Int.max_unsigned /\ stmnts!pc = Some (fork fn_rst (List.combine fn_params args)) /\ trans!pc = Some (state_goto st pc2) /\ - stmnts!pc2 = Some (join fn_return fn_rst dst) /\ + stmnts!pc2 = Some (join fn_finish fn_rst fn_return dst) /\ trans!pc2 = Some (state_wait st fn_finish n)) -> tr_code ge c pc stmnts trans externctrl fin rtrn st stk (RTL.Icall sig (inr fn) args dst n) @@ -410,6 +410,7 @@ Proof. * monad_crush. * replace x6 with (st_freshreg s7) in * by intro_step. replace x5 with (st_freshreg s6) in * by intro_step. + replace x4 with (st_freshreg s5) in * by intro_step. monad_crush. * replace x4 with (st_freshreg s5) in * by intro_step. monad_crush. |