SystemVerilog: $countones

This adds the SystemVerilog system function $countones (IEEE 1800-2017 20.9).

Author: kroening

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 @@
+KNOWNBUG
+countones2.sv
+--bound 10
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/verilog/system-functions/countones2.sv

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

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