Merge pull request #1022 from diffblue/unbased-unsized-literals

SystemVerilog: unbased unsized literals

Author: kroening

CHANGELOG

@@ -2,6 +2,7 @@
 
 * SystemVerilog: typedefs from package scopes
 * SystemVerilog: assignment patterns with keys for structs
+* SystemVerilog: unbased unsigned literals '0, '1, 'x, 'z
 * 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.desc

@@ -0,0 +1,7 @@
+CORE
+integer_literals1.sv
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/verilog/expressions/integer_literals1.sv

@@ -0,0 +1,23 @@
+module main;
+
+  p01: assert final ($bits(8'b1)==8);
+
+  // 1800-2017 5.7.1L without a given width, the number of bits "shall be at least 32"
+  p02: assert final ($bits(1)==32);
+  p03: assert final ($bits('d1)==32);
+  p04: assert final ($bits('b1)==32);
+
+  // simple decimal numbers without size and base are signed
+  p05: assert final ($typename(1)=="bit signed[31:0]");
+
+  // numbers with size or base are unsigned
+  p06: assert final ($typename('d1)=="bit[31:0]");
+  p07: assert final ($typename(10'd1)=="bit[9:0]");
+
+  // unbased unsized literals
+  p08: assert final ($typename('0)=="bit[0:0]" && '0===1'b0);
+  p09: assert final ($typename('1)=="bit[0:0]" && '1===1'b1);
+  p10: assert final ($typename('x)=="logic[0:0]" && 'x===1'bx);
+  p11: assert final ($typename('z)=="logic[0:0]" && 'z===1'bz);
+
+endmodule

src/verilog/convert_literals.cpp

@@ -132,6 +132,24 @@ constant_exprt convert_integral_literal(const irep_idt &value)
       rest += tolower(ch);
   }
 
+  // special case the "unbased unsized literals"
+  if(rest == "'0")
+  {
+    return from_integer(0, unsignedbv_typet{1});
+  }
+  else if(rest == "'1")
+  {
+    return from_integer(1, unsignedbv_typet{1});
+  }
+  else if(rest == "'x" || rest == "'X")
+  {
+    return constant_exprt{"x", verilog_unsignedbv_typet{1}};
+  }
+  else if(rest == "'z" || rest == "'Z")
+  {
+    return constant_exprt{"z", verilog_unsignedbv_typet{1}};
+  }
+
   std::string::size_type pos = rest.find('\'');
   std::size_t bits = 0;
   bool bits_given = false;

src/verilog/scanner.l

@@ -128,6 +128,7 @@ 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}
 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")
 Real            {Number}\.{Number}
 RealExp         {Number}(\.{Number})?[eE][+-]?{Number}
@@ -572,6 +573,7 @@ prove           { VL2SMV_VERILOG_KEYWORD(TOK_PROVE); }
 {Decimal}       { newstack(yyveriloglval); stack_expr(yyveriloglval).id(yytext); return TOK_NUMBER; }
 {Hexdecimal}    { newstack(yyveriloglval); stack_expr(yyveriloglval).id(yytext); return TOK_NUMBER; }
 {Number}        { newstack(yyveriloglval); stack_expr(yyveriloglval).id(yytext); return TOK_NUMBER; }
+{unbased_unsized} { newstack(yyveriloglval); stack_expr(yyveriloglval).id(yytext); return TOK_NUMBER; }
 {Time}		{ newstack(yyveriloglval); stack_expr(yyveriloglval).id(yytext); return TOK_TIME_LITERAL; }
 {Real}          { newstack(yyveriloglval); stack_expr(yyveriloglval).id(yytext); return TOK_NUMBER; }
 {RealExp}       { newstack(yyveriloglval); stack_expr(yyveriloglval).id(yytext); return TOK_NUMBER; }

src/verilog/verilog_typecheck_expr.cpp

@@ -731,7 +731,7 @@ exprt verilog_typecheck_exprt::typename_string(const exprt &expr)
 
   std::string s;
 
-  if(type.id() == ID_unsignedbv || type.id() == ID_verilog_unsignedbv)
+  if(type.id() == ID_unsignedbv)
   {
     if(verilog_type == ID_verilog_byte)
       s = "byte unsigned";
@@ -744,6 +744,10 @@ exprt verilog_typecheck_exprt::typename_string(const exprt &expr)
     else
       s = "bit[" + to_string(left) + ":" + to_string(right) + "]";
   }
+  else if(type.id() == ID_verilog_unsignedbv)
+  {
+    s = "logic[" + to_string(left) + ":" + to_string(right) + "]";
+  }
   else if(type.id() == ID_bool)
   {
     s = "bit";
@@ -761,6 +765,10 @@ exprt verilog_typecheck_exprt::typename_string(const exprt &expr)
     else
       s = "bit signed[" + to_string(left) + ":" + to_string(right) + "]";
   }
+  else if(type.id() == ID_verilog_signedbv)
+  {
+    s = "logic signed[" + to_string(left) + ":" + to_string(right) + "]";
+  }
   else if(type.id() == ID_verilog_realtime)
   {
     s = "realtime";