diff options
Diffstat (limited to 'src/hls/PrintHTL.ml')
-rw-r--r-- | src/hls/PrintHTL.ml | 69 |
1 files changed, 44 insertions, 25 deletions
diff --git a/src/hls/PrintHTL.ml b/src/hls/PrintHTL.ml index a75d0ee..8608784 100644 --- a/src/hls/PrintHTL.ml +++ b/src/hls/PrintHTL.ml @@ -30,34 +30,53 @@ open VericertClflags let pstr pp = fprintf pp "%s" -let reg pp r = - fprintf pp "x%d" (P.to_int r) +let concat = String.concat "" -let rec regs pp = function - | [] -> () - | [r] -> reg pp r - | r1::rl -> fprintf pp "%a, %a" reg r1 regs rl +let rec intersperse c = function + | [] -> [] + | [x] -> [x] + | x :: xs -> x :: c :: intersperse c xs + +let register a = sprintf "reg_%d" (P.to_int a) +let registers a = String.concat "" (intersperse ", " (List.map register a)) let print_instruction pp (pc, i) = fprintf pp "%5d:\t%s" pc (pprint_stmnt 0 i) +let string_controlsignal = function + | Coq_ctrl_finish -> "finish" + | Coq_ctrl_return -> "return" + | Coq_ctrl_start -> "start" + | Coq_ctrl_reset -> "rst" + | Coq_ctrl_clk -> "clk" + | Coq_ctrl_param idx -> sprintf "param_%d" (Nat.to_int idx) + +let print_externctrl pp ((local_reg : reg), ((target_mod: ident), (target_reg: controlsignal))) = + fprintf pp "%s -> %s.%s\n" (register local_reg) (extern_atom target_mod) (string_controlsignal target_reg) + +let ptree_to_list ptree = + List.sort + (fun (pc1, _) (pc2, _) -> compare pc2 pc1) + (List.rev_map + (fun (pc, i) -> (P.to_int pc, i)) + (PTree.elements ptree)) + 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"; + fprintf pp "%s(%s) {\n" (extern_atom id) (registers f.mod_params); + + let externctrl = PTree.elements f.mod_externctrl in + let datapath = ptree_to_list f.mod_datapath in + let controllogic = ptree_to_list f.mod_controllogic in + + fprintf pp "externctrl {\n"; + List.iter (print_externctrl pp) externctrl; + fprintf pp " }\n\n"; + + fprintf pp "datapath {\n"; List.iter (print_instruction pp) datapath; - fprintf pp " }\n\n controllogic {\n"; + fprintf pp " }\n\n"; + + fprintf pp "controllogic {\n"; List.iter (print_instruction pp) controllogic; fprintf pp " }\n}\n\n" @@ -71,10 +90,10 @@ let print_program pp prog = let destination : string option ref = ref None -let print_if prog = +let print_if passno prog = match !destination with | None -> () | Some f -> - let oc = open_out f in - print_program oc prog; - close_out oc + let oc = open_out (f ^ "." ^ Z.to_string passno) in + print_program oc prog; + close_out oc |