Verilog: constant output now includes signedness and width

The conversion of constants to Verilog source now includes the signedness
and width when outputting hex or binary literals.

Author: kroening

regression/verilog/expressions/constants1.desc

@@ -1,6 +1,8 @@
 CORE
 constants1.v
 --bound 1
+^\[.*\] always main\.w == 32'hFFFF: PROVED up to bound 1$
+^\[.*\] always main\.X == 16: PROVED up to bound 1$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/expressions/equality1.desc

@@ -10,7 +10,7 @@ equality1.v
 ^\[.*\] always 1'bx != 10 === 1'bx: PROVED up to bound 0$
 ^\[.*\] always 1'bz != 20 === 1'bx: PROVED up to bound 0$
 ^\[.*\] always 2'b11 == 2'b11 === 0: REFUTED$
-^\[.*\] always 2'sb-1 == 2'sb-1 === 1: PROVED up to bound 0$
+^\[.*\] always 2'sb11 == 2'sb11 === 1: PROVED up to bound 0$
 ^EXIT=10$
 ^SIGNAL=0$
 --

regression/verilog/expressions/equality2.desc

@@ -11,8 +11,8 @@ equality2.v
 ^\[.*\] always 1'bx === 1 == 0: PROVED up to bound 0$
 ^\[.*\] always 1'bz === 1 == 0: PROVED up to bound 0$
 ^\[.*\] always 1 === 1 == 1: PROVED up to bound 0$
-^\[.*\] always 3'b11 === 3'b111 == 1: REFUTED$
-^\[.*\] always 3'sb-1 === 3'sb-1 == 1: PROVED up to bound 0$
+^\[.*\] always 3'b011 === 3'b111 == 1: REFUTED$
+^\[.*\] always 3'sb111 === 3'sb111 == 1: PROVED up to bound 0$
 ^EXIT=10$
 ^SIGNAL=0$
 --

src/verilog/expr2verilog.cpp

@@ -1020,14 +1020,20 @@ std::string expr2verilogt::convert_constant(
     auto i = numeric_cast_v<mp_integer>(src);
 
     if(i>=256)
-      dest="'h"+integer2string(i, 16);
+    {
+      dest = std::to_string(width);
+      dest += "'h";
+      if(type.id() == ID_signedbv)
+        dest += 's';
+      dest += integer2string(i, 16);
+    }
     else if(width<=7)
     {
       dest=std::to_string(width);
       dest+="'";
       if(type.id()==ID_signedbv) dest+='s';
       dest+='b';
-      dest+=integer2string(i, 2);
+      dest += integer2binary(i, width);
     }
     else
       dest=integer2string(i);