1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
|
(* -*- mode: tuareg -*-
* Vericert: 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 Datatypes
open Camlcoq
open AST
open Clflags
open Printf
open Maps
open AST
open HTL
open PrintAST
open PrintVerilog
open VericertClflags
let pstr pp = fprintf pp "%s"
let concat = String.concat ""
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_ram pp opt_ram =
match opt_ram with
| Some ram ->
fprintf pp "ram {\n";
fprintf pp " size: %d\n" (Nat.to_int ram.ram_size);
fprintf pp " mem: %s\n" (register ram.ram_mem);
fprintf pp " en: %s\n" (register ram.ram_en);
fprintf pp " u_en: %s\n" (register ram.ram_u_en);
fprintf pp " addr: %s\n" (register ram.ram_addr);
fprintf pp " wr_en: %s\n" (register ram.ram_wr_en);
fprintf pp " d_in: %s\n" (register ram.ram_d_in);
fprintf pp " d_out: %s\n" (register ram.ram_d_out);
fprintf pp "}\n\n"
| None -> ()
let print_control pp f =
fprintf pp "control {\n";
fprintf pp " st: %s\n" (register f.mod_st);
fprintf pp " stk: %s\n" (register f.mod_stk);
fprintf pp " finish: %s\n" (register f.mod_finish);
fprintf pp " return: %s\n" (register f.mod_return);
fprintf pp " start: %s\n" (register f.mod_start);
fprintf pp " reset: %s\n" (register f.mod_reset);
fprintf pp " clk: %s\n" (register f.mod_clk);
fprintf pp "}\n\n"
let print_scldecl pp (r, (io, sz)) =
fprintf pp " %s [%d:0]%s\n" (fst (print_io io)) (Nat.to_int sz - 1) (register (P.of_int r))
let print_arrdecl pp (r, (io, Verilog.VArray(sz, ln))) =
fprintf pp " %s [%d:0]%s[%d:0]\n" (fst (print_io io)) (Nat.to_int sz - 1) (register (P.of_int r)) (Nat.to_int ln - 1)
let print_module pp id f =
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
let scldecls = ptree_to_list f.mod_scldecls in
let arrdecls = ptree_to_list f.mod_arrdecls in
print_control pp f;
fprintf pp "scldecls {\n";
List.iter (print_scldecl pp) scldecls;
fprintf pp " }\n\n";
fprintf pp "arrdecls {\n";
List.iter (print_arrdecl pp) arrdecls;
fprintf pp " }\n\n";
print_ram pp f.mod_ram;
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";
fprintf pp "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 passno prog =
match !destination with
| None -> ()
| Some f ->
let oc = open_out (f ^ "." ^ Z.to_string passno) in
print_program oc prog;
close_out oc
|
