From 8b19daffd5cca365340772ae49460beef4ac655d Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 19 Mar 2024 07:40:32 -0700 Subject: [PATCH] Verilog: indexed part select expressions with non-constant index This implements support for indexed part select expressions where the index is not an elaboration-time constant. --- .../verilog/part-select/index-of-real.desc | 8 + .../verilog/part-select/index-of-real.sv | 7 + .../indexed-part-select1.desc} | 4 +- .../indexed-part-select1.sv} | 3 +- .../part-select/indexed-part-select2.desc | 8 + .../part-select/indexed-part-select2.sv | 6 + .../part-select/indexed-part-select3.desc | 8 + .../part-select/indexed-part-select3.sv | 9 ++ .../part-select/part-select-of-real.desc | 8 + .../part-select/part-select-of-real.sv | 7 + .../verilog/part-select/real-index.desc | 8 + regression/verilog/part-select/real-index.sv | 7 + src/hw_cbmc_irep_ids.h | 6 +- src/verilog/parser.y | 57 ++----- src/verilog/verilog_typecheck_expr.cpp | 141 +++++++++++++++--- 15 files changed, 217 insertions(+), 70 deletions(-) create mode 100644 regression/verilog/part-select/index-of-real.desc create mode 100644 regression/verilog/part-select/index-of-real.sv rename regression/verilog/{indexed-part-select1/test.desc => part-select/indexed-part-select1.desc} (66%) rename regression/verilog/{indexed-part-select1/main.sv => part-select/indexed-part-select1.sv} (71%) create mode 100644 regression/verilog/part-select/indexed-part-select2.desc create mode 100644 regression/verilog/part-select/indexed-part-select2.sv create mode 100644 regression/verilog/part-select/indexed-part-select3.desc create mode 100644 regression/verilog/part-select/indexed-part-select3.sv create mode 100644 regression/verilog/part-select/part-select-of-real.desc create mode 100644 regression/verilog/part-select/part-select-of-real.sv create mode 100644 regression/verilog/part-select/real-index.desc create mode 100644 regression/verilog/part-select/real-index.sv diff --git a/regression/verilog/part-select/index-of-real.desc b/regression/verilog/part-select/index-of-real.desc new file mode 100644 index 000000000..6b38ffc41 --- /dev/null +++ b/regression/verilog/part-select/index-of-real.desc @@ -0,0 +1,8 @@ +CORE +index-of-real.sv + +^file .* line 5: bit-select of real is not allowed$ +^EXIT=2$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/verilog/part-select/index-of-real.sv b/regression/verilog/part-select/index-of-real.sv new file mode 100644 index 000000000..f3f2b6a76 --- /dev/null +++ b/regression/verilog/part-select/index-of-real.sv @@ -0,0 +1,7 @@ +module main; + + // 1800-2017 6.12.1 + real some_real; + wire x = some_real[0]; + +endmodule diff --git a/regression/verilog/indexed-part-select1/test.desc b/regression/verilog/part-select/indexed-part-select1.desc similarity index 66% rename from regression/verilog/indexed-part-select1/test.desc rename to regression/verilog/part-select/indexed-part-select1.desc index 8161014e3..39181c2be 100644 --- a/regression/verilog/indexed-part-select1/test.desc +++ b/regression/verilog/part-select/indexed-part-select1.desc @@ -1,6 +1,6 @@ CORE broken-smt-backend -main.sv ---bound 1 +indexed-part-select1.sv +--bound 0 ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/indexed-part-select1/main.sv b/regression/verilog/part-select/indexed-part-select1.sv similarity index 71% rename from regression/verilog/indexed-part-select1/main.sv rename to regression/verilog/part-select/indexed-part-select1.sv index 84abb2517..c4c127aa6 100644 --- a/regression/verilog/indexed-part-select1/main.sv +++ b/regression/verilog/part-select/indexed-part-select1.sv @@ -9,7 +9,6 @@ module main(in); out[16 +: 16]=0; end - always assert property1: - { in, { 8 { 1'b0 }} } == out; + p1: assert property ({ in, { 8 { 1'b0 }} } == out); endmodule diff --git a/regression/verilog/part-select/indexed-part-select2.desc b/regression/verilog/part-select/indexed-part-select2.desc new file mode 100644 index 000000000..c0288280e --- /dev/null +++ b/regression/verilog/part-select/indexed-part-select2.desc @@ -0,0 +1,8 @@ +CORE +indexed-part-select2.sv + +^file .* line 4: expected constant expression, but got `main\.width'$ +^EXIT=2$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/verilog/part-select/indexed-part-select2.sv b/regression/verilog/part-select/indexed-part-select2.sv new file mode 100644 index 000000000..aad5c9c74 --- /dev/null +++ b/regression/verilog/part-select/indexed-part-select2.sv @@ -0,0 +1,6 @@ +module main(input [7:0] in, input [2:0] width); + + // The width of an indexed part-select must be a constant + wire [7:0] out = in[0 +: width]; + +endmodule diff --git a/regression/verilog/part-select/indexed-part-select3.desc b/regression/verilog/part-select/indexed-part-select3.desc new file mode 100644 index 000000000..021729201 --- /dev/null +++ b/regression/verilog/part-select/indexed-part-select3.desc @@ -0,0 +1,8 @@ +CORE +indexed-part-select3.sv +--bound 0 +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/verilog/part-select/indexed-part-select3.sv b/regression/verilog/part-select/indexed-part-select3.sv new file mode 100644 index 000000000..f9cdfde8f --- /dev/null +++ b/regression/verilog/part-select/indexed-part-select3.sv @@ -0,0 +1,9 @@ +module main(input [7:0] in, input [2:0] where); + + // The base index of an indexed part-select + // does not need to be constant. + wire out = in[where +: 1]; + + p0: assert property (out == in[where]); + +endmodule diff --git a/regression/verilog/part-select/part-select-of-real.desc b/regression/verilog/part-select/part-select-of-real.desc new file mode 100644 index 000000000..b297c869a --- /dev/null +++ b/regression/verilog/part-select/part-select-of-real.desc @@ -0,0 +1,8 @@ +CORE +part-select-of-real.sv + +^file .* line 5: real not allowed in part select$ +^EXIT=2$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/verilog/part-select/part-select-of-real.sv b/regression/verilog/part-select/part-select-of-real.sv new file mode 100644 index 000000000..eacbf72d7 --- /dev/null +++ b/regression/verilog/part-select/part-select-of-real.sv @@ -0,0 +1,7 @@ +module main; + + // 1800-2017 6.12.1 + real some_real; + wire [7:0] x = some_real[7:0]; + +endmodule diff --git a/regression/verilog/part-select/real-index.desc b/regression/verilog/part-select/real-index.desc new file mode 100644 index 000000000..14a20715c --- /dev/null +++ b/regression/verilog/part-select/real-index.desc @@ -0,0 +1,8 @@ +CORE +real-index.sv + +^file .* line 5: real number index is not allowed$ +^EXIT=2$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/verilog/part-select/real-index.sv b/regression/verilog/part-select/real-index.sv new file mode 100644 index 000000000..a27596e3a --- /dev/null +++ b/regression/verilog/part-select/real-index.sv @@ -0,0 +1,7 @@ +module main; + + // 1800-2017 6.12.1 + reg [7:0] vector; + wire x = vector[real'(1.5)]; + +endmodule diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h index 7ca642e29..d5d6d0119 100644 --- a/src/hw_cbmc_irep_ids.h +++ b/src/hw_cbmc_irep_ids.h @@ -32,9 +32,9 @@ IREP_ID_TWO(C_little_endian, #little_endian) IREP_ID_ONE(ports) IREP_ID_ONE(inst) IREP_ID_ONE(Verilog) -IREP_ID_ONE(part_select) -IREP_ID_ONE(indexed_part_select_plus) -IREP_ID_ONE(indexed_part_select_minus) +IREP_ID_ONE(verilog_non_indexed_part_select) +IREP_ID_ONE(verilog_indexed_part_select_plus) +IREP_ID_ONE(verilog_indexed_part_select_minus) IREP_ID_ONE(chandle) IREP_ID_ONE(event) IREP_ID_ONE(reg) diff --git a/src/verilog/parser.y b/src/verilog/parser.y index 66b19d97b..60529a7d4 100644 --- a/src/verilog/parser.y +++ b/src/verilog/parser.y @@ -148,47 +148,6 @@ static void extractbit(YYSTYPE &expr, YYSTYPE &identifier, YYSTYPE &part) /*******************************************************************\ -Function: extractbits - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -static void extractbits(YYSTYPE &expr, YYSTYPE &identifier, YYSTYPE &range) -{ - init(expr, ID_extractbits); - mto(expr, identifier); - - if(stack_expr(range).id()==ID_part_select) - { - auto &part_select = to_binary_expr(stack_expr(range)); - stack_expr(expr).add_to_operands(std::move(part_select.op0())); - stack_expr(expr).add_to_operands(std::move(part_select.op1())); - } - else if(stack_expr(range).id()==ID_indexed_part_select_plus) - { - auto &part_select = to_binary_expr(stack_expr(range)); - exprt offset=minus_exprt(part_select.op1(), from_integer(1, integer_typet{})); - stack_expr(expr).add_to_operands(part_select.op0()); - stack_expr(expr).add_to_operands(plus_exprt(part_select.op0(), offset)); - } - else if(stack_expr(range).id()==ID_indexed_part_select_minus) - { - auto &part_select = to_binary_expr(stack_expr(range)); - exprt offset=minus_exprt(from_integer(1, integer_typet{}), part_select.op1()); - stack_expr(expr).add_to_operands(part_select.op0()); - stack_expr(expr).add_to_operands(plus_exprt(part_select.op0(), offset)); - } - else - PRECONDITION(false); -} - -/*******************************************************************\ - Function: add_as_subtype Inputs: @@ -1145,7 +1104,7 @@ bit_select: part_select: '[' const_expression TOK_COLON const_expression ']' - { init($$, ID_part_select); mto($$, $2); mto($$, $4); } + { init($$, ID_verilog_non_indexed_part_select); mto($$, $2); mto($$, $4); } ; // System Verilog standard 1800-2017 @@ -3122,14 +3081,14 @@ inc_or_dec_expression: constant_range: const_expression TOK_COLON const_expression - { init($$, ID_part_select); mto($$, $1); mto($$, $3); } + { init($$, ID_verilog_non_indexed_part_select); mto($$, $1); mto($$, $3); } ; indexed_range: expression TOK_PLUSCOLON constant_expression - { init($$, ID_indexed_part_select_plus); mto($$, $1); mto($$, $3); } + { init($$, ID_verilog_indexed_part_select_plus); mto($$, $1); mto($$, $3); } | expression TOK_MINUSCOLON constant_expression - { init($$, ID_indexed_part_select_minus); mto($$, $1); mto($$, $3); } + { init($$, ID_verilog_indexed_part_select_minus); mto($$, $1); mto($$, $3); } ; part_select_range: @@ -3161,7 +3120,13 @@ primary_literal: hierarchical_identifier_select: hierarchical_identifier_bit_select_brace | hierarchical_identifier_bit_select_brace '[' part_select_range ']' - { extractbits($$, $1, $3); } + { // part_select_range has two operands. + // We form a new expression with three operands from it. + auto &part_select = to_binary_expr(stack_expr($3)); + stack_expr($3).operands() = + { stack_expr($1), part_select.op0(), part_select.op1() }; + $$ = $3; + } ; hierarchical_identifier_bit_select_brace: diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp index d9e4ac1b8..325c62206 100644 --- a/src/verilog/verilog_typecheck_expr.cpp +++ b/src/verilog/verilog_typecheck_expr.cpp @@ -1952,13 +1952,24 @@ Function: verilog_typecheck_exprt::convert_extractbit_expr exprt verilog_typecheck_exprt::convert_extractbit_expr(extractbit_exprt expr) { exprt &op0 = expr.op0(); - convert_expr(op0); + if(op0.type().id() == ID_verilog_real) + { + throw errort().with_location(op0.source_location()) + << "bit-select of real is not allowed"; + } + if(op0.type().id()==ID_array) { exprt &op1 = to_extractbit_expr(expr).index(); convert_expr(op1); + if(op1.type().id() == ID_verilog_real) + { + throw errort().with_location(op1.source_location()) + << "real number index is not allowed"; + } + typet _index_type = index_type(to_array_type(op0.type())); if(_index_type!=op1.type()) @@ -1982,7 +1993,7 @@ exprt verilog_typecheck_exprt::convert_extractbit_expr(extractbit_exprt expr) mp_integer op1; - if(is_constant_expression(to_extractbit_expr(expr).op1(), op1)) + if(is_constant_expression(expr.op1(), op1)) { // 1800-2017 sec 11.5.1: out-of-bounds bit-select is // x for 4-state and 0 for 2-state values. @@ -1994,7 +2005,12 @@ exprt verilog_typecheck_exprt::convert_extractbit_expr(extractbit_exprt expr) } else { - convert_expr(to_extractbit_expr(expr).op1()); + convert_expr(expr.op1()); + if(expr.op1().type().id() == ID_verilog_real) + { + throw errort().with_location(expr.op1().source_location()) + << "real number index is not allowed"; + } } expr.type()=bool_typet(); @@ -2301,21 +2317,28 @@ Function: verilog_typecheck_exprt::convert_trinary_expr exprt verilog_typecheck_exprt::convert_trinary_expr(ternary_exprt expr) { - if(expr.id()==ID_extractbits) + if(expr.id() == ID_verilog_non_indexed_part_select) { - exprt &op0=expr.op0(); - + exprt &op0 = expr.op0(); convert_expr(op0); if(op0.type().id()==ID_array) { throw errort().with_location(op0.source_location()) - << "array type not allowed in extraction"; + << "array type not allowed in part select"; + } + + if(op0.type().id() == ID_verilog_real) + { + throw errort().with_location(op0.source_location()) + << "real not allowed in part select"; } - mp_integer width = get_width(op0.type()); - mp_integer offset = atoi(op0.type().get(ID_C_offset).c_str()); + mp_integer op0_width = get_width(op0.type()); + mp_integer op0_offset = string2integer(op0.type().get_string(ID_C_offset)); + // In non-indexed part-select expressions, both + // indices must be constants (1800-2017 11.5.1). mp_integer op1 = convert_integer_constant_expression(expr.op1()); mp_integer op2 = convert_integer_constant_expression(expr.op2()); @@ -2326,9 +2349,9 @@ exprt verilog_typecheck_exprt::convert_trinary_expr(ternary_exprt expr) // x for 4-state and 0 for 2-state values. We // achieve that by padding the operand from either end, // or both. - if(op2 < offset) + if(op2 < op0_offset) { - auto padding_width = offset - op2; + auto padding_width = op0_offset - op2; auto padding = from_integer( 0, unsignedbv_typet{numeric_cast_v(padding_width)}); auto new_type = unsignedbv_typet{ @@ -2338,9 +2361,9 @@ exprt verilog_typecheck_exprt::convert_trinary_expr(ternary_exprt expr) op1 += padding_width; } - if(op1 >= width + offset) + if(op1 >= op0_width + op0_offset) { - auto padding_width = op1 - (width + offset) + 1; + auto padding_width = op1 - (op0_width + op0_offset) + 1; auto padding = from_integer( 0, unsignedbv_typet{numeric_cast_v(padding_width)}); auto new_type = unsignedbv_typet{ @@ -2353,15 +2376,99 @@ exprt verilog_typecheck_exprt::convert_trinary_expr(ternary_exprt expr) auto expr_type = unsignedbv_typet{numeric_cast_v(op1 - op2 + 1)}; - op2 -= offset; - op1 -= offset; + op2 -= op0_offset; + op1 -= op0_offset; - expr.op1() = from_integer(op1, natural_typet()); - expr.op2() = from_integer(op2, natural_typet()); + // Construct the extractbits expression + expr.id(ID_extractbits); + expr.op1() = from_integer(op1, integer_typet()); + expr.op2() = from_integer(op2, integer_typet()); expr.type() = expr_type; return std::move(expr); } + else if( + expr.id() == ID_verilog_indexed_part_select_plus || + expr.id() == ID_verilog_indexed_part_select_minus) + { + exprt &op0 = expr.op0(); + convert_expr(op0); + + if(op0.type().id() == ID_array) + { + throw errort().with_location(op0.source_location()) + << "array type not allowed in part select"; + } + + if(op0.type().id() == ID_verilog_real) + { + throw errort().with_location(op0.source_location()) + << "real not allowed in part select"; + } + + mp_integer op0_width = get_width(op0.type()); + mp_integer op0_offset = string2integer(op0.type().get_string(ID_C_offset)); + + // The index need not be a constant. + exprt &op1 = expr.op1(); + convert_expr(op1); + + // The width of the indexed part select must be an + // elaboration-time constant. + mp_integer op2 = convert_integer_constant_expression(expr.op2()); + + // The width must be positive. 1800-2017 11.5.1 + if(op2 < 0) + { + throw errort().with_location(expr.op2().source_location()) + << "width of indexed part select must be positive"; + } + + // Part-select expressions are unsigned, even if the + // entire expression is selected! + auto expr_type = unsignedbv_typet{numeric_cast_v(op2)}; + + mp_integer op1_int; + if(is_constant_expression(op1, op1_int)) + { + // Construct the extractbits expression + mp_integer bottom, top; + + if(expr.id() == ID_verilog_indexed_part_select_plus) + { + bottom = op1_int - op0_offset; + top = bottom + op2; + } + else // ID_verilog_indexed_part_select_minus + { + top = op1_int - op0_offset; + bottom = bottom - op2; + } + + return extractbits_exprt{ + std::move(op0), + 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 op1_adjusted = + minus_exprt{op1, from_integer(op0_offset, op1.type())}; + + auto op0_shifted = lshr_exprt(op0, op1_adjusted); + + return extractbits_exprt{ + std::move(op0_shifted), + from_integer(op2 - 1, integer_typet{}), + from_integer(0, integer_typet{}), + std::move(expr_type)} + .with_source_location(expr); + } + } else if(expr.id()==ID_if) { convert_expr(expr.op0());