Skip to content

Commit 80476cc

Browse files
tautschnigtautschnig
authored
Merge pull request #421 from diffblue/indexed-part-select
Verilog: indexed part select expressions
2 parents fbfde77 + 8b19daf commit 80476cc

15 files changed

+217
-70
lines changed

‎regression/verilog/part-select/index-of-real.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
index-of-real.sv
3+
4+
^file .* line 5: bit-select of real is not allowed$
5+
^EXIT=2$
6+
^SIGNAL=0$
7+
--
8+
^warning: ignoring

‎regression/verilog/part-select/index-of-real.sv

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
module main;
2+
3+
// 1800-2017 6.12.1
4+
real some_real;
5+
wire x = some_real[0];
6+
7+
endmodule

‎regression/verilog/indexed-part-select1/test.desc renamed to ‎regression/verilog/part-select/indexed-part-select1.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE broken-smt-backend
2-
main.sv
3-
--bound 1
2+
indexed-part-select1.sv
3+
--bound 0
44
^EXIT=0$
55
^SIGNAL=0$
66
--

‎regression/verilog/indexed-part-select1/main.sv renamed to ‎regression/verilog/part-select/indexed-part-select1.sv

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,6 @@ module main(in);
99
out[16 +: 16]=0;
1010
end
1111

12-
always assert property1:
13-
{ in, { 8 { 1'b0 }} } == out;
12+
p1: assert property ({ in, { 8 { 1'b0 }} } == out);
1413

1514
endmodule

‎regression/verilog/part-select/indexed-part-select2.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
indexed-part-select2.sv
3+
4+
^file .* line 4: expected constant expression, but got `main\.width'$
5+
^EXIT=2$
6+
^SIGNAL=0$
7+
--
8+
^warning: ignoring

‎regression/verilog/part-select/indexed-part-select2.sv

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
module main(input [7:0] in, input [2:0] width);
2+
3+
// The width of an indexed part-select must be a constant
4+
wire [7:0] out = in[0 +: width];
5+
6+
endmodule

‎regression/verilog/part-select/indexed-part-select3.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
indexed-part-select3.sv
3+
--bound 0
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
--
7+
^warning: ignoring
8+
--

‎regression/verilog/part-select/indexed-part-select3.sv

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
module main(input [7:0] in, input [2:0] where);
2+
3+
// The base index of an indexed part-select
4+
// does not need to be constant.
5+
wire out = in[where +: 1];
6+
7+
p0: assert property (out == in[where]);
8+
9+
endmodule

‎regression/verilog/part-select/part-select-of-real.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
part-select-of-real.sv
3+
4+
^file .* line 5: real not allowed in part select$
5+
^EXIT=2$
6+
^SIGNAL=0$
7+
--
8+
^warning: ignoring

‎regression/verilog/part-select/part-select-of-real.sv

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
module main;
2+
3+
// 1800-2017 6.12.1
4+
real some_real;
5+
wire [7:0] x = some_real[7:0];
6+
7+
endmodule

‎regression/verilog/part-select/real-index.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
real-index.sv
3+
4+
^file .* line 5: real number index is not allowed$
5+
^EXIT=2$
6+
^SIGNAL=0$
7+
--
8+
^warning: ignoring

‎regression/verilog/part-select/real-index.sv

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
module main;
2+
3+
// 1800-2017 6.12.1
4+
reg [7:0] vector;
5+
wire x = vector[real'(1.5)];
6+
7+
endmodule

‎src/hw_cbmc_irep_ids.h

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -32,9 +32,9 @@ IREP_ID_TWO(C_little_endian, #little_endian)
3232
IREP_ID_ONE(ports)
3333
IREP_ID_ONE(inst)
3434
IREP_ID_ONE(Verilog)
35-
IREP_ID_ONE(part_select)
36-
IREP_ID_ONE(indexed_part_select_plus)
37-
IREP_ID_ONE(indexed_part_select_minus)
35+
IREP_ID_ONE(verilog_non_indexed_part_select)
36+
IREP_ID_ONE(verilog_indexed_part_select_plus)
37+
IREP_ID_ONE(verilog_indexed_part_select_minus)
3838
IREP_ID_ONE(chandle)
3939
IREP_ID_ONE(event)
4040
IREP_ID_ONE(reg)

‎src/verilog/parser.y

Lines changed: 11 additions & 46 deletions
Original file line numberDiff line numberDiff line change
@@ -148,47 +148,6 @@ static void extractbit(YYSTYPE &expr, YYSTYPE &identifier, YYSTYPE &part)
148148

149149
/*******************************************************************\
150150
151-
Function: extractbits
152-
153-
Inputs:
154-
155-
Outputs:
156-
157-
Purpose:
158-
159-
\*******************************************************************/
160-
161-
static void extractbits(YYSTYPE &expr, YYSTYPE &identifier, YYSTYPE &range)
162-
{
163-
init(expr, ID_extractbits);
164-
mto(expr, identifier);
165-
166-
if(stack_expr(range).id()==ID_part_select)
167-
{
168-
auto &part_select = to_binary_expr(stack_expr(range));
169-
stack_expr(expr).add_to_operands(std::move(part_select.op0()));
170-
stack_expr(expr).add_to_operands(std::move(part_select.op1()));
171-
}
172-
else if(stack_expr(range).id()==ID_indexed_part_select_plus)
173-
{
174-
auto &part_select = to_binary_expr(stack_expr(range));
175-
exprt offset=minus_exprt(part_select.op1(), from_integer(1, integer_typet{}));
176-
stack_expr(expr).add_to_operands(part_select.op0());
177-
stack_expr(expr).add_to_operands(plus_exprt(part_select.op0(), offset));
178-
}
179-
else if(stack_expr(range).id()==ID_indexed_part_select_minus)
180-
{
181-
auto &part_select = to_binary_expr(stack_expr(range));
182-
exprt offset=minus_exprt(from_integer(1, integer_typet{}), part_select.op1());
183-
stack_expr(expr).add_to_operands(part_select.op0());
184-
stack_expr(expr).add_to_operands(plus_exprt(part_select.op0(), offset));
185-
}
186-
else
187-
PRECONDITION(false);
188-
}
189-
190-
/*******************************************************************\
191-
192151
Function: add_as_subtype
193152
194153
Inputs:
@@ -1145,7 +1104,7 @@ bit_select:
11451104

11461105
part_select:
11471106
'[' const_expression TOK_COLON const_expression ']'
1148-
{ init($$, ID_part_select); mto($$, $2); mto($$, $4); }
1107+
{ init($$, ID_verilog_non_indexed_part_select); mto($$, $2); mto($$, $4); }
11491108
;
11501109

11511110
// System Verilog standard 1800-2017
@@ -3122,14 +3081,14 @@ inc_or_dec_expression:
31223081

31233082
constant_range:
31243083
const_expression TOK_COLON const_expression
3125-
{ init($$, ID_part_select); mto($$, $1); mto($$, $3); }
3084+
{ init($$, ID_verilog_non_indexed_part_select); mto($$, $1); mto($$, $3); }
31263085
;
31273086

31283087
indexed_range:
31293088
expression TOK_PLUSCOLON constant_expression
3130-
{ init($$, ID_indexed_part_select_plus); mto($$, $1); mto($$, $3); }
3089+
{ init($$, ID_verilog_indexed_part_select_plus); mto($$, $1); mto($$, $3); }
31313090
| expression TOK_MINUSCOLON constant_expression
3132-
{ init($$, ID_indexed_part_select_minus); mto($$, $1); mto($$, $3); }
3091+
{ init($$, ID_verilog_indexed_part_select_minus); mto($$, $1); mto($$, $3); }
31333092
;
31343093

31353094
part_select_range:
@@ -3161,7 +3120,13 @@ primary_literal:
31613120
hierarchical_identifier_select:
31623121
hierarchical_identifier_bit_select_brace
31633122
| hierarchical_identifier_bit_select_brace '[' part_select_range ']'
3164-
{ extractbits($$, $1, $3); }
3123+
{ // part_select_range has two operands.
3124+
// We form a new expression with three operands from it.
3125+
auto &part_select = to_binary_expr(stack_expr($3));
3126+
stack_expr($3).operands() =
3127+
{ stack_expr($1), part_select.op0(), part_select.op1() };
3128+
$$ = $3;
3129+
}
31653130
;
31663131

31673132
hierarchical_identifier_bit_select_brace:

0 commit comments

Comments
 (0)