Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 7 additions & 0 deletions regression/verilog/system-functions/countones1.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
CORE
countones1.sv
--module main --bound 0
^EXIT=0$
^SIGNAL=0$
--
^warning: ignoring
9 changes: 9 additions & 0 deletions regression/verilog/system-functions/countones1.sv
Original file line number Diff line number Diff line change
@@ -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
7 changes: 7 additions & 0 deletions regression/verilog/system-functions/countones2.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
CORE
countones2.sv
--bound 50
^EXIT=0$
^SIGNAL=0$
--
^warning: ignoring
12 changes: 12 additions & 0 deletions regression/verilog/system-functions/countones2.sv
Original file line number Diff line number Diff line change
@@ -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
14 changes: 12 additions & 2 deletions src/verilog/verilog_synthesis.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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)
{
Expand Down Expand Up @@ -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())
Expand Down Expand Up @@ -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.
Expand Down
3 changes: 2 additions & 1 deletion src/verilog/verilog_synthesis_class.h
Original file line number Diff line number Diff line change
Expand Up @@ -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;

Expand Down
51 changes: 51 additions & 0 deletions src/verilog/verilog_typecheck_expr.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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
Expand Down
1 change: 1 addition & 0 deletions src/verilog/verilog_typecheck_expr.h
Original file line number Diff line number Diff line change
Expand Up @@ -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 &);
Expand Down
5 changes: 5 additions & 0 deletions src/verilog/verilog_types.h
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down