Merge pull request #1023 from diffblue/verilog-dx-dz

Verilog: 'dx, 'dz

Author: tautschnig

CHANGELOG

@@ -3,6 +3,7 @@
 * SystemVerilog: typedefs from package scopes
 * SystemVerilog: assignment patterns with keys for structs
 * SystemVerilog: unbased unsigned literals '0, '1, 'x, 'z
+* Verilog: 'dx, 'dz
 * SMV: LTL V operator, xnor operator
 * SMV: word types and operators
 * --smv-word-level outputs the model as word-level SMV

regression/verilog/expressions/integer_literals1.sv

@@ -20,4 +20,16 @@ module main;
   p10: assert final ($typename('x)=="logic[0:0]" && 'x===1'bx);
   p11: assert final ($typename('z)=="logic[0:0]" && 'z===1'bz);
 
+  // decimals must not contain x/z "unless there is
+  // exactly one digit in the token"
+  p12: assert final ('dx===32'hxxxx_xxxx);
+  p13: assert final ('dX===32'hxxxx_xxxx);
+  p14: assert final ('dz===32'hzzzz_zzzz);
+  p15: assert final ('dZ===32'hzzzz_zzzz);
+  p16: assert final (4'dx===4'hx);
+  p17: assert final (4'dX===4'hx);
+  p18: assert final (4'dz===4'hz);
+  p19: assert final (4'dZ===4'hz);
+  p20: assert final ($typename(4'sdx)==="logic signed[3:0]");
+
 endmodule

src/verilog/convert_literals.cpp

@@ -174,6 +174,26 @@ constant_exprt convert_integral_literal(const irep_idt &value)
     rest = rest.substr(1);
   }
 
+  // special case for 'dx/'dX/'dz/'dZ
+  // "The default length of x and z is the same as the default length of an integer."
+  // Introduced by Verilog 1364-2001.
+  if(rest == "dx" || rest == "dX")
+  {
+    std::size_t final_bits = bits_given ? bits : 32;
+    auto type = s_flag_given
+                  ? static_cast<typet>(verilog_signedbv_typet{final_bits})
+                  : verilog_unsignedbv_typet{final_bits};
+    return constant_exprt{std::string(final_bits, 'x'), type};
+  }
+  else if(rest == "dz" || rest == "dZ")
+  {
+    std::size_t final_bits = bits_given ? bits : 32;
+    auto type = s_flag_given
+                  ? static_cast<typet>(verilog_signedbv_typet{final_bits})
+                  : verilog_unsignedbv_typet{final_bits};
+    return constant_exprt{std::string(final_bits, 'z'), type};
+  }
+
   unsigned base = 10;
 
   // base given?

src/verilog/scanner.l

@@ -126,7 +126,7 @@ Word            {LetterU}{WordNumUD}*
 EscapedWord     "\\"[^\n \t\r]+
 Binary          ({Number})?{WSst}'{WSst}[sS]?[bB]{WSst}[01xXzZ?]([01xXzZ?_])*
 Octal           ({Number})?{WSst}'{WSst}[sS]?[oO]{WSst}[0-7xXzZ?]([0-7xXzZ?_])*
-Decimal         ({Number})?{WSst}'{WSst}[sS]?[dD]{WSst}{Number}
+Decimal         ({Number})?{WSst}'{WSst}[sS]?[dD]{WSst}({Number}|[xXzZ]_*)
 Hexdecimal      ({Number})?{WSst}'{WSst}[sS]?[hH]{WSst}[0-9a-fA-FxXzZ?]([0-9a-fA-FxXzZ?_])*
 unbased_unsized '0|'1|'x|'X|'z|'Z
 Time            {Number}(\.{Number})?("fs"|"ps"|"ns"|"us"|"ms"|"s")

src/verilog/verilog_typecheck_expr.cpp

@@ -752,7 +752,7 @@ exprt verilog_typecheck_exprt::typename_string(const exprt &expr)
   {
     s = "bit";
   }
-  else if(type.id() == ID_signedbv || type.id() == ID_verilog_signedbv)
+  else if(type.id() == ID_signedbv)
   {
     if(verilog_type == ID_verilog_byte)
       s = "byte";