diff --git a/regression/verilog/system-functions/array_functions1.desc b/regression/verilog/system-functions/array_functions1.desc new file mode 100644 index 000000000..e839304b2 --- /dev/null +++ b/regression/verilog/system-functions/array_functions1.desc @@ -0,0 +1,22 @@ +CORE +array_functions1.sv +--module main --bound 0 +^\[main\.pP0\] always 32 == 32 && 1 == 1: PROVED up to bound 0$ +^\[main\.pP1\] always 0 == 0 && 31 == 31: PROVED up to bound 0$ +^\[main\.pP2\] always 1 == 1 && 32 == 32: PROVED up to bound 0$ +^\[main\.pP3\] always 0 == 0 && 31 == 31: PROVED up to bound 0$ +^\[main\.pP4\] always 1 == 1: PROVED up to bound 0$ +^\[main\.pP5\] always -1 == -1: PROVED up to bound 0$ +^\[main\.pU0\] always 32 == 32 && 1 == 1: PROVED up to bound 0$ +^\[main\.pU1\] always 0 == 0 && 31 == 31: PROVED up to bound 0$ +^\[main\.pU2\] always 31 == 31 && 0 == 0: PROVED up to bound 0$ +^\[main\.pU3\] always 1 == 1 && 32 == 32: PROVED up to bound 0$ +^\[main\.pU4\] always 0 == 0 && 31 == 31: PROVED up to bound 0$ +^\[main\.pU5\] always 0 == 0 && 31 == 31: PROVED up to bound 0$ +^\[main\.pU6\] always 1 == 1: PROVED up to bound 0$ +^\[main\.pU7\] always -1 == -1: PROVED up to bound 0$ +^\[main\.pU8\] always 1 == 1: PROVED up to bound 0$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/verilog/system-functions/array_functions1.sv b/regression/verilog/system-functions/array_functions1.sv new file mode 100644 index 000000000..b348dbbf9 --- /dev/null +++ b/regression/verilog/system-functions/array_functions1.sv @@ -0,0 +1,27 @@ +module main; + + wire [32:1] packed1; + wire [0:31] packed2; + + wire unpacked1 [32:1]; + wire unpacked2 [0:31]; + wire unpacked3 [32]; + + pP0: assert property ($left(packed1) == 32 and $right(packed1) == 1); + pP1: assert property ($left(packed2) == 0 and $right(packed2) == 31); + pP2: assert property ($low(packed1) == 1 and $high(packed1) == 32); + pP3: assert property ($low(packed2) == 0 and $high(packed2) == 31); + pP4: assert property ($increment(packed1) == 1); + pP5: assert property ($increment(packed2) == -1); + + pU0: assert property ($left(unpacked1) == 32 and $right(unpacked1) == 1); + pU1: assert property ($left(unpacked2) == 0 and $right(unpacked2) == 31); + pU2: assert property ($left(unpacked3) == 31 and $right(unpacked3) == 0); + pU3: assert property ($low(unpacked1) == 1 and $high(unpacked1) == 32); + pU4: assert property ($low(unpacked2) == 0 and $high(unpacked2) == 31); + pU5: assert property ($low(unpacked3) == 0 and $high(unpacked3) == 31); + pU6: assert property ($increment(unpacked1) == 1); + pU7: assert property ($increment(unpacked2) == -1); + pU8: assert property ($increment(unpacked3) == 1); + +endmodule diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp index 74285f441..cc9c93b5e 100644 --- a/src/verilog/verilog_typecheck_expr.cpp +++ b/src/verilog/verilog_typecheck_expr.cpp @@ -447,6 +447,179 @@ exprt verilog_typecheck_exprt::bits(const exprt &expr) /*******************************************************************\ +Function: verilog_typecheck_exprt::left + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +constant_exprt verilog_typecheck_exprt::left(const exprt &expr) +{ + // unpacked array: left bound + // packed array: index of most significant element + // 0 otherwise + auto left = [](const typet &type) -> mp_integer { + if( + type.id() == ID_unsignedbv || type.id() == ID_signedbv || + type.id() == ID_verilog_unsignedbv || type.id() == ID_verilog_signedbv || + type.id() == ID_bool) + { + auto offset = type.get_int(ID_C_offset); + if(type.get_bool(ID_C_little_endian)) + return offset + get_width(type) - 1; + else + return offset; + } + else if(type.id() == ID_array) + { + auto offset = numeric_cast_v( + to_constant_expr(static_cast(type.find(ID_offset)))); + if(type.get_bool(ID_C_little_endian)) + return offset + + numeric_cast_v( + to_constant_expr(to_array_type(type).size())) - + 1; + else + return offset; + } + else + return 0; + }; + + return from_integer(left(expr.type()), integer_typet{}); +} + +/*******************************************************************\ + +Function: verilog_typecheck_exprt::right + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +constant_exprt verilog_typecheck_exprt::right(const exprt &expr) +{ + // unpacked array: right bound + // packed array: index of least significant element + // 0 otherwise + auto right = [](const typet &type) -> mp_integer { + if( + type.id() == ID_unsignedbv || type.id() == ID_signedbv || + type.id() == ID_verilog_unsignedbv || type.id() == ID_verilog_signedbv || + type.id() == ID_bool) + { + auto offset = type.get_int(ID_C_offset); + if(type.get_bool(ID_C_little_endian)) + return offset; + else + return offset + get_width(type) - 1; + } + else if(type.id() == ID_array) + { + auto offset = numeric_cast_v( + to_constant_expr(static_cast(type.find(ID_offset)))); + if(type.get_bool(ID_C_little_endian)) + return offset; + else + return offset + + numeric_cast_v( + to_constant_expr(to_array_type(type).size())) - + 1; + } + else + return 0; + }; + + return from_integer(right(expr.type()), integer_typet{}); +} + +/*******************************************************************\ + +Function: verilog_typecheck_exprt::increment + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +constant_exprt verilog_typecheck_exprt::increment(const exprt &expr) +{ + // fixed-size dimension: 1 if $left >= $right, -1 otherwise + auto increment = [](const typet &type) -> mp_integer { + if( + type.id() == ID_unsignedbv || type.id() == ID_signedbv || + type.id() == ID_verilog_unsignedbv || type.id() == ID_verilog_signedbv || + type.id() == ID_array) + { + if(type.get_bool(ID_C_little_endian)) + return 1; + else + return -1; + } + else + return -1; + }; + + return from_integer(increment(expr.type()), integer_typet{}); +} + +/*******************************************************************\ + +Function: verilog_typecheck_exprt::low + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +constant_exprt verilog_typecheck_exprt::low(const exprt &expr) +{ + // $left if $increment returns –1 + // $right otherwise + if(numeric_cast_v(increment(expr)) == -1) + return left(expr); + else + return right(expr); +} + +/*******************************************************************\ + +Function: verilog_typecheck_exprt::high + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +constant_exprt verilog_typecheck_exprt::high(const exprt &expr) +{ + // $right if $increment returns –1 + // $left otherwise + if(numeric_cast_v(increment(expr)) == -1) + return right(expr); + else + return left(expr); +} + +/*******************************************************************\ + Function: verilog_typecheck_exprt::convert_system_function Inputs: @@ -549,12 +722,14 @@ exprt verilog_typecheck_exprt::convert_system_function( expr.type() = arguments.front().type(); return std::move(expr); } - else if(identifier == "$bits") + else if( + identifier == "$bits" || identifier == "$left" || identifier == "$right" || + identifier == "$increment" || identifier == "$low" || identifier == "$high") { if(arguments.size() != 1) { throw errort().with_location(expr.source_location()) - << "$bits takes one argument"; + << identifier << " takes one argument"; } // The return type is integer. @@ -1370,6 +1545,31 @@ exprt verilog_typecheck_exprt::elaborate_constant_system_function_call( DATA_INVARIANT(arguments.size() == 1, "$bits has one argument"); return bits(arguments[0]); } + else if(identifier == "$low") + { + DATA_INVARIANT(arguments.size() == 1, "$low has one argument"); + return low(arguments[0]); + } + else if(identifier == "$high") + { + DATA_INVARIANT(arguments.size() == 1, "$high has one argument"); + return high(arguments[0]); + } + else if(identifier == "$left") + { + DATA_INVARIANT(arguments.size() == 1, "$left has one argument"); + return left(arguments[0]); + } + else if(identifier == "$right") + { + DATA_INVARIANT(arguments.size() == 1, "$right has one argument"); + return right(arguments[0]); + } + else if(identifier == "$increment") + { + DATA_INVARIANT(arguments.size() == 1, "$increment has one argument"); + return increment(arguments[0]); + } 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 dd866411d..4848ade2e 100644 --- a/src/verilog/verilog_typecheck_expr.h +++ b/src/verilog/verilog_typecheck_expr.h @@ -133,8 +133,14 @@ class verilog_typecheck_exprt:public verilog_typecheck_baset void tc_binary_expr(const exprt &expr, exprt &op0, exprt &op1); void no_bool_ops(exprt &); + // system functions exprt bits(const exprt &); std::optional bits_rec(const typet &) const; + constant_exprt left(const exprt &); + constant_exprt right(const exprt &); + constant_exprt low(const exprt &); + constant_exprt high(const exprt &); + constant_exprt increment(const exprt &); }; bool verilog_typecheck(