diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-11-18 22:14:30 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-11-18 22:14:30 +0000 |
| commit | 3c5bd88f22f744e4908afbc5a56e202dfa469360 (patch) | |
| tree | 57ddb252b09bdc61665fcab97ff169acc9af23e7 /src/Compiler.v | |
| parent | e6348c97faee39754efd13b69a70c54851e2a789 (diff) | |
| download | vericert-3c5bd88f22f744e4908afbc5a56e202dfa469360.tar.gz vericert-3c5bd88f22f744e4908afbc5a56e202dfa469360.zip | |
Fix compilation with new HTL language
Diffstat (limited to 'src/Compiler.v')
| -rw-r--r-- | src/Compiler.v | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/src/Compiler.v b/src/Compiler.v index 0ac2b80..e4ab607 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -196,8 +196,8 @@ Definition transf_backend (r : RTL.program) : res Verilog.program := @@ print (print_RTL 7) @@@ HTLgen.transl_program @@ print (print_HTL 0) - @@ total_if HLSOpts.optim_ram Memorygen.transf_program - @@ print (print_HTL 1) +(* @@ total_if HLSOpts.optim_ram Memorygen.transf_program + @@ print (print_HTL 1)*) @@ Veriloggen.transl_program. (*| @@ -279,7 +279,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 (match_if HLSOpts.optim_ram Memorygen.match_prog)*) ::: mkpass Veriloggenproof.match_prog ::: pass_nil _. @@ -317,8 +317,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 := total_if HLSOpts.optim_ram Memorygen.transf_program p14) in *. - set (p16 := Veriloggen.transl_program p15) in *. + (*set (p15 := total_if HLSOpts.optim_ram Memorygen.transf_program p14) in *.*) + set (p15 := Veriloggen.transl_program p14) in *. unfold match_prog; simpl. exists p1; split. apply SimplExprproof.transf_program_match; auto. exists p2; split. apply SimplLocalsproof.match_transf_program; auto. @@ -334,8 +334,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 total_if_match. apply Memorygen.transf_program_match; auto. - exists p16; split. apply Veriloggenproof.transf_program_match; auto. + (*exists p15; split. apply total_if_match. apply Memorygen.transf_program_match; auto.*) + exists p15; split. apply Veriloggenproof.transf_program_match; auto. inv T. reflexivity. Qed. @@ -353,7 +353,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 p16)). + assert (F: forward_simulation (Cstrategy.semantics p) (Verilog.semantics p15)). { eapply compose_forward_simulations. eapply SimplExprproof.transl_program_correct; eassumption. @@ -383,8 +383,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 compose_forward_simulations. + eapply match_if_simulation. eassumption. exact Memorygen.transf_program_correct; eassumption.*) eapply Veriloggenproof.transf_program_correct; eassumption. } split. auto. |