From 52c41786bb4673ebea32a870e7a3ad948cfe574d Mon Sep 17 00:00:00 2001 From: Michalis Pardalos Date: Mon, 1 Mar 2021 11:17:09 +0000 Subject: Add idle state after return --- src/hls/HTLgen.v | 13 ++++++------ src/hls/HTLgenspec.v | 57 +++++++++++++++++++++++++++------------------------- 2 files changed, 37 insertions(+), 33 deletions(-) (limited to 'src') diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v index 9373a33..052aaad 100644 --- a/src/hls/HTLgen.v +++ b/src/hls/HTLgen.v @@ -563,12 +563,13 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni add_node_skip n (Vcase (Vvar r) (tbl_to_case_expr s.(st_st) tbl) (Some Vskip))*) error (Errors.msg "Ijumptable: Case statement not supported.") | Ireturn r => - match r with - | Some r' => - add_instr_skip n (data_vstmnt (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vvar r')))) - | None => - add_instr_skip n (data_vstmnt (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vlit (ZToValue 0%Z))))) - end + do idle_state <- create_state; + let retval := match r with + | Some r' => Vvar r' + | None => Vlit (ZToValue 0%Z) + end in + do _ <- add_instr n idle_state (data_vstmnt (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn retval))); + add_instr_skip idle_state (data_vstmnt (nonblock fin (Vlit (ZToValue 0%Z)))) end end. diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v index b76b8ec..d9928a9 100644 --- a/src/hls/HTLgenspec.v +++ b/src/hls/HTLgenspec.v @@ -481,7 +481,10 @@ Proof. congruence. - monadInv H. apply translate_condition_freshreg_trans in EQ. apply add_branch_instr_freshreg_trans in EQ0. congruence. - (*- inv EQ. apply add_node_skip_freshreg_trans in EQ0. congruence.*) + - apply create_state_freshreg_trans in EQ. + apply add_instr_freshreg_trans in EQ1. + apply add_instr_skip_freshreg_trans in EQ2. + congruence. Qed. Hint Resolve transf_instr_freshreg_trans : htlspec. @@ -598,32 +601,32 @@ Proof. eauto with htlspec. * apply in_map with (f := fst) in H2. contradiction. - (*+ destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. - + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. - + inversion H2. - * inversion H14. constructor. congruence. - * apply in_map with (f := fst) in H14. contradiction. - *) - + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. - + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. - + inversion H2. - * inversion H9. - replace (st_st s2) with (st_st s0) by congruence. - eauto with htlspec. - * apply in_map with (f := fst) in H9. contradiction. - - + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. - + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. - + inversion H2. - * inversion H9. - replace (st_st s2) with (st_st s0) by congruence. - eauto with htlspec. - * apply in_map with (f := fst) in H9. contradiction. - - - eapply IHl. apply EQ0. assumption. - destruct H2. inversion H2. subst. contradiction. - intros. specialize H1 with pc0 instr0. destruct H1. tauto. trivial. - destruct H2. inv H2. contradiction. assumption. assumption. + (* + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. *) + (* + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. *) + (* + inversion H2. *) + (* * inversion H14. constructor. congruence. *) + (* * apply in_map with (f := fst) in H14. contradiction. *) + + (* + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. *) + (* + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. *) + (* + inversion H2. *) + (* * inversion H9. *) + (* replace (st_st s2) with (st_st s0) by congruence. *) + (* eauto with htlspec. *) + (* * apply in_map with (f := fst) in H9. contradiction. *) + + (* + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. *) + (* + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. *) + (* + inversion H2. *) + (* * inversion H9. *) + (* replace (st_st s2) with (st_st s0) by congruence. *) + (* eauto with htlspec. *) + (* * apply in_map with (f := fst) in H9. contradiction. *) + + (* - eapply IHl. apply EQ0. assumption. *) + (* destruct H2. inversion H2. subst. contradiction. *) + (* intros. specialize H1 with pc0 instr0. destruct H1. tauto. trivial. *) + (* destruct H2. inv H2. contradiction. assumption. assumption. *) Admitted. Hint Resolve iter_expand_instr_spec : htlspec. -- cgit