aboutsummaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2020-10-23 13:25:10 +0100
committerYann Herklotz <git@yannherklotz.com>2020-11-09 19:37:20 +0000
commit82ee873033f51e856e69cea95db95e292bd0aea9 (patch)
tree6c3e27c5a94589b20e72ccb79e96bdb8ed676c51 /src
parent9d6979baa0e4b505862bcedee1dfd075f36579c3 (diff)
downloadvericert-kvx-82ee873033f51e856e69cea95db95e292bd0aea9.tar.gz
vericert-kvx-82ee873033f51e856e69cea95db95e292bd0aea9.zip
Fix printing of negative numbers
Diffstat (limited to 'src')
-rw-r--r--src/verilog/PrintVerilog.ml6
1 files changed, 5 insertions, 1 deletions
diff --git a/src/verilog/PrintVerilog.ml b/src/verilog/PrintVerilog.ml
index 0f64066..353bfac 100644
--- a/src/verilog/PrintVerilog.ml
+++ b/src/verilog/PrintVerilog.ml
@@ -72,7 +72,11 @@ 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%ld" (camlint_of_coqint l)
+let literal l =
+ let l' = camlint_of_coqint l in
+ if l' < Int32.zero
+ then sprintf "(- 32'd%ld)" (Int32.neg l')
+ else sprintf "32'd%ld" l'
let rec pprint_expr = function
| Vlit l -> literal l