diff --git a/regression/verilog/structs/structs1.desc b/regression/verilog/structs/structs1.desc index 7d5f9568a..a097603ef 100644 --- a/regression/verilog/structs/structs1.desc +++ b/regression/verilog/structs/structs1.desc @@ -1,8 +1,10 @@ -KNOWNBUG +CORE structs1.sv --bound 0 +^\[main\.property\.p0\] always 9 == 9: PROVED up to bound 0$ +^\[main\.property\.p1\] always main\.s\.field1 == 1: PROVED up to bound 0$ +^\[main\.property\.p2\] always main\.s\.field2 == 0: PROVED up to bound 0$ +^\[main\.property\.p3\] always main\.s\.field3 == 115: PROVED up to bound 0$ ^EXIT=0$ ^SIGNAL=0$ -- --- -cast bitvector to struct missing diff --git a/regression/verilog/structs/structs1.sv b/regression/verilog/structs/structs1.sv index 1c0d5cded..3d8d9d4e8 100644 --- a/regression/verilog/structs/structs1.sv +++ b/regression/verilog/structs/structs1.sv @@ -7,12 +7,12 @@ module main; } s; // bit-vectors can be converted without cast to packed structs - initial s = 8'b1011111; + initial s = 'b1_0_1110011; // Expected to pass. p0: assert property ($bits(s) == 9); p1: assert property (s.field1 == 1); p2: assert property (s.field2 == 0); - p3: assert property (s.field3 == 'b111111); + p3: assert property (s.field3 == 'b1110011); endmodule diff --git a/src/verilog/verilog_synthesis.cpp b/src/verilog/verilog_synthesis.cpp index 2bf5d00b0..5d5bf026d 100644 --- a/src/verilog/verilog_synthesis.cpp +++ b/src/verilog/verilog_synthesis.cpp @@ -30,6 +30,136 @@ Author: Daniel Kroening, kroening@kroening.com /*******************************************************************\ +Function: verilog_synthesist::extract + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +exprt verilog_synthesist::extract( + const exprt &src, + const mp_integer &offset, + const typet &dest_type) +{ + auto src_width = to_bitvector_type(src.type()).get_width(); + auto dest_width = get_width(dest_type); + + // first add padding, if src is too small + exprt padded_src; + auto padding_width = dest_width + offset - src_width; + + if(padding_width > 0) + { + auto padded_width_int = + numeric_cast_v(src_width + padding_width); + padded_src = concatenation_exprt{ + {unsignedbv_typet{numeric_cast_v(padding_width)}.zero_expr(), + src}, + bv_typet{padded_width_int}}; + } + else // large enough + padded_src = src; + + // now extract + if(dest_type.id() == ID_bool) + { + return extractbit_exprt{padded_src, from_integer(offset, integer_typet{})}; + } + else + { + return extractbits_exprt{ + padded_src, from_integer(offset, integer_typet{}), dest_type}; + } +} + +/*******************************************************************\ + +Function: verilog_synthesist::from_bitvector + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +exprt verilog_synthesist::from_bitvector( + const exprt &src, + const mp_integer &offset, + const typet &dest) +{ + if(dest.id() == ID_struct) + { + const auto &struct_type = to_struct_type(dest); + exprt::operandst field_values; + field_values.reserve(struct_type.components().size()); + + // start from the top; the first field is the most significant + mp_integer component_offset = get_width(dest); + + for(auto &component : struct_type.components()) + { + auto width = get_width(component.type()); + component_offset -= width; + // rec. call + field_values.push_back( + from_bitvector(src, offset + component_offset, component.type())); + } + + return struct_exprt{std::move(field_values), struct_type}; + } + else + { + return extract(src, offset, dest); + } +} + +/*******************************************************************\ + +Function: verilog_synthesist::to_bitvector + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +exprt verilog_synthesist::to_bitvector(const exprt &src) +{ + const auto &src_type = src.type(); + + if(src_type.id() == ID_struct) + { + const auto &struct_type = to_struct_type(src_type); + exprt::operandst field_values; + field_values.reserve(struct_type.components().size()); + + // the first struct member is the most significant + for(auto &component : struct_type.components()) + { + auto member = member_exprt{src, component}; + auto field_value = to_bitvector(member); // rec. call + field_values.push_back(std::move(field_value)); + } + + auto width_int = numeric_cast_v(get_width(src)); + return concatenation_exprt{std::move(field_values), bv_typet{width_int}}; + } + else + { + return src; + } +} + +/*******************************************************************\ + Function: verilog_synthesist::synth_expr Inputs: @@ -100,23 +230,45 @@ exprt verilog_synthesist::synth_expr(exprt expr, symbol_statet symbol_state) } else if(expr.id()==ID_typecast) { - auto &typecast_expr = to_typecast_expr(expr); - typecast_expr.op() = synth_expr(typecast_expr.op(), symbol_state); + { + auto &op = to_typecast_expr(expr).op(); + op = synth_expr(op, symbol_state); - // we perform some form of simplification for these - if(typecast_expr.op().is_constant()) - simplify(expr, ns); + // we perform some form of simplification for these + if(op.is_constant()) + simplify(expr, ns); + } - if( - expr.type().id() == ID_verilog_unsignedbv || - expr.type().id() == ID_verilog_signedbv) + if(expr.id() == ID_typecast) { - auto aval_bval_type = lower_to_aval_bval(expr.type()); + auto &typecast_expr = to_typecast_expr(expr); + typecast_expr.op() = synth_expr(typecast_expr.op(), symbol_state); - if(is_aval_bval(typecast_expr.op().type())) + const auto &src_type = typecast_expr.op().type(); + const auto &dest_type = typecast_expr.type(); + + if( + dest_type.id() == ID_verilog_unsignedbv || + dest_type.id() == ID_verilog_signedbv) + { + auto aval_bval_type = lower_to_aval_bval(dest_type); + + if(is_aval_bval(src_type)) + { + // separately convert aval and bval + return aval_bval_conversion(typecast_expr.op(), aval_bval_type); + } + } + else if(dest_type.id() == ID_struct) { - // separately convert aval and bval - return aval_bval_conversion(typecast_expr.op(), aval_bval_type); + return from_bitvector(typecast_expr.op(), 0, dest_type); + } + else + { + if(src_type.id() == ID_struct) + { + return extract(to_bitvector(typecast_expr.op()), 0, dest_type); + } } } diff --git a/src/verilog/verilog_synthesis_class.h b/src/verilog/verilog_synthesis_class.h index 26e5b0916..70354d7ed 100644 --- a/src/verilog/verilog_synthesis_class.h +++ b/src/verilog/verilog_synthesis_class.h @@ -71,6 +71,11 @@ class verilog_synthesist: protected: const optionst &options; + static exprt extract(const exprt &, const mp_integer &offset, const typet &); + static exprt + from_bitvector(const exprt &, const mp_integer &offset, const typet &); + static exprt to_bitvector(const exprt &); + // For $ND(...) std::size_t nondet_count = 0;