diff options
author | Yann Herklotz <git@yannherklotz.com> | 2021-02-16 14:11:32 +0000 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2021-02-16 14:11:32 +0000 |
commit | 6a395495bd35bb7d4d2cc7d3271c9b588d466594 (patch) | |
tree | 0fcc285046352b9f677454eac3224ce5a90ba48e /src/hls/PrintHTL.ml | |
parent | 5f1e7aa8fbc4a0e04d0b137410c13f3d8da4d987 (diff) | |
parent | b5c79cb4913087a0e4b577b5dff616fc88ee938b (diff) | |
download | vericert-6a395495bd35bb7d4d2cc7d3271c9b588d466594.tar.gz vericert-6a395495bd35bb7d4d2cc7d3271c9b588d466594.zip |
Merge branch 'michalis' of https://github.com/mpardalos/vericert into michalis-merge
Diffstat (limited to 'src/hls/PrintHTL.ml')
-rw-r--r-- | src/hls/PrintHTL.ml | 66 |
1 files changed, 44 insertions, 22 deletions
diff --git a/src/hls/PrintHTL.ml b/src/hls/PrintHTL.ml index a75d0ee..836222e 100644 --- a/src/hls/PrintHTL.ml +++ b/src/hls/PrintHTL.ml @@ -30,35 +30,57 @@ 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 pprint_datapath_stmnt i = function + | HTLDataVstmnt s -> pprint_stmnt i s + | HTLfork (name, args) -> concat [ + "fork "; extern_atom name; "("; concat (intersperse ", " (List.map register args)); ");\n" + ] + | HTLjoin (name, dst) -> concat [ + register dst; " <= join "; extern_atom name; ";\n" + ] + +let print_datapath_instruction pp (pc, i) = + fprintf pp "%5d:\t%s" pc (pprint_datapath_stmnt 0 i) + +let pprint_control_stmnt i = function + | HTLCtrlVstmnt s -> pprint_stmnt i s + | HTLwait (name, statereg, expr) -> concat [ + "wait("; extern_atom name; ", "; + register statereg; ", "; + pprint_expr expr; ");\n" + ] + +let print_control_instruction pp (pc, i) = + fprintf pp "%5d:\t%s" pc (pprint_control_stmnt 0 i) + +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"; - List.iter (print_instruction pp) datapath; + fprintf pp "%s(%s) {\n" (extern_atom id) (registers f.mod_params); + let datapath = ptree_to_list f.mod_datapath in + let controllogic = ptree_to_list f.mod_controllogic in + fprintf pp "datapath {\n"; + List.iter (print_datapath_instruction pp) datapath; fprintf pp " }\n\n controllogic {\n"; - List.iter (print_instruction pp) controllogic; + List.iter (print_control_instruction pp) controllogic; fprintf pp " }\n}\n\n" let print_globdef pp (id, gd) = |