aboutsummaryrefslogtreecommitdiffstats
path: root/src/verilog/PrintVerilog.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/verilog/PrintVerilog.ml')
-rw-r--r--src/verilog/PrintVerilog.ml10
1 files changed, 8 insertions, 2 deletions
diff --git a/src/verilog/PrintVerilog.ml b/src/verilog/PrintVerilog.ml
index 5265c97..db78ad5 100644
--- a/src/verilog/PrintVerilog.ml
+++ b/src/verilog/PrintVerilog.ml
@@ -17,7 +17,7 @@
*)
open Verilog
-open Value
+open ValueInt
open Datatypes
open Camlcoq
@@ -70,11 +70,17 @@ let unop = function
let register a = sprintf "reg_%d" (P.to_int a)
-let literal l = sprintf "%d'd%d" (Nat.to_int l.vsize) (Z.to_int (uvalueToZ l))
+let literal l = sprintf "32'd%d" (Z.to_int (uvalueToZ l))
+
+let byte n s = sprintf "reg_%d[%d:%d]" (P.to_int s) (7 + n * 8) (n * 8)
let rec pprint_expr = function
| Vlit l -> literal l
| Vvar s -> register s
+ | Vvarb0 s -> byte 0 s
+ | Vvarb1 s -> byte 1 s
+ | Vvarb2 s -> byte 2 s
+ | Vvarb3 s -> byte 3 s
| Vvari (s, i) -> concat [register s; "["; pprint_expr i; "]"]
| Vinputvar s -> register s
| Vunop (u, e) -> concat ["("; unop u; pprint_expr e; ")"]