diff --git a/regression/verilog/system-functions/countones1.desc b/regression/verilog/system-functions/countones1.desc new file mode 100644 index 000000000..163f089cc --- /dev/null +++ b/regression/verilog/system-functions/countones1.desc @@ -0,0 +1,7 @@ +CORE +countones1.sv +--module main --bound 0 +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/verilog/system-functions/countones1.sv b/regression/verilog/system-functions/countones1.sv new file mode 100644 index 000000000..e32e6999e --- /dev/null +++ b/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 diff --git a/regression/verilog/system-functions/countones2.desc b/regression/verilog/system-functions/countones2.desc new file mode 100644 index 000000000..5cb9850ef --- /dev/null +++ b/regression/verilog/system-functions/countones2.desc @@ -0,0 +1,7 @@ +CORE +countones2.sv +--bound 50 +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/verilog/system-functions/countones2.sv b/regression/verilog/system-functions/countones2.sv new file mode 100644 index 000000000..72d9556f3 --- /dev/null +++ b/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 diff --git a/src/verilog/verilog_synthesis.cpp b/src/verilog/verilog_synthesis.cpp index 617502d39..0d22c123c 100644 --- a/src/verilog/verilog_synthesis.cpp +++ b/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. diff --git a/src/verilog/verilog_synthesis_class.h b/src/verilog/verilog_synthesis_class.h index 777c62d29..de4b607d8 100644 --- a/src/verilog/verilog_synthesis_class.h +++ b/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 replace_mapt; diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp index 28618db5b..aafd7dbfd 100644 --- a/src/verilog/verilog_typecheck_expr.cpp +++ b/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 diff --git a/src/verilog/verilog_typecheck_expr.h b/src/verilog/verilog_typecheck_expr.h index afebb185f..70caa618c 100644 --- a/src/verilog/verilog_typecheck_expr.h +++ b/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 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 &); diff --git a/src/verilog/verilog_types.h b/src/verilog/verilog_types.h index 73db4c5ce..842d23f82 100644 --- a/src/verilog/verilog_types.h +++ b/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