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

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"
 
@@ -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,21 @@ 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)