diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-06-25 18:15:09 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-06-25 18:15:09 +0100 |
| commit | ea0f077891a3935f1138f14796b323b1a9bdab1f (patch) | |
| tree | 976543faa2fd61fb62daaefddb5d97dcf4899f50 | |
| parent | 75c75c52cdaa71b268f0fadc4c31aba0e099abbc (diff) | |
| download | vericert-ea0f077891a3935f1138f14796b323b1a9bdab1f.tar.gz vericert-ea0f077891a3935f1138f14796b323b1a9bdab1f.zip | |
Add optimisations
| -rw-r--r-- | src/Compiler.v | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/src/Compiler.v b/src/Compiler.v index 98ef429..f9fe686 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -76,11 +76,27 @@ 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 @@ Veriloggen.transl_program. +(* Unoptimised below: *) +(*Definition transf_backend (r : RTL.program) : res Verilog.program := + OK r + @@@ Inlining.transf_program + @@ print (print_RTL 1) + @@@ HTLgen.transl_program + @@ Veriloggen.transl_program. +*) + Definition transf_frontend (p: Csyntax.program) : res RTL.program := OK p @@@ SimplExpr.transl_program |