6 files changed, 88 insertions, 1 deletions
diff --git a/src/Compiler.v b/src/Compiler.v
index 98ef429..a34b359 100644
--- a/src/Compiler.v
+++ b/src/Compiler.v
@@ -51,6 +51,7 @@ From coqup Require
      HTLgen.
 
 Parameter print_RTL: Z -> RTL.program -> unit.
+Parameter print_HTL: HTL.program -> unit.
 
 Definition print {A: Type} (printer: A -> unit) (prog: A) : A :=
   let unused := printer prog in prog.
@@ -79,6 +80,7 @@ Definition transf_backend (r : RTL.program) : res Verilog.program :=
   @@@ Inlining.transf_program
   @@ print (print_RTL 1)
   @@@ HTLgen.transl_program
+  @@ print print_HTL
   @@ Veriloggen.transl_program.
 
 Definition transf_frontend (p: Csyntax.program) : res RTL.program :=
diff --git a/src/CoqupClflags.ml b/src/CoqupClflags.ml
index 83dd31d..5b40ce6 100644
--- a/src/CoqupClflags.ml
+++ b/src/CoqupClflags.ml
@@ -3,3 +3,4 @@ let option_simulate = ref false
 let option_hls = ref true
 let option_debug_hls = ref false
 let option_initial = ref false
+let option_dhtl = ref false
diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v
index ba87af6..df21dc4 100644
--- a/src/extraction/Extraction.v
+++ b/src/extraction/Extraction.v
@@ -128,6 +128,7 @@ Extract Constant Compiler.print_Clight => "PrintClight.print_if".
 Extract Constant Compiler.print_Cminor => "PrintCminor.print_if".
 Extract Constant driver.Compiler.print_RTL => "PrintRTL.print_if".
 Extract Constant Compiler.print_RTL => "PrintRTL.print_if".
+Extract Constant Compiler.print_HTL => "PrintHTL.print_if".
 Extract Constant Compiler.print_LTL => "PrintLTL.print_if".
 Extract Constant Compiler.print_Mach => "PrintMach.print_if".
 Extract Constant Compiler.print => "fun (f: 'a -> unit) (x: 'a) -> f x; x".
diff --git a/src/verilog/PrintHTL.ml b/src/verilog/PrintHTL.ml
new file mode 100644
index 0000000..0bdba51
--- /dev/null
+++ b/src/verilog/PrintHTL.ml
@@ -0,0 +1,81 @@
+(* -*- mode: tuareg -*-
+ * CoqUp: Verified high-level synthesis.
+ * Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ *)
+
+open Value
+open Datatypes
+open Camlcoq
+open AST
+open Clflags
+open Printf
+open Maps
+open AST
+open HTL
+open PrintAST
+open PrintVerilog
+open CoqupClflags
+
+let pstr pp = fprintf pp "%s"
+
+let reg pp r =
+  fprintf pp "x%d" (P.to_int r)
+
+let rec regs pp = function
+  | [] -> ()
+  | [r] -> reg pp r
+  | r1::rl -> fprintf pp "%a, %a" reg r1 regs rl
+
+let print_instruction pp (pc, i) =
+  fprintf pp "%5d:\t%s" pc (pprint_stmnt 0 i)
+
+let print_module pp id f =
+  fprintf pp "%s(%a) {\n" (extern_atom id) regs f.mod_params;
+  let datapath =
+    List.sort
+      (fun (pc1, _) (pc2, _) -> compare pc2 pc1)
+      (List.rev_map
+        (fun (pc, i) -> (P.to_int pc, i))
+        (PTree.elements f.mod_datapath)) in
+  let controllogic =
+    List.sort
+      (fun (pc1, _) (pc2, _) -> compare pc2 pc1)
+      (List.rev_map
+        (fun (pc, i) -> (P.to_int pc, i))
+        (PTree.elements f.mod_controllogic)) in
+  fprintf pp "  datapath {\n";
+  List.iter (print_instruction pp) datapath;
+  fprintf pp "  }\n\n  controllogic {\n";
+  List.iter (print_instruction pp) controllogic;
+  fprintf pp "  }\n}\n\n"
+
+let print_globdef pp (id, gd) =
+  match gd with
+  | Gfun(Internal f) -> print_module pp id f
+  | _ -> ()
+
+let print_program pp prog =
+  List.iter (print_globdef pp) prog.prog_defs
+
+let destination : string option ref = ref None
+
+let print_if prog =
+  match !destination with
+  | None -> ()
+  | Some f ->
+    let oc = open_out f in
+    print_program oc prog;
+    close_out oc
diff --git a/src/verilog/PrintVerilog.ml b/src/verilog/PrintVerilog.ml
index 6d10887..5265c97 100644
--- a/src/verilog/PrintVerilog.ml
+++ b/src/verilog/PrintVerilog.ml
@@ -78,7 +78,7 @@ let rec pprint_expr = function
   | Vvari (s, i) -> concat [register s; "["; pprint_expr i; "]"]
   | Vinputvar s -> register s
   | Vunop (u, e) -> concat ["("; unop u; pprint_expr e; ")"]
-  | Vbinop (op, a, b) -> concat ["("; pprint_binop (pprint_expr a) (pprint_expr b) op; ")"]
+  | Vbinop (op, a, b) -> concat [pprint_binop (pprint_expr a) (pprint_expr b) op]
   | Vternary (c, t, f) -> concat ["("; pprint_expr c; " ? "; pprint_expr t; " : "; pprint_expr f; ")"]
 
 let rec pprint_stmnt i =
diff --git a/src/verilog/PrintVerilog.mli b/src/verilog/PrintVerilog.mli
index 6544e52..62bf63f 100644
--- a/src/verilog/PrintVerilog.mli
+++ b/src/verilog/PrintVerilog.mli
@@ -16,6 +16,8 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
+val pprint_stmnt : int -> Verilog.stmnt -> string
+
 val print_value : out_channel -> Value.value -> unit
 
 val print_program : bool -> out_channel -> Verilog.program -> unit