diff options
Diffstat (limited to 'src/Compiler.v')
| -rw-r--r-- | src/Compiler.v | 34 |
1 files changed, 22 insertions, 12 deletions
diff --git a/src/Compiler.v b/src/Compiler.v index e9d76dc..ff0938e 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -65,11 +65,13 @@ Require vericert.hls.HTLgen. Require vericert.hls.RTLBlock. Require vericert.hls.RTLBlockgen. Require vericert.hls.RTLPargen. +Require vericert.hls.RTLParFUgen. Require vericert.hls.HTLPargen. Require vericert.hls.Pipeline. Require vericert.hls.IfConversion. -Require vericert.hls.PipelineOp. +(*Require vericert.hls.PipelineOp.*) Require vericert.HLSOpts. +Require vericert.hls.Memorygen. Require Import vericert.hls.HTLgenproof. @@ -81,7 +83,7 @@ We then need to declare the external OCaml functions used to print out intermedi |*) Parameter print_RTL: Z -> RTL.program -> unit. -Parameter print_HTL: HTL.program -> unit. +Parameter print_HTL: Z -> HTL.program -> unit. Parameter print_RTLBlock: Z -> RTLBlock.program -> unit. Parameter print_RTLPar: Z -> RTLPar.program -> unit. @@ -192,7 +194,9 @@ Definition transf_backend (r : RTL.program) : res Verilog.program := @@@ time "Unused globals" Unusedglob.transform_program @@ print (print_RTL 7) @@@ HTLgen.transl_program - @@ print print_HTL + @@ print (print_HTL 0) + @@ total_if HLSOpts.optim_ram Memorygen.transf_program + @@ print (print_HTL 1) @@ Veriloggen.transl_program. (*| @@ -214,6 +218,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 @@ -237,15 +243,14 @@ Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program := @@@ time "Unused globals" Unusedglob.transform_program @@ print (print_RTL 7) @@@ RTLBlockgen.transl_program - @@ print (print_RTLBlock 1) + @@ print (print_RTLBlock 0) @@ total_if HLSOpts.optim_if_conversion IfConversion.transf_program - @@ print (print_RTLBlock 2) + @@ print (print_RTLBlock 1) @@@ RTLPargen.transl_program - @@ print (print_RTLPar 1) - @@ PipelineOp.transf_program - @@ print (print_RTLPar 2) + @@ print (print_RTLPar 0) + @@@ RTLParFUgen.transl_program @@@ HTLPargen.transl_program - @@ print print_HTL + @@ print (print_HTL 0) @@ Veriloggen.transl_program. (*| @@ -272,6 +277,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 _. @@ -309,7 +315,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. @@ -325,7 +332,8 @@ 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. + 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. @@ -343,7 +351,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. @@ -373,6 +381,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. |