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"
 
@@ -53,6 +54,18 @@ static constant_exprt onehot0(const constant_exprt &expr, const namespacet &ns)
     return false_exprt();
 }
 
+/// constant folding for $isunknown
+static constant_exprt
+isunknown(const constant_exprt &expr, const namespacet &ns)
+{
+  auto bval = ::bval(expr);
+  CHECK_RETURN(bval.is_constant());
+  if(numeric_cast_v<mp_integer>(to_constant_expr(bval)) == 0)
+    return false_exprt{};
+  else
+    return true_exprt{};
+}
+
 static exprt verilog_simplifier_rec(exprt expr, const namespacet &ns)
 {
   // Remember the Verilog type.
@@ -161,6 +174,21 @@ static exprt verilog_simplifier_rec(exprt expr, const namespacet &ns)
     if(op.is_constant())
       expr = onehot0(to_constant_expr(op), ns);
   }
+  else if(expr.id() == ID_function_call)
+  {
+    auto &call = to_function_call_expr(expr);
+    if(call.function().id() == ID_symbol)
+    {
+      auto identifier = to_symbol_expr(call.function()).get_identifier();
+      if(identifier == "$isunknown")
+      {
+        DATA_INVARIANT(
+          call.arguments().size() == 1, "$isunknown gets one argument");
+        if(call.arguments()[0].is_constant())
+          expr = isunknown(to_constant_expr(call.arguments()[0]), ns);
+      }
+    }
+  }
 
   // We fall back to the simplifier to approximate
   // the standard's definition of 'constant expression'.

src/verilog/verilog_typecheck_expr.cpp

@@ -979,6 +979,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)

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 &);