From 5b121800db192b3d31cb6a245529f876079f442e Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 2 Mar 2021 10:27:43 +0000 Subject: Add option to turn on/off ram inferrence --- src/Compiler.v | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'src/Compiler.v') diff --git a/src/Compiler.v b/src/Compiler.v index d99ce56..4e4665b 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -69,6 +69,7 @@ Require vericert.hls.HTLPargen. Require vericert.hls.Pipeline. Require vericert.hls.IfConversion. Require vericert.HLSOpts. +Require vericert.hls.Memorygen. Require Import vericert.hls.HTLgenproof. @@ -191,6 +192,7 @@ Definition transf_backend (r : RTL.program) : res Verilog.program := @@ print (print_RTL 7) @@@ HTLgen.transl_program @@ print print_HTL + @@ total_if HLSOpts.optim_ram Memorygen.transf_program @@ Veriloggen.transl_program. (*| @@ -321,8 +323,8 @@ Proof. exists p13; split. apply Unusedglobproof.transf_program_match; auto. exists p14; split. apply HTLgenproof.transf_program_match; auto. exists p15; split. apply Veriloggenproof.transf_program_match; auto. - inv T. reflexivity. -Qed. + inv T. Admitted. (*reflexivity. +Qed.*) Theorem cstrategy_semantic_preservation: forall p tp, -- cgit From 1fc4099fc354ce44ca00ed94d73028c347f9b470 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 7 Apr 2021 02:58:02 +0100 Subject: Remove Admitted in the highest of top-levels --- src/Compiler.v | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) (limited to 'src/Compiler.v') diff --git a/src/Compiler.v b/src/Compiler.v index 4e4665b..61adad1 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -269,6 +269,7 @@ Definition CompCert's_passes := ::: mkpass (match_if Compopts.optim_redundancy Deadcodeproof.match_prog) ::: mkpass Unusedglobproof.match_prog ::: (@mkpass _ _ HTLgenproof.match_prog (HTLgenproof.TransfHTLLink HTLgen.transl_program)) + ::: mkpass (match_if HLSOpts.optim_ram Memorygen.match_prog) ::: mkpass Veriloggenproof.match_prog ::: pass_nil _. @@ -306,7 +307,8 @@ Proof. destruct (partial_if Compopts.optim_redundancy Deadcode.transf_program p11) as [p12|e] eqn:P12; simpl in T; try discriminate. destruct (Unusedglob.transform_program p12) as [p13|e] eqn:P13; simpl in T; try discriminate. destruct (HTLgen.transl_program p13) as [p14|e] eqn:P14; simpl in T; try discriminate. - set (p15 := Veriloggen.transl_program p14) in *. + set (p15 := total_if HLSOpts.optim_ram Memorygen.transf_program p14) in *. + set (p16 := Veriloggen.transl_program p15) in *. unfold match_prog; simpl. exists p1; split. apply SimplExprproof.transf_program_match; auto. exists p2; split. apply SimplLocalsproof.match_transf_program; auto. @@ -322,9 +324,10 @@ Proof. exists p12; split. eapply partial_if_match; eauto. apply Deadcodeproof.transf_program_match. exists p13; split. apply Unusedglobproof.transf_program_match; auto. exists p14; split. apply HTLgenproof.transf_program_match; auto. - exists p15; split. apply Veriloggenproof.transf_program_match; auto. - inv T. Admitted. (*reflexivity. -Qed.*) + exists p15; split. apply total_if_match. apply Memorygen.transf_program_match; auto. + exists p16; split. apply Veriloggenproof.transf_program_match; auto. + inv T. reflexivity. +Qed. Theorem cstrategy_semantic_preservation: forall p tp, @@ -340,7 +343,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 p15)). + assert (F: forward_simulation (Cstrategy.semantics p) (Verilog.semantics p16)). { eapply compose_forward_simulations. eapply SimplExprproof.transl_program_correct; eassumption. @@ -370,6 +373,8 @@ Ltac DestructM := eapply Unusedglobproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply HTLgenproof.transf_program_correct. eassumption. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact Memorygen.transf_program_correct; eassumption. eapply Veriloggenproof.transf_program_correct; eassumption. } split. auto. -- cgit From 817aea90deff7f381bf50d0cb7cbfc96c1c9ea7f Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 9 Jul 2021 20:11:46 +0200 Subject: Add docker file and some comments --- src/Compiler.v | 2 ++ 1 file changed, 2 insertions(+) (limited to 'src/Compiler.v') diff --git a/src/Compiler.v b/src/Compiler.v index 61adad1..268f451 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -214,6 +214,8 @@ Definition transf_hls (p : Csyntax.program) : res Verilog.program := .. coq:: none |*) +(* This is an unverified version of transf_hls with some experimental additions such as scheduling +that aren't completed yet. *) Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program := OK p @@@ SimplExpr.transl_program -- cgit From 178a7c4781c96857fe0a33c777da83e769516152 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 11 Jul 2021 15:59:21 +0200 Subject: Remove unnecessary files and proofs --- src/Compiler.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/Compiler.v') diff --git a/src/Compiler.v b/src/Compiler.v index 268f451..de29889 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -216,7 +216,7 @@ Definition transf_hls (p : Csyntax.program) : res Verilog.program := (* This is an unverified version of transf_hls with some experimental additions such as scheduling that aren't completed yet. *) -Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program := +(*Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program := OK p @@@ SimplExpr.transl_program @@@ SimplLocals.transf_program @@ -245,7 +245,7 @@ Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program := @@@ RTLPargen.transl_program @@@ HTLPargen.transl_program @@ print print_HTL - @@ Veriloggen.transl_program. + @@ Veriloggen.transl_program.*) (*| Correctness Proof -- cgit