Merge pull request #619 from diffblue/countones1

SystemVerilog: $countones

Author: tautschnig

regression/verilog/system-functions/countones1.desc

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

regression/verilog/system-functions/countones1.sv

@@ -0,0 +1,9 @@
+module main;
+
+  always assert ($countones('b10101)==3);
+
+  // $countones yields an elaboration-time constant
+  parameter P = 123;
+  parameter Q = $countones(P);
+
+endmodule

regression/verilog/system-functions/countones2.desc

@@ -0,0 +1,7 @@
+CORE
+countones2.sv
+--bound 50
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/verilog/system-functions/countones2.sv

@@ -0,0 +1,12 @@
+module gray_counter#(N = 4) (input clk, output [N-1:0] out);
+
+  reg [N-1:0] state = 0;
+  assign out = {state[N-1], state[N-1:1] ^ state[N-2:0]};
+
+  always_ff @(posedge clk) state++;
+
+  // two successive values differ in one bit exactly
+  p0: assert property (@(posedge clk)
+       ##1 $countones($past(out) ^ out) == 1);
+
+endmodule

src/verilog/verilog_synthesis.cpp

@@ -235,7 +235,7 @@ exprt verilog_synthesist::synth_expr(exprt expr, symbol_statet symbol_state)
   }
   else if(expr.id()==ID_function_call)
   {
-    return expand_function_call(to_function_call_expr(expr));
+    return expand_function_call(to_function_call_expr(expr), symbol_state);
   }
   else if(expr.id()==ID_hierarchical_identifier)
   {
@@ -461,7 +461,9 @@ Function: verilog_synthesist::expand_function_call
 
 \*******************************************************************/
 
-exprt verilog_synthesist::expand_function_call(const function_call_exprt &call)
+exprt verilog_synthesist::expand_function_call(
+  const function_call_exprt &call,
+  symbol_statet symbol_state)
 {
   // Is it a 'system function call'?
   if(call.is_system_function_call())
@@ -511,6 +513,14 @@ exprt verilog_synthesist::expand_function_call(const function_call_exprt &call)
       else
         DATA_INVARIANT(false, "all cases covered");
     }
+    else if(identifier == "$countones")
+    {
+      // lower to popcount
+      DATA_INVARIANT(
+        call.arguments().size() == 1, "$countones must have one argument");
+      auto what = synth_expr(call.arguments()[0], symbol_state); // rec. call
+      return popcount_exprt{what, call.type()};
+    }
     else
     {
       // Attempt to constant fold.

src/verilog/verilog_synthesis_class.h

@@ -304,7 +304,8 @@ class verilog_synthesist:
     class hierarchical_identifier_exprt &expr,
     symbol_statet symbol_state);
 
-  exprt expand_function_call(const class function_call_exprt &call);
+  exprt
+  expand_function_call(const class function_call_exprt &call, symbol_statet);
 
   typedef std::map<irep_idt, exprt> replace_mapt;
 

src/verilog/verilog_typecheck_expr.cpp

@@ -561,6 +561,33 @@ constant_exprt verilog_typecheck_exprt::right(const exprt &expr)
 
 /*******************************************************************\
 
+Function: verilog_typecheck_exprt::countones
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+constant_exprt verilog_typecheck_exprt::countones(const constant_exprt &expr)
+{
+  // lower to popcount and try simplifier
+  auto simplified =
+    simplify_expr(popcount_exprt{expr, verilog_int_typet{}.lower()}, ns);
+
+  if(!simplified.is_constant())
+  {
+    throw errort{}.with_location(expr.source_location())
+      << "failed to simplify constant $countones";
+  }
+  else
+    return to_constant_expr(simplified);
+}
+
+/*******************************************************************\
+
 Function: verilog_typecheck_exprt::increment
 
   Inputs:
@@ -755,6 +782,19 @@ exprt verilog_typecheck_exprt::convert_system_function(
 
     return std::move(expr);
   }
+  else if(identifier == "$countones") // SystemVerilog
+  {
+    if(arguments.size() != 1)
+    {
+      throw errort().with_location(expr.source_location())
+        << "$countones takes one argument";
+    }
+
+    // The return type is 'int'
+    expr.type() = verilog_int_typet{}.lower();
+
+    return std::move(expr);
+  }
   else if(identifier=="$onehot") // SystemVerilog
   {
     if(arguments.size()!=1)
@@ -1586,6 +1626,17 @@ exprt verilog_typecheck_exprt::elaborate_constant_system_function_call(
     DATA_INVARIANT(arguments.size() == 1, "$increment has one argument");
     return increment(arguments[0]);
   }
+  else if(identifier == "$countones")
+  {
+    DATA_INVARIANT(arguments.size() == 1, "$countones has one argument");
+
+    auto op = elaborate_constant_expression(arguments[0]);
+
+    if(!op.is_constant())
+      return std::move(expr); // give up
+
+    return countones(to_constant_expr(op));
+  }
   else if(identifier == "$clog2")
   {
     // the ceiling of the log with base 2 of the argument

src/verilog/verilog_typecheck_expr.h

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

src/verilog/verilog_types.h

@@ -218,6 +218,11 @@ class verilog_int_typet : public typet
   {
     return 32;
   }
+
+  typet lower() const
+  {
+    return signedbv_typet{width()};
+  }
 };
 
 /// 2-state data type, 64-bit signed integer