diff options
| author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-01-25 13:50:10 +0200 |
|---|---|---|
| committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-01-25 13:50:10 +0200 |
| commit | 2181eac18441168f773e3391c4671619f4339ee6 (patch) | |
| tree | 87fbb4c83af5199325027a69ad983f3a9f9f3890 /src/Compiler.v | |
| parent | 9404debd87728ab9b78f8bfed68a758ee03520e3 (diff) | |
| download | vericert-2181eac18441168f773e3391c4671619f4339ee6.tar.gz vericert-2181eac18441168f773e3391c4671619f4339ee6.zip | |
Implement renumbering (wrong)
Diffstat (limited to 'src/Compiler.v')
| -rw-r--r-- | src/Compiler.v | 20 |
1 files changed, 12 insertions, 8 deletions
diff --git a/src/Compiler.v b/src/Compiler.v index 3daa713..a643074 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -86,7 +86,7 @@ Definition transf_backend (r : RTL.program) : res Verilog.program := (* @@ print (print_RTL 1) *) @@@ HTLgen.transl_program @@ print print_HTL - @@ Veriloggen.transl_program. + @@@ Veriloggen.transl_program. Definition transf_hls (p : Csyntax.program) : res Verilog.program := OK p @@ -101,6 +101,9 @@ Definition transf_hls (p : Csyntax.program) : res Verilog.program := Local Open Scope linking_scope. +Definition verilog_transflink : TransfLink Veriloggenproof.match_prog. +Admitted. + Definition CompCert's_passes := mkpass SimplExprproof.match_prog ::: mkpass SimplLocalsproof.match_prog @@ -109,7 +112,7 @@ Definition CompCert's_passes := ::: mkpass Selectionproof.match_prog ::: mkpass RTLgenproof.match_prog ::: (@mkpass _ _ HTLgenproof.match_prog (HTLgenproof.TransfHTLLink HTLgen.transl_program)) - ::: mkpass Veriloggenproof.match_prog + ::: (@mkpass _ _ Veriloggenproof.match_prog verilog_transflink) ::: pass_nil _. Definition match_prog: Csyntax.program -> Verilog.program -> Prop := @@ -132,7 +135,7 @@ Proof. 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 p6) as [p7|e] eqn:P7; simpl in T; try discriminate. - set (p8 := Veriloggen.transl_program p7) in *. + destruct (Veriloggen.transl_program p7) as [p8|e] eqn:P8; simpl in T; try discriminate. unfold match_prog; simpl. exists p1; split. apply SimplExprproof.transf_program_match; auto. exists p2; split. apply SimplLocalsproof.match_transf_program; auto. @@ -142,9 +145,9 @@ Proof. exists p6; split. apply RTLgenproof.transf_program_match; auto. (* exists p7; split. apply Inliningproof.transf_program_match; auto. *) exists p7; split. apply HTLgenproof.transf_program_match; auto. - exists p8; split. apply Veriloggenproof.transf_program_match; auto. - inv T. reflexivity. -Qed. + (* exists p8; split. apply Veriloggenproof.transf_program_match; auto. *) + (* inv T. reflexivity. *) +Admitted. Remark forward_simulation_identity: forall sem, forward_simulation sem sem. @@ -187,14 +190,15 @@ Ltac DestructM := eapply RTLgenproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply HTLgenproof.transf_program_correct. eassumption. - eapply Veriloggenproof.transf_program_correct; eassumption. + (* eapply Veriloggenproof.transf_program_correct; eassumption. *) + admit. } 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. +Admitted. Theorem c_semantic_preservation: forall p tp, |