diff options
Diffstat (limited to 'src/Compiler.v')
| -rw-r--r-- | src/Compiler.v | 13 |
1 files changed, 9 insertions, 4 deletions
diff --git a/src/Compiler.v b/src/Compiler.v index db3a810..0a8617d 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -82,14 +82,19 @@ Qed. Definition transf_backend (r : RTL.program) : res Verilog.program := OK r + @@ Tailcall.transf_program @@@ Inlining.transf_program + @@ Renumber.transf_program + @@ Constprop.transf_program + @@ Renumber.transf_program + @@@ CSE.transf_program + @@@ Deadcode.transf_program + @@@ Unusedglob.transform_program @@ print (print_RTL 1) @@@ HTLgen.transl_program @@ print print_HTL @@ Veriloggen.transl_program. -Check mkpass. - Definition transf_hls (p : Csyntax.program) : res Verilog.program := OK p @@@ SimplExpr.transl_program @@ -144,8 +149,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. |