Add idle state after return

2 files changed, 37 insertions, 33 deletions

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.