Verilog: expand $ND during synthesis, not typechecking

This prevents premature optimisation by expanding $ND during synthesis.

Author: kroening

src/verilog/verilog_synthesis.cpp

@@ -152,16 +152,32 @@ exprt verilog_synthesist::expand_function_call(const function_call_exprt &call)
   // Is it a 'system function call'?
   if(call.is_system_function_call())
   {
-    // Attempt to constant fold.
-    verilog_typecheck_exprt verilog_typecheck_expr(ns, get_message_handler());
-    auto result = verilog_typecheck_expr.elaborate_constant_system_function_call(call);
-    if(!result.is_constant())
+    auto identifier = to_symbol_expr(call.function()).get_identifier();
+    if(identifier == "$ND")
     {
-      throw errort().with_location(call.source_location())
-        << "cannot synthesise system function " << to_string(call.function());
+      std::string identifier =
+        id2string(module) + "::nondet::" + std::to_string(nondet_count++);
+
+      auto arguments = call.arguments();
+      exprt select_one(
+        ID_constraint_select_one, call.type(), std::move(arguments));
+      select_one.set(ID_identifier, identifier);
+      return select_one.with_source_location<exprt>(call);
     }
+    else
+    {
+      // Attempt to constant fold.
+      verilog_typecheck_exprt verilog_typecheck_expr(ns, get_message_handler());
+      auto result =
+        verilog_typecheck_expr.elaborate_constant_system_function_call(call);
+      if(!result.is_constant())
+      {
+        throw errort().with_location(call.source_location())
+          << "cannot synthesise system function " << to_string(call.function());
+      }
 
-    return result;
+      return result;
+    }
   }
 
   // check some restrictions

src/verilog/verilog_synthesis_class.h

@@ -70,7 +70,10 @@ class verilog_synthesist:
 
 protected:
   const optionst &options;
- 
+
+  // For $ND(...)
+  std::size_t nondet_count = 0;
+
   enum class event_guardt { NONE, CLOCK, COMBINATIONAL };
 
   inline std::string as_string(event_guardt g)

src/verilog/verilog_typecheck_expr.cpp

@@ -200,15 +200,6 @@ void verilog_typecheck_exprt::propagate_type(
         }
       }
     }
-    else if(expr.id()==ID_constraint_select_one)
-    {
-      expr.type()=type;
-
-      Forall_operands(it, expr)
-        propagate_type(*it, type);
-
-      return;
-    }
   }
 
   implicit_typecast(expr, type);
@@ -327,10 +318,6 @@ exprt verilog_typecheck_exprt::convert_expr_rec(exprt expr)
   {
     return convert_expr_function_call(to_function_call_expr(expr));
   }
-  else if(expr.id()==ID_constraint_select_one)
-  {
-    return convert_constraint_select_one(std::move(expr));
-  }
   else
   {
     std::size_t no_op;
@@ -435,29 +422,6 @@ exprt verilog_typecheck_exprt::convert_expr_function_call(
 
 /*******************************************************************\
 
-Function: verilog_typecheck_exprt::convert_constraint_select_one
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-exprt verilog_typecheck_exprt::convert_constraint_select_one(exprt expr)
-{
-  if(expr.operands().size()<2)
-  {
-    throw errort().with_location(expr.source_location())
-      << "constraint_select_one takes at least two operands";
-  }
-
-  return expr;
-}
-
-/*******************************************************************\
-
 Function: verilog_typecheck_exprt::bits
 
   Inputs:
@@ -632,20 +596,9 @@ exprt verilog_typecheck_exprt::convert_system_function(
       throw errort().with_location(expr.source_location())
         << "$ND takes at least one argument";
     }
-    
-    if(arguments.size()==1)
-      return arguments.front(); // remove
 
-    std::string identifier=
-      id2string(module_identifier)+"::nondet::"+std::to_string(nondet_count++);
-
-    typet type=arguments.front().type();
-
-    exprt select_one(ID_constraint_select_one, type);
-    select_one.operands()=arguments;
-    select_one.set(ID_identifier, identifier);
-
-    return select_one;
+    expr.type() = arguments.front().type();
+    return std::move(expr);
   }
   else if(identifier == "$bits")
   {

src/verilog/verilog_typecheck_expr.h

@@ -26,18 +26,16 @@ class verilog_typecheck_exprt:public verilog_typecheck_baset
 public:
   verilog_typecheck_exprt(
     const namespacet &_ns,
-    message_handlert &_message_handler):
-    verilog_typecheck_baset(_ns, _message_handler),
-    nondet_count(0)
+    message_handlert &_message_handler)
+    : verilog_typecheck_baset(_ns, _message_handler)
   { }
 
   verilog_typecheck_exprt(
     const namespacet &_ns,
     const std::string &_module_identifier,
-    message_handlert &_message_handler):
-    verilog_typecheck_baset(_ns, _message_handler),
-    module_identifier(_module_identifier),
-    nondet_count(0)
+    message_handlert &_message_handler)
+    : verilog_typecheck_baset(_ns, _message_handler),
+      module_identifier(_module_identifier)
   { }
 
   virtual void convert_expr(exprt &expr)
@@ -52,7 +50,6 @@ class verilog_typecheck_exprt:public verilog_typecheck_baset
 protected:
   irep_idt module_identifier;
   irep_idt function_or_task_name;
-  unsigned nondet_count;
 
   // module_identifier.function.block.base_name
   // including the Verilog:: prefix.
@@ -127,7 +124,6 @@ class verilog_typecheck_exprt:public verilog_typecheck_baset
   [[nodiscard]] exprt convert_expr_function_call(function_call_exprt);
   [[nodiscard]] exprt
   convert_system_function(const irep_idt &identifier, function_call_exprt);
-  [[nodiscard]] exprt convert_constraint_select_one(exprt);
   [[nodiscard]] exprt convert_bit_select_expr(binary_exprt);
   [[nodiscard]] exprt convert_replication_expr(replication_exprt);
   [[nodiscard]] exprt convert_shl_expr(shl_exprt);