From 128b5d3a20647db3d0b17cc918d17fe5cadc07ff Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 6 Jul 2020 23:27:05 +0100 Subject: Add top level backward simulation --- src/Compiler.v | 127 ++++++++++++++++++++++++++++++++++++++++++++++++++------- 1 file changed, 112 insertions(+), 15 deletions(-) (limited to 'src/Compiler.v') diff --git a/src/Compiler.v b/src/Compiler.v index 17d8921..05353f9 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -16,6 +16,8 @@ * along with this program. If not, see . *) +From coqup Require Import HTLgenproof. + From compcert.common Require Import Errors Linking. @@ -49,8 +51,9 @@ From coqup Require Verilog Veriloggen Veriloggenproof - HTLgen - HTLgenproof. + HTLgen. + +From compcert Require Import Smallstep. Parameter print_RTL: Z -> RTL.program -> unit. Parameter print_HTL: HTL.program -> unit. @@ -85,7 +88,9 @@ Definition transf_backend (r : RTL.program) : res Verilog.program := @@ print print_HTL @@ Veriloggen.transl_program. -Definition transf_frontend (p: Csyntax.program) : res RTL.program := +Check mkpass. + +Definition transf_hls (p : Csyntax.program) : res Verilog.program := OK p @@@ SimplExpr.transl_program @@@ SimplLocals.transf_program @@ -93,11 +98,6 @@ Definition transf_frontend (p: Csyntax.program) : res RTL.program := @@@ Cminorgen.transl_program @@@ Selection.sel_program @@@ RTLgen.transl_program - @@ print (print_RTL 0). - -Definition transf_hls (p : Csyntax.program) : res Verilog.program := - OK p - @@@ transf_frontend @@@ transf_backend. Local Open Scope linking_scope. @@ -110,27 +110,30 @@ Definition CompCert's_passes := ::: mkpass Selectionproof.match_prog ::: mkpass RTLgenproof.match_prog ::: mkpass Inliningproof.match_prog - ::: mkpass HTLgenproof.match_prog + ::: (@mkpass _ _ HTLgenproof.match_prog (HTLgenproof.TransfHTLLink HTLgen.transl_program)) ::: mkpass Veriloggenproof.match_prog ::: pass_nil _. -Definition match_prog: Csyntax.program -> RTL.program -> Prop := +Definition match_prog: Csyntax.program -> Verilog.program -> Prop := pass_match (compose_passes CompCert's_passes). -Theorem transf_frontend_match: +Theorem transf_hls_match: forall p tp, - transf_frontend p = OK tp -> + transf_hls p = OK tp -> match_prog p tp. Proof. intros p tp T. - unfold transf_frontend in T. simpl in T. + unfold transf_hls in T. simpl in T. destruct (SimplExpr.transl_program p) as [p1|e] eqn:P1; simpl in T; try discriminate. destruct (SimplLocals.transf_program p1) as [p2|e] eqn:P2; simpl in T; try discriminate. destruct (Cshmgen.transl_program p2) as [p3|e] eqn:P3; simpl in T; try discriminate. destruct (Cminorgen.transl_program p3) as [p4|e] eqn:P4; simpl in T; try discriminate. destruct (Selection.sel_program p4) as [p5|e] eqn:P5; simpl in T; try discriminate. - rewrite ! compose_print_identity in T. destruct (RTLgen.transl_program p5) as [p6|e] eqn:P6; simpl in T; try discriminate. + unfold transf_backend in T. simpl in T. rewrite ! compose_print_identity in T. + destruct (Inlining.transf_program p6) as [p7|e] eqn:P7; simpl in T; try discriminate. + destruct (HTLgen.transl_program p7) as [p8|e] eqn:P8; simpl in T; try discriminate. + set (p9 := Veriloggen.transl_program p8) in *. unfold match_prog; simpl. exists p1; split. apply SimplExprproof.transf_program_match; auto. exists p2; split. apply SimplLocalsproof.match_transf_program; auto. @@ -138,5 +141,99 @@ Proof. exists p4; split. apply Cminorgenproof.transf_program_match; auto. exists p5; split. apply Selectionproof.transf_program_match; auto. exists p6; split. apply RTLgenproof.transf_program_match; auto. - inversion T. reflexivity. + exists p7; split. apply Inliningproof.transf_program_match; auto. + exists p8; split. apply HTLgenproof.transf_program_match; auto. + exists p9; split. apply Veriloggenproof.transf_program_match; auto. + inv T. reflexivity. +Qed. + +Remark forward_simulation_identity: + forall sem, forward_simulation sem sem. +Proof. + intros. apply forward_simulation_step with (fun s1 s2 => s2 = s1); intros. +- auto. +- exists s1; auto. +- subst s2; auto. +- subst s2. exists s1'; auto. +Qed. + +Theorem cstrategy_semantic_preservation: + forall p tp, + match_prog p tp -> + forward_simulation (Cstrategy.semantics p) (Verilog.semantics tp) + /\ backward_simulation (atomic (Cstrategy.semantics p)) (Verilog.semantics tp). +Proof. + intros p tp M. unfold match_prog, pass_match in M; simpl in M. +Ltac DestructM := + match goal with + [ H: exists p, _ /\ _ |- _ ] => + let p := fresh "p" in let M := fresh "M" in let MM := fresh "MM" in + destruct H as (p & M & MM); clear H + end. + repeat DestructM. subst tp. + assert (F: forward_simulation (Cstrategy.semantics p) (Verilog.semantics p9)). + { + eapply compose_forward_simulations. + eapply SimplExprproof.transl_program_correct; eassumption. + eapply compose_forward_simulations. + eapply SimplLocalsproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply Cshmgenproof.transl_program_correct; eassumption. + eapply compose_forward_simulations. + eapply Cminorgenproof.transl_program_correct; eassumption. + eapply compose_forward_simulations. + eapply Selectionproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply RTLgenproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply Inliningproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply HTLgenproof.transf_program_correct. eassumption. + eapply Veriloggenproof.transf_program_correct; eassumption. + } + split. auto. + apply forward_to_backward_simulation. + apply factor_forward_simulation. auto. eapply sd_traces. eapply Verilog.semantics_determinate. + apply atomic_receptive. apply Cstrategy.semantics_strongly_receptive. + apply Verilog.semantics_determinate. +Qed. + +Theorem c_semantic_preservation: + forall p tp, + match_prog p tp -> + backward_simulation (Csem.semantics p) (Verilog.semantics tp). +Proof. + intros. + apply compose_backward_simulation with (atomic (Cstrategy.semantics p)). + eapply sd_traces; eapply Verilog.semantics_determinate. + apply factor_backward_simulation. + apply Cstrategy.strategy_simulation. + apply Csem.semantics_single_events. + eapply ssr_well_behaved; eapply Cstrategy.semantics_strongly_receptive. + exact (proj2 (cstrategy_semantic_preservation _ _ H)). +Qed. + +Theorem transf_c_program_correct: + forall p tp, + transf_hls p = OK tp -> + backward_simulation (Csem.semantics p) (Verilog.semantics tp). +Proof. + intros. apply c_semantic_preservation. apply transf_hls_match; auto. +Qed. + +Theorem separate_transf_c_program_correct: + forall c_units asm_units c_program, + nlist_forall2 (fun cu tcu => transf_hls cu = OK tcu) c_units asm_units -> + link_list c_units = Some c_program -> + exists asm_program, + link_list asm_units = Some asm_program + /\ backward_simulation (Csem.semantics c_program) (Verilog.semantics asm_program). +Proof. + intros. + assert (nlist_forall2 match_prog c_units asm_units). + { eapply nlist_forall2_imply. eauto. simpl; intros. apply transf_hls_match; auto. } + assert (exists asm_program, link_list asm_units = Some asm_program /\ match_prog c_program asm_program). + { eapply link_list_compose_passes; eauto. } + destruct H2 as (asm_program & P & Q). + exists asm_program; split; auto. apply c_semantic_preservation; auto. Qed. -- cgit From bfb722caf2d46867779222b45615481e9020f0aa Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 6 Jul 2020 23:28:28 +0100 Subject: Rename asm to verilog --- src/Compiler.v | 19 ++++++++++--------- 1 file changed, 10 insertions(+), 9 deletions(-) (limited to 'src/Compiler.v') diff --git a/src/Compiler.v b/src/Compiler.v index 05353f9..db3a810 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -222,18 +222,19 @@ Proof. Qed. Theorem separate_transf_c_program_correct: - forall c_units asm_units c_program, - nlist_forall2 (fun cu tcu => transf_hls cu = OK tcu) c_units asm_units -> + forall c_units verilog_units c_program, + nlist_forall2 (fun cu tcu => transf_hls cu = OK tcu) c_units verilog_units -> link_list c_units = Some c_program -> - exists asm_program, - link_list asm_units = Some asm_program - /\ backward_simulation (Csem.semantics c_program) (Verilog.semantics asm_program). + exists verilog_program, + link_list verilog_units = Some verilog_program + /\ backward_simulation (Csem.semantics c_program) (Verilog.semantics verilog_program). Proof. intros. - assert (nlist_forall2 match_prog c_units asm_units). + assert (nlist_forall2 match_prog c_units verilog_units). { eapply nlist_forall2_imply. eauto. simpl; intros. apply transf_hls_match; auto. } - assert (exists asm_program, link_list asm_units = Some asm_program /\ match_prog c_program asm_program). + assert (exists verilog_program, link_list verilog_units = Some verilog_program + /\ match_prog c_program verilog_program). { eapply link_list_compose_passes; eauto. } - destruct H2 as (asm_program & P & Q). - exists asm_program; split; auto. apply c_semantic_preservation; auto. + destruct H2 as (verilog_program & P & Q). + exists verilog_program; split; auto. apply c_semantic_preservation; auto. Qed. -- cgit