aboutsummaryrefslogtreecommitdiffstats
path: root/src/verilog/PrintVerilog.ml
diff options
context:
space:
mode:
authorMichalis Pardalos <m.pardalos@gmail.com>2020-11-27 12:51:20 +0000
committerMichalis Pardalos <m.pardalos@gmail.com>2020-11-27 12:56:26 +0000
commit130d11a3291e3bce761ecbaeb7185df4ea98009d (patch)
tree0043544128f4409871433130df07ccb80458b74d /src/verilog/PrintVerilog.ml
parent303a45374643f75698c61f062899973d2c297831 (diff)
downloadvericert-130d11a3291e3bce761ecbaeb7185df4ea98009d.tar.gz
vericert-130d11a3291e3bce761ecbaeb7185df4ea98009d.zip
Revert changes relating to instance generation
Revert "Add todo for missing logic around instantiations" This reverts commit 303a45374643f75698c61f062899973d2c297831. Revert "Add wires and use them for output of instances" This reverts commit a72f26319dabca414a2b576424b9f72afaca161c. Revert "Separate HTL instantiations from Verilog ones" This reverts commit 653c8729f4322f538aa7116c5e311c884b3c5047. Revert "Translate instantiations from HTL to verilog" This reverts commit 982e6c69a52e8ec4e677147004cc5472f8a80d6d. Revert "Print instantiations in HTL output" This reverts commit 9b87637d3e4d6a75dee1221b017e3ccf6632642e. Revert "Add a field in HTL modules for instances" This reverts commit d79dae026b150e9671e0aa7262f6aa2d1d302502. Revert "Generate (invalid) module instantiations for calls" This reverts commit dfaa3a9cbc07649feea3220693a8a854a32eafb6.
Diffstat (limited to 'src/verilog/PrintVerilog.ml')
-rw-r--r--src/verilog/PrintVerilog.ml18
1 files changed, 5 insertions, 13 deletions
diff --git a/src/verilog/PrintVerilog.ml b/src/verilog/PrintVerilog.ml
index a355a17..b3fb6c8 100644
--- a/src/verilog/PrintVerilog.ml
+++ b/src/verilog/PrintVerilog.ml
@@ -36,11 +36,6 @@ let fold_map f s = List.map f s |> concat
let pstr pp = fprintf pp "%s"
-let rec intersperse c = function
- | [] -> []
- | [x] -> [x]
- | x :: xs -> x :: c :: intersperse c xs
-
let pprint_binop l r =
let unsigned op = sprintf "{%s %s %s}" l op r in
let signed op = sprintf "{$signed(%s) %s $signed(%s)}" l op r in
@@ -74,8 +69,6 @@ let unop = function
| Vnot -> " ! "
let register a = sprintf "reg_%d" (P.to_int a)
-let vmodule a = sprintf "%s" (extern_atom a)
-let instance a = sprintf "instance_%d" (P.to_int a)
(*let literal l = sprintf "%d'd%d" (Nat.to_int l.vsize) (Z.to_int (uvalueToZ l))*)
@@ -141,12 +134,6 @@ let print_io = function
let decl i = function
| Vdecl (io, r, sz) -> concat [indent i; declare (print_io io) (r, sz)]
| Vdeclarr (io, r, sz, ln) -> concat [indent i; declarearr (print_io io) (r, sz, ln)]
- | Vdeclwire (r, sz) -> concat [indent i; declare "wire" (r, sz)]
- | Vinstancedecl (m, name, args) -> concat [
- indent i; vmodule m; " ";
- instance name; "("; concat (intersperse ", " (List.map register args)); ")";
- ";\n"
- ]
(* TODO Fix always blocks, as they currently always print the same. *)
let pprint_module_item i = function
@@ -158,6 +145,11 @@ let pprint_module_item i = function
| Valways_comb (e, s) ->
concat [indent i; "always "; pprint_edge_top i e; "\n"; pprint_stmnt (i+1) s]
+let rec intersperse c = function
+ | [] -> []
+ | [x] -> [x]
+ | x :: xs -> x :: c :: intersperse c xs
+
let make_io i io r = concat [indent i; io; " "; register r; ";\n"]
let compose f g x = g x |> f