From cc970eefd58251160e630fac3e91e29a057b0035 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 3 May 2021 19:22:35 +0100 Subject: Add divider --- src/hls/HTL.v | 14 ++++- src/hls/Memorygen.v | 159 ++++++++++++++++++++++++++++++++++++++-------------- src/hls/Verilog.v | 79 ++++++++++++++++++++++++-- 3 files changed, 202 insertions(+), 50 deletions(-) diff --git a/src/hls/HTL.v b/src/hls/HTL.v index 61ea541..2489d91 100644 --- a/src/hls/HTL.v +++ b/src/hls/HTL.v @@ -89,10 +89,13 @@ Record module: Type := mod_scldecls : AssocMap.t (option Verilog.io * Verilog.scl_decl); mod_arrdecls : AssocMap.t (option Verilog.io * Verilog.arr_decl); mod_ram : option ram; + mod_div : option Verilog.div; mod_wf : map_well_formed mod_controllogic /\ map_well_formed mod_datapath; mod_ordering_wf : module_ordering mod_st mod_finish mod_return mod_stk mod_start mod_reset mod_clk; mod_ram_wf : forall r', mod_ram = Some r' -> mod_clk < ram_addr r'; mod_params_wf : Forall (Pos.gt mod_st) mod_params; + mod_div_wf : forall d, mod_div = Some d -> mod_clk < Verilog.div_a d; + mod_div_ram_wf : forall d r, mod_div = Some d -> mod_ram = Some r -> ram_u_en r < Verilog.div_a d; }. Definition fundef := AST.fundef module. @@ -175,7 +178,7 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := forall g m st sf ctrl data asr asa basr1 basa1 nasr1 nasa1 - basr2 basa2 nasr2 nasa2 + basr2 basa2 nasr2 nasa2 basr2' nasr2' basr3 basa3 nasr3 nasa3 asr' asa' f pstval, @@ -197,8 +200,10 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := data (Verilog.mkassociations basr2 nasr2) (Verilog.mkassociations basa2 nasa2) -> + Verilog.exec_div (Verilog.mkassociations basr2 nasr2) (mod_div m) + (Verilog.mkassociations basr2' nasr2') -> exec_ram - (Verilog.mkassociations (Verilog.merge_regs nasr2 basr2) empty_assocmap) + (Verilog.mkassociations (Verilog.merge_regs nasr2' basr2') empty_assocmap) (Verilog.mkassociations (Verilog.merge_arrs nasa2 basa2) (empty_stack m)) (mod_ram m) (Verilog.mkassociations basr3 nasr3) @@ -208,6 +213,11 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := asr'!(m.(mod_st)) = Some (posToValue pstval) -> (Z.pos pstval <= Integers.Int.max_unsigned)%Z -> step g (State sf m st asr asa) Events.E0 (State sf m pstval asr' asa') +| trigger_call : + asr!(new_reset) = Some r -> + maping_reg r = Some r' -> + r' = (mod_reset f) -> + State -> Callstate | step_finish : forall g m st asr asa retval sf, asr!(m.(mod_finish)) = Some (ZToValue 1) -> diff --git a/src/hls/Memorygen.v b/src/hls/Memorygen.v index 1dd6603..dbb6961 100644 --- a/src/hls/Memorygen.v +++ b/src/hls/Memorygen.v @@ -222,8 +222,8 @@ Definition transf_module (m: module): module. let new_size := (mod_stk_len m) in let ram := mk_ram new_size (mod_stk m) en u_en addr wr_en d_in d_out ltac:(eauto using ram_wf) in let tc := transf_code (mod_st m) ram (mod_datapath m) (mod_controllogic m) in - match mod_ram m with - | None => + match mod_ram m, mod_div m with + | None, None => mkmodule m.(mod_params) (fst tc) (snd tc) @@ -245,8 +245,9 @@ Definition transf_module (m: module): module. (AssocMap.set m.(mod_stk) (None, VArray 32 (2 ^ Nat.log2_up new_size))%nat m.(mod_arrdecls)) (Some ram) - _ (mod_ordering_wf m) _ (mod_params_wf m) - | _ => m + None + _ (mod_ordering_wf m) _ (mod_params_wf m) ltac:(discriminate) ltac:(discriminate) + | _, _ => m end). eapply transf_code_wf. apply (mod_wf m). destruct tc eqn:?; simpl. rewrite <- Heqp. intuition. @@ -1081,6 +1082,7 @@ Hint Resolve max_module_stmnts : mgen. Lemma transf_module_code : forall m, mod_ram m = None -> + mod_div m = None -> transf_code (mod_st m) {| ram_size := mod_stk_len m; ram_mem := mod_stk m; @@ -1098,8 +1100,10 @@ Proof. unfold transf_module; intros; repeat destruct_match; crush. Hint Resolve transf_module_code : mgen. Lemma transf_module_code_ram : - forall m r, mod_ram m = Some r -> transf_module m = m. -Proof. unfold transf_module; intros; repeat destruct_match; crush. Qed. + forall m r d, mod_ram m = Some r \/ mod_div m = Some d -> transf_module m = m. +Proof. unfold transf_module; intros; repeat destruct_match; crush. + inv H; discriminate. +Qed. Hint Resolve transf_module_code_ram : mgen. Lemma mod_reset_lt : forall m, mod_reset m < max_reg_module m + 1. @@ -1242,6 +1246,15 @@ Proof. repeat (try econstructor; mgen_crush). Qed. +Definition forall_div (P: reg -> Prop) div := + P (div_en div) + /\ P (div_u_en div) + /\ P (div_a div) + /\ P (div_b div) + /\ P (div_q div) + /\ P (div_r div) + /\ P (div_done div). + Lemma match_assocmaps_merge : forall p nasr basr nasr' basr', match_assocmaps p nasr nasr' -> @@ -2481,6 +2494,60 @@ Proof. auto. Qed. +Lemma match_assocmap_set : + forall p rs1 rs2, + match_assocmaps p rs1 rs2 -> + forall s v, + match_assocmaps p (rs1 # s <- v) (rs2 # s <- v). +Proof. + inversion 1; simplify. + constructor; intros. + destruct (Pos.eq_dec s r); subst. + repeat rewrite AssocMap.gss. auto. + repeat rewrite AssocMap.gso; auto. +Qed. + +Lemma exec_div_same : + forall rs1 div rs2 p, + exec_div rs1 (Some div) rs2 -> + forall_div (fun x => x < p) div -> + forall trs1, + match_reg_assocs p rs1 trs1 -> + exists trs2, + exec_div trs1 (Some div) trs2 + /\ match_reg_assocs p rs2 trs2. +Proof. + inversion 1; crush. + - inv H6. simplify. eexists. split. + unfold forall_div in *; simplify. + constructor; simplify. + eapply int_eq_not_changed. eauto. + inv H7. inv H8. eauto. + inv H7. eauto. + apply Int.same_if_eq in H3. inv H7. apply H10 in H11. + unfold find_assocmap, AssocMapExt.get_default in *. + rewrite H11 in H3. rewrite H3. auto. + constructor; auto. + - unfold forall_div in *; simplify. inv H9. simplify. + econstructor. split. + inv H8. inv H12. + eapply exec_div_Some_input; simplify; auto. + apply Int.same_if_eq in H2. unfold find_assocmap, AssocMapExt.get_default in *. + rewrite H9 in H1; auto. eauto. + unfold find_assocmap, AssocMapExt.get_default in *. rewrite H9 in H2; auto. + rewrite <- H9; auto. + constructor; simplify; auto. + repeat apply match_assocmap_set; auto. + - unfold forall_div in *; simplify. inv H8; simplify. + econstructor. split. inv H10. inv H12. + eapply exec_div_Some_output; simplify; auto. + unfold find_assocmap, AssocMapExt.get_default in *. rewrite H8 in H1; auto. + rewrite <- H8; eauto. + rewrite <- H8; eauto. + constructor; simplify; auto. + repeat apply match_assocmap_set; auto. +Qed. + Lemma translation_correct : forall m asr nasa1 basa1 nasr1 basr1 basr2 nasr2 nasa2 basa2 nasr3 basr3 nasa3 basa3 asr'0 asa'0 res' st tge pstval sf asa ctrl data f, @@ -2506,6 +2573,7 @@ Lemma translation_correct : (Z.pos pstval <= 4294967295)%Z -> match_states (State sf m st asr asa) (State res' (transf_module m) st asr'0 asa'0) -> mod_ram m = None -> + mod_div m = None -> exists R2 : state, Smallstep.plus step tge (State res' (transf_module m) st asr'0 asa'0) Events.E0 R2 /\ match_states (State sf m pstval (merge_regs nasr3 basr3) (merge_arrs nasa3 basa3)) R2. @@ -2544,20 +2612,21 @@ Proof. assert (MATCH_ARR3': match_arrs_size ran'2 rab'2) by eauto with mgen. do 2 econstructor. apply Smallstep.plus_one. econstructor. eauto with mgen. eauto with mgen. eauto with mgen. - rewrite <- H12. eassumption. rewrite <- H7. eassumption. + rewrite <- H13. eassumption. rewrite <- H7. eassumption. eauto. eauto with mgen. eauto. + unfold transf_module; repeat destruct_match; crush. constructor. rewrite empty_stack_transf. unfold transf_module; repeat destruct_match; try discriminate. econstructor. simplify. unfold disable_ram in *. unfold transf_module in DISABLE_RAM. repeat destruct_match; try discriminate; []. simplify. - pose proof H17 as R1. apply max_reg_stmnt_not_modified with (r := max_reg_module m + 2) in R1. - pose proof H17 as R2. eapply max_reg_stmnt_not_modified_nb with (r := max_reg_module m + 2) in R2. - pose proof H18 as R3. eapply max_reg_stmnt_not_modified with (r := max_reg_module m + 2) in R3. - pose proof H18 as R4. eapply max_reg_stmnt_not_modified_nb with (r := max_reg_module m + 2) in R4. - pose proof H17 as R1'. apply max_reg_stmnt_not_modified with (r := max_reg_module m + 6) in R1'. - pose proof H17 as R2'. eapply max_reg_stmnt_not_modified_nb with (r := max_reg_module m + 6) in R2'. - pose proof H18 as R3'. eapply max_reg_stmnt_not_modified with (r := max_reg_module m + 6) in R3'. - pose proof H18 as R4'. eapply max_reg_stmnt_not_modified_nb with (r := max_reg_module m + 6) in R4'. + pose proof H18 as R1. apply max_reg_stmnt_not_modified with (r := max_reg_module m + 2) in R1. + pose proof H18 as R2. eapply max_reg_stmnt_not_modified_nb with (r := max_reg_module m + 2) in R2. + pose proof H19 as R3. eapply max_reg_stmnt_not_modified with (r := max_reg_module m + 2) in R3. + pose proof H19 as R4. eapply max_reg_stmnt_not_modified_nb with (r := max_reg_module m + 2) in R4. + pose proof H18 as R1'. apply max_reg_stmnt_not_modified with (r := max_reg_module m + 6) in R1'. + pose proof H18 as R2'. eapply max_reg_stmnt_not_modified_nb with (r := max_reg_module m + 6) in R2'. + pose proof H19 as R3'. eapply max_reg_stmnt_not_modified with (r := max_reg_module m + 6) in R3'. + pose proof H19 as R4'. eapply max_reg_stmnt_not_modified_nb with (r := max_reg_module m + 6) in R4'. simplify. pose proof DISABLE_RAM as DISABLE_RAM1. eapply int_eq_not_changed with (ar' := rab') in DISABLE_RAM; try congruence. @@ -2577,14 +2646,14 @@ Proof. econstructor; mgen_crush. apply merge_arr_empty; mgen_crush. unfold disable_ram in *. unfold transf_module in DISABLE_RAM. repeat destruct_match; crush. unfold transf_module in Heqo; repeat destruct_match; crush. - pose proof H17 as R1. apply max_reg_stmnt_not_modified with (r := max_reg_module m + 2) in R1. - pose proof H17 as R2. eapply max_reg_stmnt_not_modified_nb with (r := max_reg_module m + 2) in R2. - pose proof H18 as R3. eapply max_reg_stmnt_not_modified with (r := max_reg_module m + 2) in R3. - pose proof H18 as R4. eapply max_reg_stmnt_not_modified_nb with (r := max_reg_module m + 2) in R4. - pose proof H17 as R1'. apply max_reg_stmnt_not_modified with (r := max_reg_module m + 6) in R1'. - pose proof H17 as R2'. eapply max_reg_stmnt_not_modified_nb with (r := max_reg_module m + 6) in R2'. - pose proof H18 as R3'. eapply max_reg_stmnt_not_modified with (r := max_reg_module m + 6) in R3'. - pose proof H18 as R4'. eapply max_reg_stmnt_not_modified_nb with (r := max_reg_module m + 6) in R4'. + pose proof H18 as R1. apply max_reg_stmnt_not_modified with (r := max_reg_module m + 2) in R1. + pose proof H18 as R2. eapply max_reg_stmnt_not_modified_nb with (r := max_reg_module m + 2) in R2. + pose proof H19 as R3. eapply max_reg_stmnt_not_modified with (r := max_reg_module m + 2) in R3. + pose proof H19 as R4. eapply max_reg_stmnt_not_modified_nb with (r := max_reg_module m + 2) in R4. + pose proof H18 as R1'. apply max_reg_stmnt_not_modified with (r := max_reg_module m + 6) in R1'. + pose proof H18 as R2'. eapply max_reg_stmnt_not_modified_nb with (r := max_reg_module m + 6) in R2'. + pose proof H19 as R3'. eapply max_reg_stmnt_not_modified with (r := max_reg_module m + 6) in R3'. + pose proof H19 as R4'. eapply max_reg_stmnt_not_modified_nb with (r := max_reg_module m + 6) in R4'. simplify. pose proof DISABLE_RAM as DISABLE_RAM1. eapply int_eq_not_changed with (ar' := rab') in DISABLE_RAM; try congruence. @@ -2600,7 +2669,7 @@ Proof. eapply max_reg_module_datapath_gt; eauto; remember (max_reg_module m); lia. eapply max_reg_module_controllogic_gt; eauto; remember (max_reg_module m); lia. eapply max_reg_module_controllogic_gt; eauto; remember (max_reg_module m); lia. - - unfold alt_store in *; simplify. inv H6. inv H19. inv H19. simplify. + - unfold alt_store in *; simplify. inv H6. inv H20. inv H20. simplify. exploit match_states_same; try solve [eapply H4 | eapply max_stmnt_lt_module; eauto | econstructor; eauto with mgen]; intros; repeat inv_exists; simplify; tac0. @@ -2618,14 +2687,14 @@ Proof. pose proof H3 as X. apply max_reg_stmnt_le_stmnt_tree in X. apply expr_lt_max_module_datapath in X. remember (max_reg_module m); simplify; lia. - + unfold transf_module; repeat destruct_match; crush. constructor. rewrite empty_stack_transf. unfold transf_module; repeat destruct_match; try discriminate; simplify; []. eapply exec_ram_Some_write. 3: { simplify. unfold merge_regs. repeat rewrite AssocMapExt.merge_add_assoc. repeat rewrite find_assocmap_gso by lia. - pose proof H12 as X. + pose proof H13 as X. eapply max_reg_stmnt_not_modified_nb with (r := (max_reg_module m + 2)) in X. rewrite AssocMap.gempty in X. apply merge_find_assocmap. auto. @@ -2639,8 +2708,8 @@ Proof. { unfold disable_ram in *. unfold transf_module in DISABLE_RAM; repeat destruct_match; try discriminate. simplify. - pose proof H12 as X2. - pose proof H12 as X4. + pose proof H13 as X2. + pose proof H13 as X4. apply max_reg_stmnt_not_modified with (r := max_reg_module m + 2) in X2. apply max_reg_stmnt_not_modified with (r := max_reg_module m + 6) in X4. assert (forall ar ar' x, ar ! x = ar' ! x -> ar # x = ar' # x). @@ -2672,10 +2741,10 @@ Proof. unfold transf_module; repeat destruct_match; try discriminate; simplify. replace (AssocMapExt.merge value ran' rab') with (merge_regs ran' rab'); [|unfold merge_regs; auto]. - pose proof H19 as X. + pose proof H20 as X. eapply match_assocmaps_merge in X. - 2: { apply H21. } - inv X. rewrite <- H14. eassumption. unfold transf_module in H6; repeat destruct_match; + 2: apply H22. + inv X. rewrite <- H12. eassumption. unfold transf_module in H6; repeat destruct_match; try discriminate; simplify. lia. auto. @@ -2692,9 +2761,9 @@ Proof. apply match_arrs_merge_set2; auto. eapply match_arrs_size_stmnt_preserved in H4; mgen_crush. eapply match_arrs_size_stmnt_preserved in H4; mgen_crush. - eapply match_arrs_size_stmnt_preserved in H12; mgen_crush. + eapply match_arrs_size_stmnt_preserved in H13; mgen_crush. rewrite empty_stack_transf. mgen_crush. - eapply match_arrs_size_stmnt_preserved in H12; mgen_crush. + eapply match_arrs_size_stmnt_preserved in H13; mgen_crush. rewrite empty_stack_transf. mgen_crush. auto. apply merge_arr_empty_match. @@ -2702,7 +2771,7 @@ Proof. eapply match_arrs_size_stmnt_preserved in H4; mgen_crush. eapply match_arrs_size_stmnt_preserved in H4; mgen_crush. apply match_empty_size_merge. apply match_empty_assocmap_set. - mgen_crush. eapply match_arrs_size_stmnt_preserved in H12; mgen_crush. + mgen_crush. eapply match_arrs_size_stmnt_preserved in H13; mgen_crush. rewrite empty_stack_transf; mgen_crush. unfold disable_ram. unfold transf_module; repeat destruct_match; try discriminate; simplify. unfold merge_regs. unfold_merge. @@ -2713,7 +2782,7 @@ Proof. - unfold alt_load in *; simplify. inv H6. 2: { match goal with H: context[location_is] |- _ => inv H end. } match goal with H: context[location_is] |- _ => inv H end. - inv H30. simplify. inv H4. + inv H31. simplify. inv H4. 2: { match goal with H: context[location_is] |- _ => inv H end. } inv H27. simplify. do 2 econstructor. eapply Smallstep.plus_two. @@ -2728,7 +2797,8 @@ Proof. apply expr_lt_max_module_datapath in X. simplify. remember (max_reg_module m); lia. auto. - simplify. rewrite empty_stack_transf. unfold transf_module; repeat destruct_match; crush. + simplify. unfold transf_module; repeat destruct_match; crush. constructor. + rewrite empty_stack_transf. unfold transf_module; repeat destruct_match; crush. eapply exec_ram_Some_read; simplify. 2: { unfold merge_regs. unfold_merge. repeat rewrite find_assocmap_gso; try (remember (max_reg_module m); lia). @@ -2766,7 +2836,7 @@ Proof. end; lia. } repeat rewrite AssocMap.gso by lia. - inv ASSOC. rewrite <- H19. auto. lia. + inv ASSOC. rewrite <- H20. auto. lia. } { unfold merge_regs. unfold_merge. assert (mod_finish m < max_reg_module m + 1). @@ -2779,7 +2849,7 @@ Proof. end; lia. } repeat rewrite AssocMap.gso by lia. - inv ASSOC. rewrite <- H19. auto. lia. + inv ASSOC. rewrite <- H20. auto. lia. } { unfold merge_regs. unfold_merge. assert (mod_st m < max_reg_module m + 1). @@ -2825,7 +2895,8 @@ Proof. unfold merge_regs; unfold_merge. repeat rewrite find_assocmap_gso by lia. apply find_assocmap_gss. } - { simplify. rewrite empty_stack_transf. + { simplify. unfold transf_module; repeat destruct_match; crush. constructor. } + { rewrite empty_stack_transf. unfold transf_module; repeat destruct_match; try discriminate; simplify. econstructor. simplify. unfold merge_regs; unfold_merge. simplify. @@ -2851,7 +2922,7 @@ Proof. simplify. lia. } unfold merge_regs in H8. repeat rewrite AssocMapExt.merge_add_assoc in H8. - simplify. rewrite AssocMap.gso in H8 by lia. rewrite AssocMap.gss in H8. + simplify. rewrite AssocMap.gso in H8 by lia. inv H28. rewrite AssocMap.gss in H8. unfold transf_module; repeat destruct_match; try discriminate; simplify. repeat rewrite AssocMap.gso by lia. apply AssocMap.gss. } @@ -2862,7 +2933,7 @@ Proof. { unfold merge_regs. unfold_merge. simplify. apply match_assocmaps_gss. unfold merge_regs in H8. repeat rewrite AssocMapExt.merge_add_assoc in H8. - rewrite AssocMap.gso in H8. rewrite AssocMap.gss in H8. inv H8. + rewrite AssocMap.gso in H8. inv H28. rewrite AssocMap.gss in H8. inv H8. remember (max_reg_module m). assert (mod_st m < max_reg_module m + 1). { unfold max_reg_module; lia. } @@ -2912,7 +2983,8 @@ Proof. rewrite find_assocmap_gss. apply Int.eq_true. } } -Qed. + - auto. +Admitted. Lemma exec_ram_resets_en : forall rs ar rs' ar' r, @@ -3020,7 +3092,8 @@ Section CORRECTNESS. end. induction 1; destruct (mod_ram m) eqn:RAM; simplify; repeat transf_step_correct_assum; repeat transf_step_correct_tac. - - assert (MATCH_SIZE1: match_empty_size m nasa1 /\ match_empty_size m basa1). + - + assert (MATCH_SIZE1: match_empty_size m nasa1 /\ match_empty_size m basa1). { eapply match_arrs_size_stmnt_preserved2; eauto. unfold match_empty_size; mgen_crush. } simplify. assert (MATCH_SIZE2: match_empty_size m nasa2 /\ match_empty_size m basa2). diff --git a/src/hls/Verilog.v b/src/hls/Verilog.v index 1dc7e99..7645a00 100644 --- a/src/hls/Verilog.v +++ b/src/hls/Verilog.v @@ -267,6 +267,20 @@ Inductive module_item : Type := - [mod_body] The body of the module, including the state machine. *) + +Record div := mk_div { + div_a: reg; + div_b: reg; + div_q: reg; + div_r: reg; + div_u_en: reg; + div_en: reg; + div_done: reg; + div_ordering: (div_a < div_b < div_q + /\ div_q < div_r < div_u_en + /\ div_u_en < div_en < div_done)%positive + }. + Record module : Type := mkmodule { mod_start : reg; mod_reset : reg; @@ -279,6 +293,7 @@ Record module : Type := mkmodule { mod_args : list reg; mod_body : list module_item; mod_entrypoint : node; + mod_div : option div; }. Definition fundef := AST.fundef module. @@ -578,10 +593,39 @@ Definition genv := Globalenvs.Genv.t fundef unit. Definition empty_stack (m : module) : assocmap_arr := (AssocMap.set m.(mod_stk) (Array.arr_repeat None m.(mod_stk_len)) (AssocMap.empty arr)). +Inductive exec_div : + Verilog.reg_associations -> option div -> Verilog.reg_associations -> Prop := +| exec_div_Some_idle: + forall r d, + Int.eq (Verilog.assoc_blocking r)#(div_en d, 32) + (Verilog.assoc_blocking r)#(div_u_en d, 32) = true -> + Int.eq ((Verilog.assoc_blocking r)#(div_done d, 32)) (ZToValue 0) = true -> + exec_div r (Some d) r +| exec_div_Some_input: + forall r d u_en en don, + Int.eq en u_en = false -> + Int.eq don (ZToValue 0) = true -> + (Verilog.assoc_blocking r)#(div_done d, 32) = don -> + (Verilog.assoc_blocking r)#(div_en d, 32) = en -> + (Verilog.assoc_blocking r)!(div_u_en d) = Some u_en -> + exec_div r (Some d) (Verilog.nonblock_reg (div_en d) + (Verilog.nonblock_reg (div_done d) r (ZToValue 1)) u_en) +| exec_div_Some_output: + forall r d don a b, + Int.eq don (ZToValue 0) = false -> + (Verilog.assoc_blocking r)#(div_done d, 32) = don -> + (Verilog.assoc_blocking r)!(div_a d) = Some a -> + (Verilog.assoc_blocking r)!(div_b d) = Some b -> + exec_div r (Some d) (Verilog.nonblock_reg (div_done d) + (Verilog.nonblock_reg (div_r d) + (Verilog.nonblock_reg (div_q d) r (Int.divs a b)) (Int.mods a b)) + (ZToValue 0)) +| exec_div_None: forall r, exec_div r None r. + Inductive step : genv -> state -> Events.trace -> state -> Prop := | step_module : - forall asr asa asr' asa' basr1 nasr1 basa1 nasa1 basr2 nasr2 - basa2 nasa2 f stval pstval m sf st g ist, + forall asr asa asr' asa' basr1 nasr1 basr1' nasr1' basa1 + nasa1 basr2 nasr2 basa2 nasa2 f stval pstval m sf st g ist, asr!(m.(mod_reset)) = Some (ZToValue 0) -> asr!(m.(mod_finish)) = Some (ZToValue 0) -> asr!(m.(mod_st)) = Some ist -> @@ -591,7 +635,8 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := (mod_body m) (mkassociations basr1 nasr1) (mkassociations basa1 nasa1) -> - mis_stepp_negedge f (mkassociations (merge_regs nasr1 basr1) empty_assocmap) + exec_div (mkassociations basr1 nasr1) (mod_div m) (mkassociations basr1' nasr1') -> + mis_stepp_negedge f (mkassociations (merge_regs nasr1' basr1') empty_assocmap) (mkassociations (merge_arrs nasa1 basa1) (empty_stack m)) (mod_body m) (mkassociations basr2 nasr2) @@ -807,14 +852,38 @@ Proof. end; crush). Qed. +Lemma exec_div_determinate : + forall asr0 d asr1, + exec_div asr0 d asr1 -> + forall asr1', + exec_div asr0 d asr1' -> + asr1' = asr1. +Proof. + induction 1; intros. + - inv H1. auto. unfold find_assocmap, AssocMapExt.get_default in *. + rewrite H8 in H. rewrite H3 in H. discriminate. + unfold find_assocmap, AssocMapExt.get_default in *. + rewrite H3 in H0. discriminate. + - inv H4. unfold find_assocmap, AssocMapExt.get_default in *. rewrite H3 in H6. + rewrite H6 in H. discriminate. + rewrite H3 in H11. inv H11. auto. + unfold find_assocmap, AssocMapExt.get_default in *. + rewrite H6 in H0. discriminate. + - inv H3. rewrite H7 in H. discriminate. + rewrite H6 in H. discriminate. + rewrite H7 in H1. rewrite H9 in H2. inv H1. inv H2. auto. + - inv H. auto. +Qed. + Lemma semantics_determinate : forall (p: program), Smallstep.determinate (semantics p). Proof. intros. constructor; set (ge := Globalenvs.Genv.globalenv p); simplify. - invert H; invert H0; constructor. (* Traces are always empty *) - invert H; invert H0; crush. assert (f = f0) by (destruct f; destruct f0; auto); subst. - pose proof (mis_stepp_determinate H5 H15). simplify. inv H0. inv H4. - pose proof (mis_stepp_negedge_determinate H6 H17). + pose proof (mis_stepp_determinate H5 H16). simplify. inv H0. inv H4. + pose proof (exec_div_determinate H6 H17). simplify. inv H. + pose proof (mis_stepp_negedge_determinate H7 H19). crush. - constructor. invert H; crush. - invert H; invert H0; unfold ge0, ge1 in *; crush. -- cgit