From dfaa3a9cbc07649feea3220693a8a854a32eafb6 Mon Sep 17 00:00:00 2001 From: Michalis Pardalos Date: Mon, 16 Nov 2020 20:26:28 +0000 Subject: Generate (invalid) module instantiations for calls --- src/Compiler.v | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'src/Compiler.v') diff --git a/src/Compiler.v b/src/Compiler.v index 6efd7a2..80aae3f 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -82,7 +82,6 @@ Qed. Definition transf_backend (r : RTL.program) : res Verilog.program := OK r - @@@ Inlining.transf_program @@ print (print_RTL 1) @@@ HTLgen.transl_program @@ print print_HTL @@ -144,8 +143,8 @@ Proof. 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. + inv T. (* reflexivity. *) +Admitted. Remark forward_simulation_identity: forall sem, forward_simulation sem sem. -- cgit From 130d11a3291e3bce761ecbaeb7185df4ea98009d Mon Sep 17 00:00:00 2001 From: Michalis Pardalos Date: Fri, 27 Nov 2020 12:51:20 +0000 Subject: Revert changes relating to instance generation Revert "Add todo for missing logic around instantiations" This reverts commit 303a45374643f75698c61f062899973d2c297831. Revert "Add wires and use them for output of instances" This reverts commit a72f26319dabca414a2b576424b9f72afaca161c. Revert "Separate HTL instantiations from Verilog ones" This reverts commit 653c8729f4322f538aa7116c5e311c884b3c5047. Revert "Translate instantiations from HTL to verilog" This reverts commit 982e6c69a52e8ec4e677147004cc5472f8a80d6d. Revert "Print instantiations in HTL output" This reverts commit 9b87637d3e4d6a75dee1221b017e3ccf6632642e. Revert "Add a field in HTL modules for instances" This reverts commit d79dae026b150e9671e0aa7262f6aa2d1d302502. Revert "Generate (invalid) module instantiations for calls" This reverts commit dfaa3a9cbc07649feea3220693a8a854a32eafb6. --- src/Compiler.v | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'src/Compiler.v') diff --git a/src/Compiler.v b/src/Compiler.v index 80aae3f..6efd7a2 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -82,6 +82,7 @@ Qed. Definition transf_backend (r : RTL.program) : res Verilog.program := OK r + @@@ Inlining.transf_program @@ print (print_RTL 1) @@@ HTLgen.transl_program @@ print print_HTL @@ -143,8 +144,8 @@ Proof. 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. *) -Admitted. + inv T. reflexivity. +Qed. Remark forward_simulation_identity: forall sem, forward_simulation sem sem. -- cgit From 753ec32951d1a6bbf3d93e02e28e58daa3a070f9 Mon Sep 17 00:00:00 2001 From: Michalis Pardalos Date: Mon, 30 Nov 2020 11:58:14 +0000 Subject: Add a call instruction to HTL. Use it for Icall. --- src/Compiler.v | 56 ++++++++++++++++++++++++++++---------------------------- 1 file changed, 28 insertions(+), 28 deletions(-) (limited to 'src/Compiler.v') diff --git a/src/Compiler.v b/src/Compiler.v index 6efd7a2..2e190f9 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -82,8 +82,8 @@ Qed. Definition transf_backend (r : RTL.program) : res Verilog.program := OK r - @@@ Inlining.transf_program - @@ print (print_RTL 1) + (* @@@ Inlining.transf_program *) + (* @@ print (print_RTL 1) *) @@@ HTLgen.transl_program @@ print print_HTL @@ Veriloggen.transl_program. @@ -120,32 +120,32 @@ Theorem transf_hls_match: forall p tp, transf_hls p = OK tp -> match_prog p tp. -Proof. - intros p tp 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. - exists p3; split. apply Cshmgenproof.transf_program_match; auto. - 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. - 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. +Proof. Admitted. + (* intros p tp 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. *) + (* exists p3; split. apply Cshmgenproof.transf_program_match; auto. *) + (* 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. *) + (* 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. -- cgit From 0cbfa55ea4b91d00134ec2c4f6b13d7814ecd9d6 Mon Sep 17 00:00:00 2001 From: Michalis Pardalos Date: Tue, 1 Dec 2020 10:45:52 +0000 Subject: Get top-level proofs passing. Needed change because inlining was removed. --- src/Compiler.v | 54 ++++++++++++++++++++++++++---------------------------- 1 file changed, 26 insertions(+), 28 deletions(-) (limited to 'src/Compiler.v') diff --git a/src/Compiler.v b/src/Compiler.v index 2e190f9..3daa713 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -108,7 +108,6 @@ Definition CompCert's_passes := ::: mkpass Cminorgenproof.match_prog ::: mkpass Selectionproof.match_prog ::: mkpass RTLgenproof.match_prog - ::: mkpass Inliningproof.match_prog ::: (@mkpass _ _ HTLgenproof.match_prog (HTLgenproof.TransfHTLLink HTLgen.transl_program)) ::: mkpass Veriloggenproof.match_prog ::: pass_nil _. @@ -120,32 +119,32 @@ Theorem transf_hls_match: forall p tp, transf_hls p = OK tp -> match_prog p tp. -Proof. Admitted. - (* intros p tp 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. *) +Proof. + intros p tp 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. *) - (* exists p3; split. apply Cshmgenproof.transf_program_match; auto. *) - (* 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. *) + destruct (HTLgen.transl_program p6) as [p7|e] eqn:P7; simpl in T; try discriminate. + set (p8 := Veriloggen.transl_program p7) in *. + unfold match_prog; simpl. + exists p1; split. apply SimplExprproof.transf_program_match; auto. + exists p2; split. apply SimplLocalsproof.match_transf_program; auto. + exists p3; split. apply Cshmgenproof.transf_program_match; auto. + 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. (* 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. *) + exists p7; split. apply HTLgenproof.transf_program_match; auto. + exists p8; split. apply Veriloggenproof.transf_program_match; auto. + inv T. reflexivity. +Qed. Remark forward_simulation_identity: forall sem, forward_simulation sem sem. @@ -164,6 +163,7 @@ Theorem cstrategy_semantic_preservation: /\ 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, _ /\ _ |- _ ] => @@ -171,7 +171,7 @@ Ltac DestructM := destruct H as (p & M & MM); clear H end. repeat DestructM. subst tp. - assert (F: forward_simulation (Cstrategy.semantics p) (Verilog.semantics p9)). + assert (F: forward_simulation (Cstrategy.semantics p) (Verilog.semantics p8)). { eapply compose_forward_simulations. eapply SimplExprproof.transl_program_correct; eassumption. @@ -185,8 +185,6 @@ Ltac DestructM := 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. -- cgit From 2181eac18441168f773e3391c4671619f4339ee6 Mon Sep 17 00:00:00 2001 From: Michalis Pardalos Date: Mon, 25 Jan 2021 13:50:10 +0200 Subject: Implement renumbering (wrong) --- src/Compiler.v | 20 ++++++++++++-------- 1 file changed, 12 insertions(+), 8 deletions(-) (limited to 'src/Compiler.v') 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, -- cgit