Verilog: $isunknown

This adds a lowering and constant-folding for $isunknown.

Author: kroening

CHANGELOG

@@ -3,6 +3,7 @@
 * Verilog: `elsif preprocessor directive
 * Verilog: fix for named generate blocks
 * Verilog: $onehot and $onehot0 are now elaboration-time constant
+* Verilog: $isunknown
 * SystemVerilog: fix for #-# and #=# for empty matches
 * SystemVerilog: fix for |-> and |=> for empty matches
 * LTL/SVA to Buechi with --buechi

regression/verilog/system-functions/isunknown1.desc

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

regression/verilog/system-functions/isunknown1.sv

@@ -0,0 +1,13 @@
+module main;
+
+  p0: assert final ($isunknown(123)==0);
+  p1: assert final ($isunknown('z)==1);
+  p2: assert final ($isunknown('x)==1);
+  p3: assert final ($isunknown('b01x0)==1);
+  p4: assert final ($isunknown(3'bzzz)==1);
+
+  // $isunknown yields an elaboration-time constant
+  parameter Q1 = $isunknown(3'b10z);
+  parameter P1 = $isunknown(3'b101);
+
+endmodule

src/verilog/verilog_simplifier.cpp

@@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <ebmc/ebmc_error.h>
 
+#include "aval_bval_encoding.h"
 #include "verilog_expr.h"
 #include "verilog_types.h"
 

src/verilog/verilog_typecheck_expr.cpp

@@ -20,6 +20,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/std_expr.h>
 #include <util/string2int.h>
 
+#include "aval_bval_encoding.h"
 #include "convert_literals.h"
 #include "expr2verilog.h"
 #include "verilog_bits.h"
@@ -488,6 +489,31 @@ exprt verilog_typecheck_exprt::convert_expr_function_call(
 
 /*******************************************************************\
 
+Function: verilog_typecheck_exprt::isunknown
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+constant_exprt verilog_typecheck_exprt::isunknown(const constant_exprt &expr)
+{
+  // constant folding for $isunknown
+  auto bval = ::bval(expr);
+  auto bval_simplified = simplify_expr(bval, ns);
+  CHECK_RETURN(bval_simplified.is_constant());
+  auto all_zeros = to_bv_type(bval_simplified.type()).all_zeros_expr();
+  if(bval_simplified == all_zeros)
+    return false_exprt{};
+  else
+    return true_exprt{};
+}
+
+/*******************************************************************\
+
 Function: verilog_typecheck_exprt::bits
 
   Inputs:
@@ -979,6 +1005,18 @@ exprt verilog_typecheck_exprt::convert_system_function(
 
     return std::move(expr);
   }
+  else if(identifier == "$isunknown")
+  {
+    if(arguments.size() != 1)
+    {
+      throw errort().with_location(expr.source_location())
+        << "$isunknown takes one argument";
+    }
+
+    expr.type() = bool_typet();
+
+    return std::move(expr);
+  }
   else if(identifier == "$past")
   {
     if(arguments.size() == 0 || arguments.size() >= 4)
@@ -1784,6 +1822,17 @@ exprt verilog_typecheck_exprt::elaborate_constant_system_function_call(
     DATA_INVARIANT(arguments.size() == 1, "$typename takes one argument");
     return typename_string(arguments[0]);
   }
+  else if(identifier == "$isunknown")
+  {
+    DATA_INVARIANT(arguments.size() == 1, "$isunknown takes one argument");
+
+    auto op = elaborate_constant_expression(arguments[0]);
+
+    if(!op.is_constant())
+      return std::move(expr); // give up
+    else
+      return isunknown(to_constant_expr(op));
+  }
   else
     return std::move(expr); // don't know it, won't elaborate
 }

src/verilog/verilog_typecheck_expr.h

@@ -215,6 +215,7 @@ class verilog_typecheck_exprt:public verilog_typecheck_baset
   exprt bits(const exprt &);
   std::optional<mp_integer> bits_rec(const typet &) const;
   constant_exprt countones(const constant_exprt &);
+  constant_exprt isunknown(const constant_exprt &);
   constant_exprt left(const exprt &);
   constant_exprt right(const exprt &);
   constant_exprt low(const exprt &);