From 491a289f65e5bfc61b3d603ef0f628a19089bf57 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Wed, 15 May 2024 12:04:15 +0100 Subject: [PATCH] Verilog: move translation of part select expressions into synthesis phase The Verilog frontend translates Verilog part select expressions into extractbits expressions. This is moved from the typechecker to the synthesis phase. --- .../verilog/synthesis/part_select1.desc | 7 + regression/verilog/synthesis/part_select1.sv | 15 + src/verilog/verilog_synthesis.cpp | 326 +++++++++++++++--- src/verilog/verilog_typecheck.cpp | 17 +- src/verilog/verilog_typecheck_expr.cpp | 84 +---- 5 files changed, 321 insertions(+), 128 deletions(-) create mode 100644 regression/verilog/synthesis/part_select1.desc create mode 100644 regression/verilog/synthesis/part_select1.sv diff --git a/regression/verilog/synthesis/part_select1.desc b/regression/verilog/synthesis/part_select1.desc new file mode 100644 index 000000000..64a1014f0 --- /dev/null +++ b/regression/verilog/synthesis/part_select1.desc @@ -0,0 +1,7 @@ +CORE +part_select1.sv + +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/verilog/synthesis/part_select1.sv b/regression/verilog/synthesis/part_select1.sv new file mode 100644 index 000000000..07bc85b68 --- /dev/null +++ b/regression/verilog/synthesis/part_select1.sv @@ -0,0 +1,15 @@ +module main; + + reg [31:0] t; + + always @(*) begin + t = 0; + + // out of bounds accesses are ignored + t[0:-1] = 'b10; + + // should pass + assert(t == 1); + end + +endmodule diff --git a/src/verilog/verilog_synthesis.cpp b/src/verilog/verilog_synthesis.cpp index c80f0c857..60954953d 100644 --- a/src/verilog/verilog_synthesis.cpp +++ b/src/verilog/verilog_synthesis.cpp @@ -96,6 +96,120 @@ exprt verilog_synthesist::synth_expr(exprt expr, symbol_statet symbol_state) return expr; } + else if(expr.id() == ID_verilog_non_indexed_part_select) + { + auto &part_select = to_verilog_non_indexed_part_select_expr(expr); + auto &src = part_select.src(); + + src = synth_expr(src, symbol_state); + + auto op1 = numeric_cast_v(to_constant_expr(part_select.msb())); + auto op2 = numeric_cast_v(to_constant_expr(part_select.lsb())); + + mp_integer src_width = get_width(src.type()); + mp_integer src_offset = string2integer(src.type().get_string(ID_C_offset)); + + // 1800-2017 sec 11.5.1: out-of-bounds bit-select is + // x for 4-state and 0 for 2-state values. We + // achieve that by padding the operand from either end, + // or both. + exprt src_padded = src; + + if(op2 < src_offset) + { + // lsb too small, pad below + auto padding_width = src_offset - op2; + auto padding = from_integer( + 0, unsignedbv_typet{numeric_cast_v(padding_width)}); + auto new_type = unsignedbv_typet{numeric_cast_v( + get_width(src_padded.type()) + padding_width)}; + src_padded = concatenation_exprt(src_padded, padding, new_type); + op2 += padding_width; + op1 += padding_width; + } + + if(op1 >= src_width + src_offset) + { + // msb too large, pad above + auto padding_width = op1 - (src_width + src_offset) + 1; + auto padding = from_integer( + 0, unsignedbv_typet{numeric_cast_v(padding_width)}); + auto new_type = unsignedbv_typet{numeric_cast_v( + get_width(src_padded.type()) + padding_width)}; + src_padded = concatenation_exprt(padding, src_padded, new_type); + } + + op2 -= src_offset; + op1 -= src_offset; + + // Construct the extractbits expression + return extractbits_exprt{ + src_padded, + from_integer(op1, integer_typet()), + from_integer(op2, integer_typet()), + expr.type()} + .with_source_location(expr.source_location()); + } + else if( + expr.id() == ID_verilog_indexed_part_select_plus || + expr.id() == ID_verilog_indexed_part_select_minus) + { + auto &part_select = to_verilog_indexed_part_select_plus_or_minus_expr(expr); + exprt &src = part_select.src(); + + mp_integer src_width = get_width(src.type()); + mp_integer src_offset = string2integer(src.type().get_string(ID_C_offset)); + + // The width of the indexed part select must be an + // elaboration-time constant. + auto width = + numeric_cast_v(to_constant_expr(part_select.width())); + + // The index need not be a constant. + exprt &index = part_select.index(); + + if(index.is_constant()) + { + auto index_int = numeric_cast_v(to_constant_expr(index)); + + // Construct the extractbits expression + mp_integer bottom, top; + + if(part_select.id() == ID_verilog_indexed_part_select_plus) + { + bottom = index_int - src_offset; + top = bottom + width; + } + else // ID_verilog_indexed_part_select_minus + { + top = index_int - src_offset; + bottom = bottom - width; + } + + return extractbits_exprt{ + std::move(src), + from_integer(top, integer_typet{}), + from_integer(bottom, integer_typet{}), + expr.type()} + .with_source_location(expr); + } + else + { + // Index not constant. + // Use logical right-shift followed by (constant) extractbits. + auto index_adjusted = + minus_exprt{index, from_integer(src_offset, index.type())}; + + auto src_shifted = lshr_exprt(src, index_adjusted); + + return extractbits_exprt{ + std::move(src_shifted), + from_integer(width - 1, integer_typet{}), + from_integer(0, integer_typet{}), + expr.type()} + .with_source_location(expr); + } + } else if(expr.has_operands()) { for(auto &op : expr.operands()) @@ -526,41 +640,36 @@ void verilog_synthesist::assignment_rec( // do the value assignment_rec(lhs_array, new_rhs, new_value); // recursive call } - else if(lhs.id()==ID_extractbits) + else if(lhs.id() == ID_verilog_non_indexed_part_select) { - // we flatten n-bit extractbits into n times extractbit - - if(lhs.operands().size()!=3) - { - throw errort() << "extractbits takes three operands"; - } + // we flatten n-bit part select into n times extractbit + auto &part_select = to_verilog_non_indexed_part_select_expr(lhs); - const exprt &lhs_bv = to_extractbits_expr(lhs).src(); - const exprt &lhs_index_one = to_extractbits_expr(lhs).upper(); - const exprt &lhs_index_two = to_extractbits_expr(lhs).lower(); + const exprt &lhs_src = part_select.src(); + const exprt &lhs_msb = part_select.msb(); + const exprt &lhs_lsb = part_select.lsb(); mp_integer from, to; - if(to_integer_non_constant(lhs_index_one, from)) + if(to_integer_non_constant(lhs_msb, to)) { - throw errort().with_location(lhs_index_one.source_location()) + throw errort().with_location(lhs_msb.source_location()) << "failed to convert range"; } - if(to_integer_non_constant(lhs_index_two, to)) + if(to_integer_non_constant(lhs_lsb, from)) { - throw errort().with_location(lhs_index_two.source_location()) + throw errort().with_location(lhs_lsb.source_location()) << "failed to convert range"; } - if(from>to) + if(from > to) std::swap(from, to); // redundant? - if(from==0 && - to==get_width(lhs_bv.type())-1) + if(from == 0 && to == get_width(lhs_src.type()) - 1) { - assignment_rec(lhs_bv, rhs, new_value); // recursive call + assignment_rec(lhs_src, rhs, new_value); // recursive call return; } @@ -569,44 +678,133 @@ void verilog_synthesist::assignment_rec( // into // a'==a WITH [i:=e] - exprt synth_lhs_bv(lhs_bv); + exprt synth_lhs_src(lhs_src); // do the array, but just once - synth_lhs_bv = synth_expr(synth_lhs_bv, symbol_statet::FINAL); + synth_lhs_src = synth_expr(synth_lhs_src, symbol_statet::FINAL); exprt last_value; last_value.make_nil(); + const auto rhs_width = get_width(lhs_src.type()); + + // We drop bits that are out of bounds + auto from_in_range = std::max(mp_integer{0}, from); + auto to_in_range = std::min(rhs_width - 1, to); + // now add the indexes in the range - for(mp_integer i=from; i<=to; ++i) + for(mp_integer i = from_in_range; i <= to_in_range; ++i) + { + exprt offset = from_integer(i - from, integer_typet()); + + exprt rhs_extractbit(ID_extractbit, bool_typet()); + rhs_extractbit.reserve_operands(2); + rhs_extractbit.add_to_operands(rhs); + rhs_extractbit.add_to_operands(std::move(offset)); + + exprt count = from_integer(i, integer_typet()); + + exprt new_rhs(ID_with, lhs_src.type()); + new_rhs.reserve_operands(3); + new_rhs.add_to_operands(synth_lhs_src); + new_rhs.add_to_operands(std::move(count)); + new_rhs.add_to_operands(std::move(rhs_extractbit)); + + // do the value + assignment_rec(lhs_src, new_rhs, new_value); // recursive call + + if(last_value.is_nil()) + last_value.swap(new_value); + else + { + // merge the withs + assert(new_value.id() == ID_with); + assert(new_value.operands().size() == 3); + assert(last_value.id() == ID_with); + assert(last_value.operands().size() >= 3); + + last_value.add_to_operands(std::move(to_with_expr(new_value).where())); + last_value.add_to_operands( + std::move(to_with_expr(new_value).new_value())); + } + } + + new_value.swap(last_value); + } + else if( + lhs.id() == ID_verilog_indexed_part_select_plus || + lhs.id() == ID_verilog_indexed_part_select_minus) + { + // we flatten n-bit part select into n times extractbit + auto &part_select = to_verilog_indexed_part_select_plus_or_minus_expr(lhs); + + const exprt &lhs_src = part_select.src(); + const exprt &lhs_index = part_select.index(); + const exprt &lhs_width = part_select.width(); + + mp_integer index, width; + + if(to_integer_non_constant(lhs_index, index)) + { + throw errort().with_location(lhs_index.source_location()) + << "failed to convert part select index"; + } + + if(to_integer_non_constant(lhs_width, width)) + { + throw errort().with_location(lhs_width.source_location()) + << "failed to convert part select width"; + } + + // turn + // a[i]=e + // into + // a'==a WITH [i:=e] + + exprt synth_lhs_src(lhs_src); + + // do the array, but just once + synth_lhs_src = synth_expr(synth_lhs_src, symbol_statet::FINAL); + + exprt last_value; + last_value.make_nil(); + + const auto rhs_width = get_width(lhs_src.type()); + + // We drop bits that are out of bounds + auto from_in_range = std::max(mp_integer{0}, index); + auto to_in_range = std::min(rhs_width - 1, index + width); + + // now add the indexes in the range + for(mp_integer i = from_in_range; i <= to_in_range; ++i) { - exprt offset=from_integer(i-from, integer_typet()); + exprt offset = from_integer(i - index, integer_typet()); exprt rhs_extractbit(ID_extractbit, bool_typet()); rhs_extractbit.reserve_operands(2); rhs_extractbit.add_to_operands(rhs); rhs_extractbit.add_to_operands(std::move(offset)); - exprt count=from_integer(i, integer_typet()); + exprt count = from_integer(i, integer_typet()); - exprt new_rhs(ID_with, lhs_bv.type()); + exprt new_rhs(ID_with, lhs_src.type()); new_rhs.reserve_operands(3); - new_rhs.add_to_operands(synth_lhs_bv); + new_rhs.add_to_operands(synth_lhs_src); new_rhs.add_to_operands(std::move(count)); new_rhs.add_to_operands(std::move(rhs_extractbit)); // do the value - assignment_rec(lhs_bv, new_rhs, new_value); // recursive call + assignment_rec(lhs_src, new_rhs, new_value); // recursive call if(last_value.is_nil()) last_value.swap(new_value); else { // merge the withs - assert(new_value.id()==ID_with); - assert(new_value.operands().size()==3); - assert(last_value.id()==ID_with); - assert(last_value.operands().size()>=3); + assert(new_value.id() == ID_with); + assert(new_value.operands().size() == 3); + assert(last_value.id() == ID_with); + assert(last_value.operands().size() >= 3); last_value.add_to_operands(std::move(to_with_expr(new_value).where())); last_value.add_to_operands( @@ -758,18 +956,14 @@ void verilog_synthesist::assignment_member_rec( member.pop_back(); } } - else if(lhs.id()==ID_extractbits) + else if(lhs.id() == ID_verilog_non_indexed_part_select) { - // we flatten n-bit extractbits into n times extractbit - - if(lhs.operands().size()!=3) - { - throw errort() << "extractbits takes three operands"; - } + // we flatten n-bit part select into n times extractbit + auto &part_select = to_verilog_non_indexed_part_select_expr(lhs); - const exprt &lhs_bv = to_extractbits_expr(lhs).src(); - const exprt &lhs_index_one = to_extractbits_expr(lhs).upper(); - const exprt &lhs_index_two = to_extractbits_expr(lhs).lower(); + const exprt &lhs_bv = part_select.src(); + const exprt &lhs_index_one = part_select.msb(); + const exprt &lhs_index_two = part_select.lsb(); mp_integer from, to; @@ -800,6 +994,43 @@ void verilog_synthesist::assignment_member_rec( member.pop_back(); } + else if( + lhs.id() == ID_verilog_indexed_part_select_plus || + lhs.id() == ID_verilog_indexed_part_select_minus) + { + // we flatten n-bit part select into n times extractbit + auto &part_select = to_verilog_indexed_part_select_plus_or_minus_expr(lhs); + + const exprt &lhs_bv = part_select.src(); + const exprt &lhs_index = part_select.index(); + const exprt &lhs_width = part_select.width(); + + mp_integer index, width; + + if(to_integer_non_constant(lhs_index, index)) + { + throw errort().with_location(lhs_index.source_location()) + << "failed to convert part select index"; + } + + if(to_integer_non_constant(lhs_width, width)) + { + throw errort().with_location(lhs_width.source_location()) + << "failed to convert part select width"; + } + + member.push_back(mp_integer()); + + // now add the indexes in the range + for(mp_integer i = index; i <= index + width; ++i) + { + // do the value + member.back() = i; + assignment_member_rec(lhs_bv, member, data); + } + + member.pop_back(); + } else if(lhs.id() == ID_member) { add_assignment_member(lhs, member, data); @@ -909,14 +1140,15 @@ const symbolt &verilog_synthesist::assignment_symbol(const exprt &lhs) e = &to_extractbit_expr(*e).src(); } - else if(e->id()==ID_extractbits) + else if(e->id() == ID_verilog_non_indexed_part_select) { - if(e->operands().size()!=3) - { - throw errort() << "extractbits takes three operands"; - } - - e = &to_extractbits_expr(*e).src(); + e = &to_verilog_non_indexed_part_select_expr(*e).src(); + } + else if( + e->id() == ID_verilog_indexed_part_select_plus || + e->id() == ID_verilog_indexed_part_select_minus) + { + e = &to_verilog_indexed_part_select_plus_or_minus_expr(*e).src(); } else if(e->id()==ID_symbol) { diff --git a/src/verilog/verilog_typecheck.cpp b/src/verilog/verilog_typecheck.cpp index 52a67a2ff..b8aeaff39 100644 --- a/src/verilog/verilog_typecheck.cpp +++ b/src/verilog/verilog_typecheck.cpp @@ -681,14 +681,17 @@ void verilog_typecheckt::check_lhs( check_lhs(to_extractbit_expr(lhs).src(), vassign); } - else if(lhs.id()==ID_extractbits) + else if(lhs.id() == ID_verilog_non_indexed_part_select) { - if(lhs.operands().size()!=3) - { - throw errort() << "extractbits takes three operands"; - } - - check_lhs(to_extractbits_expr(lhs).src(), vassign); + auto &part_select = to_verilog_non_indexed_part_select_expr(lhs); + check_lhs(part_select.src(), vassign); + } + else if( + lhs.id() == ID_verilog_indexed_part_select_plus || + lhs.id() == ID_verilog_indexed_part_select_minus) + { + auto &part_select = to_verilog_indexed_part_select_plus_or_minus_expr(lhs); + check_lhs(part_select.src(), vassign); } else if(lhs.id()==ID_concatenation) { diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp index c270f7bc3..8cf84cc3e 100644 --- a/src/verilog/verilog_typecheck_expr.cpp +++ b/src/verilog/verilog_typecheck_expr.cpp @@ -2344,44 +2344,17 @@ exprt verilog_typecheck_exprt::convert_trinary_expr(ternary_exprt expr) if(msb < lsb) std::swap(msb, lsb); // now msb>=lsb - // 1800-2017 sec 11.5.1: out-of-bounds bit-select is - // x for 4-state and 0 for 2-state values. We - // achieve that by padding the operand from either end, - // or both. - if(lsb < src_offset) - { - auto padding_width = src_offset - lsb; - auto padding = from_integer( - 0, unsignedbv_typet{numeric_cast_v(padding_width)}); - auto new_type = unsignedbv_typet{ - numeric_cast_v(get_width(src.type()) + padding_width)}; - src = concatenation_exprt(src, padding, new_type); - lsb += padding_width; - msb += padding_width; - } - - if(msb >= src_width + src_offset) - { - auto padding_width = msb - (src_width + src_offset) + 1; - auto padding = from_integer( - 0, unsignedbv_typet{numeric_cast_v(padding_width)}); - auto new_type = unsignedbv_typet{ - numeric_cast_v(get_width(src.type()) + padding_width)}; - src = concatenation_exprt(padding, src, new_type); - } + // store these back onto the expression + expr.op1() = from_integer(msb, integer_typet()) + .with_source_location(expr.op1().source_location()); + expr.op2() = from_integer(lsb, integer_typet()) + .with_source_location(expr.op2().source_location()); // Part-select expressions are unsigned, even if the - // entire expression is selected! + // op0 is signed and the entire expression is selected! auto expr_type = unsignedbv_typet{numeric_cast_v(msb - lsb + 1)}; - lsb -= src_offset; - msb -= src_offset; - - // Construct the extractbits expression - expr.id(ID_extractbits); - expr.op1() = from_integer(msb, integer_typet()); - expr.op2() = from_integer(lsb, integer_typet()); expr.type() = expr_type; return std::move(expr); @@ -2424,50 +2397,13 @@ exprt verilog_typecheck_exprt::convert_trinary_expr(ternary_exprt expr) << "width of indexed part select must be positive"; } + part_select.width() = from_integer(width, integer_typet()); + // Part-select expressions are unsigned, even if the // entire expression is selected! - auto expr_type = unsignedbv_typet{numeric_cast_v(width)}; - - mp_integer index_int; - if(is_constant_expression(index, index_int)) - { - // Construct the extractbits expression - mp_integer bottom, top; - - if(part_select.id() == ID_verilog_indexed_part_select_plus) - { - bottom = index_int - src_offset; - top = bottom + width; - } - else // ID_verilog_indexed_part_select_minus - { - top = index_int - src_offset; - bottom = bottom - width; - } - - return extractbits_exprt{ - std::move(src), - from_integer(top, integer_typet{}), - from_integer(bottom, integer_typet{}), - std::move(expr_type)} - .with_source_location(expr); - } - else - { - // Index not constant. - // Use logical right-shift followed by (constant) extractbits. - auto index_adjusted = - minus_exprt{index, from_integer(src_offset, index.type())}; - - auto src_shifted = lshr_exprt(src, index_adjusted); + expr.type() = unsignedbv_typet{numeric_cast_v(width)}; - return extractbits_exprt{ - std::move(src_shifted), - from_integer(width - 1, integer_typet{}), - from_integer(0, integer_typet{}), - std::move(expr_type)} - .with_source_location(expr); - } + return std::move(expr); } else if(expr.id()==ID_if) {