Verilog: $isunknown

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

Author: kroening

CHANGELOG

@@ -1,6 +1,7 @@
 # EBMC 5.7
 
 * Verilog: `elsif preprocessor directive
+* Verilog: $isunknown
 * LTL/SVA to Buechi with --buechi
 
 # EBMC 5.6

src/verilog/verilog_simplifier.cpp

@@ -17,6 +17,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "verilog_expr.h"
 #include "verilog_types.h"
+#include "aval_bval_encoding.h"
 
 static constant_exprt
 countones(const constant_exprt &expr, const namespacet &ns)
@@ -33,6 +34,18 @@ countones(const constant_exprt &expr, const namespacet &ns)
     return to_constant_expr(simplified);
 }
 
+/// 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.
@@ -129,6 +142,20 @@ static exprt verilog_simplifier_rec(exprt expr, const namespacet &ns)
       ops.push_back(replication.op());
     expr = concatenation_exprt{ops, expr.type()};
   }
+  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)