Skip to content

Commit 8dbbbc0

Browse files
kroeningkroening
authored
Merge pull request #412 from diffblue/verilog-array-types
Verilog: distinguish packed and unpacked arrays
2 parents 80476cc + 0844c0b commit 8dbbbc0

File tree

11 files changed

+179
-122
lines changed

11 files changed

+179
-122
lines changed

‎regression/verilog/arrays/packed_real1.desc‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
KNOWNBUG
2+
packed_real1.sv
3+
--module main --bound 0
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
--
7+
--
8+
A packed array of reals must be rejected.

‎regression/verilog/arrays/packed_real1.sv‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
module main;
2+
3+
// Packed arrays can be made of single bit data types
4+
// or other packed types.
5+
typedef real my_real;
6+
my_real [7:0] my_array;
7+
8+
endmodule
9+

‎regression/verilog/arrays/packed_typedef1.desc‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
KNOWNBUG
2+
packed_typedef1.sv
3+
--module main --bound 0
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
--
7+
--
8+
The packed array type must not be dropped.

‎regression/verilog/arrays/packed_typedef1.sv‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
module main;
2+
3+
typedef bit my_bit;
4+
my_bit [7:0] my_vector;
5+
6+
always assert p0: ($bits(my_vector) == 8);
7+
8+
endmodule

‎src/hw_cbmc_irep_ids.h‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -110,9 +110,11 @@ IREP_ID_ONE(wire)
110110
IREP_ID_ONE(uwire)
111111
IREP_ID_ONE(wand)
112112
IREP_ID_ONE(automatic)
113-
IREP_ID_ONE(verilog_enum)
114113
IREP_ID_TWO(C_verilog_type, #verilog_type)
114+
IREP_ID_ONE(verilog_enum)
115+
IREP_ID_ONE(verilog_packed_array)
115116
IREP_ID_ONE(verilog_type_reference)
117+
IREP_ID_ONE(verilog_unpacked_array)
116118
IREP_ID_ONE(enum_names)
117119
IREP_ID_ONE(var)
118120
IREP_ID_ONE(trireg)

‎src/verilog/parser.y‎

Lines changed: 30 additions & 33 deletions
Original file line numberDiff line numberDiff line change
@@ -785,23 +785,29 @@ module_port_input_declaration:
785785
TOK_INPUT net_port_type port_identifier unpacked_dimension_brace
786786
{ init($$, ID_decl);
787787
stack_expr($$).set(ID_class, ID_input);
788-
add_as_subtype(stack_type($4), stack_type($2));
789-
addswap($$, ID_type, $4);
788+
// The net_port_type goes onto the declaration,
789+
// and the unpacked_array_type goes onto the declarator.
790+
addswap($$, ID_type, $2);
791+
addswap($3, ID_type, $4);
790792
mto($$, $3); }
791793
;
792794

793795
module_port_output_declaration:
794796
TOK_OUTPUT net_port_type port_identifier unpacked_dimension_brace
795797
{ init($$, ID_decl);
796798
stack_expr($$).set(ID_class, ID_output);
797-
add_as_subtype(stack_type($4), stack_type($2));
798-
addswap($$, ID_type, $4);
799+
// The data_type goes onto the declaration,
800+
// and the unpacked_array_type goes onto the declarator.
801+
addswap($$, ID_type, $2);
802+
addswap($3, ID_type, $4);
799803
mto($$, $3); }
800804
| TOK_OUTPUT data_type port_identifier unpacked_dimension_brace
801805
{ init($$, ID_decl);
802806
stack_expr($$).set(ID_class, ID_output_register);
803-
add_as_subtype(stack_type($4), stack_type($2));
804-
addswap($$, ID_type, $4);
807+
// The data_type goes onto the declaration,
808+
// and the unpacked_array_type goes onto the declarator.
809+
addswap($$, ID_type, $2);
810+
addswap($3, ID_type, $4);
805811
mto($$, $3); }
806812
;
807813

@@ -1132,12 +1138,7 @@ genvar_declaration:
11321138
;
11331139

11341140
net_declaration:
1135-
net_type drive_strength_opt vectored_scalared_opt data_type_or_implicit delay3_opt list_of_net_names ';'
1136-
{ init($$, ID_decl);
1137-
addswap($$, ID_class, $1);
1138-
addswap($$, ID_type, $4);
1139-
swapop($$, $6); }
1140-
| net_type drive_strength_opt vectored_scalared_opt data_type_or_implicit delay3_opt list_of_net_decl_assignments ';'
1141+
net_type drive_strength_opt vectored_scalared_opt data_type_or_implicit delay3_opt list_of_net_decl_assignments ';'
11411142
{ init($$, ID_decl);
11421143
addswap($$, ID_class, $1);
11431144
addswap($$, ID_type, $4);
@@ -1167,21 +1168,6 @@ vectored_scalared_opt:
11671168
| TOK_SCALARED { init($$, "scalared"); }
11681169
;
11691170

1170-
list_of_net_names:
1171-
net_name
1172-
{ init($$); mto($$, $1); }
1173-
| list_of_net_names ',' net_name
1174-
{ $$=$1; mto($$, $3); }
1175-
;
1176-
1177-
net_name: net_identifier packed_dimension_brace
1178-
{
1179-
$$=$1;
1180-
stack_expr($$).id(ID_declarator);
1181-
addswap($$, ID_type, $2);
1182-
}
1183-
;
1184-
11851171
list_of_net_decl_assignments:
11861172
net_decl_assignment
11871173
{ init($$); mto($$, $1); }
@@ -1244,7 +1230,9 @@ data_type:
12441230
| TOK_VIRTUAL interface_opt interface_identifier
12451231
{ init($$, "virtual_interface"); }
12461232
| /*scope_opt*/ type_identifier packed_dimension_brace
1247-
{ $$ = $1; stack_expr($$).id(ID_typedef_type); }
1233+
{ stack_expr($1).id(ID_typedef_type);
1234+
add_as_subtype(stack_type($2), stack_type($1));
1235+
$$ = $2; }
12481236
// | class_type
12491237
| TOK_EVENT
12501238
{ init($$, ID_event); }
@@ -1659,8 +1647,16 @@ range: part_select;
16591647
// System Verilog standard 1800-2017
16601648
// A.2.4 Declaration assignments
16611649

1662-
net_decl_assignment: net_identifier '=' expression
1663-
{ $$ = $1; stack_expr($$).id(ID_declarator); addswap($$, ID_value, $3); }
1650+
net_decl_assignment:
1651+
net_identifier unpacked_dimension_brace
1652+
{ $$ = $1;
1653+
stack_expr($$).id(ID_declarator);
1654+
addswap($$, ID_type, $2); }
1655+
| net_identifier unpacked_dimension_brace '=' expression
1656+
{ $$ = $1;
1657+
stack_expr($$).id(ID_declarator);
1658+
addswap($$, ID_type, $2);
1659+
addswap($$, ID_value, $4); }
16641660
;
16651661

16661662
variable_decl_assignment:
@@ -1693,7 +1689,7 @@ packed_dimension_opt:
16931689

16941690
packed_dimension:
16951691
'[' const_expression TOK_COLON const_expression ']'
1696-
{ init($$, ID_array);
1692+
{ init($$, ID_verilog_packed_array);
16971693
stack_type($$).add_subtype().make_nil();
16981694
exprt &range=static_cast<exprt &>(stack_type($$).add(ID_range));
16991695
range.add_to_operands(stack_expr($2));
@@ -1703,13 +1699,14 @@ packed_dimension:
17031699

17041700
unpacked_dimension:
17051701
'[' const_expression TOK_COLON const_expression ']'
1706-
{ init($$, ID_array);
1702+
{ init($$, ID_verilog_unpacked_array);
17071703
stack_type($$).add_subtype().make_nil();
17081704
exprt &range=static_cast<exprt &>(stack_type($$).add(ID_range));
17091705
range.add_to_operands(stack_expr($2));
17101706
range.add_to_operands(stack_expr($4)); }
17111707
| '[' expression ']'
1712-
{ init($$, ID_array);
1708+
{ // starts at index 0
1709+
init($$, ID_verilog_unpacked_array);
17131710
stack_type($$).add_subtype().make_nil();
17141711
stack_type($$).set(ID_size, std::move(stack_expr($2)));
17151712
}

‎src/verilog/verilog_elaborate.cpp‎

Lines changed: 29 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,9 @@ void verilog_typecheckt::collect_port_symbols(const verilog_declt &decl)
2424

2525
const irep_idt &base_name = declarator.base_name();
2626
const irep_idt &port_class = decl.get_class();
27+
2728
auto type = convert_type(decl.type());
29+
2830
irep_idt identifier = hierarchical_identifier(base_name);
2931

3032
if(port_class.empty())
@@ -34,7 +36,18 @@ void verilog_typecheckt::collect_port_symbols(const verilog_declt &decl)
3436
else
3537
{
3638
// add the symbol
37-
symbolt new_symbol(identifier, type, mode);
39+
typet final_type;
40+
if(declarator.type().is_nil())
41+
final_type = type;
42+
else if(declarator.type().id() == ID_verilog_unpacked_array)
43+
final_type = unpacked_array_type(declarator.type(), type);
44+
else
45+
{
46+
throw errort().with_location(declarator.source_location())
47+
<< "unexpected type on declarator";
48+
}
49+
50+
symbolt new_symbol(identifier, final_type, mode);
3851

3952
if(port_class == ID_input)
4053
{
@@ -222,8 +235,8 @@ void verilog_typecheckt::collect_symbols(const verilog_declt &decl)
222235

223236
if(declarator.type().is_nil())
224237
symbol.type = type;
225-
else if(declarator.type().id() == ID_array)
226-
symbol.type = array_type(declarator.type(), type);
238+
else if(declarator.type().id() == ID_verilog_unpacked_array)
239+
symbol.type = unpacked_array_type(declarator.type(), type);
227240
else
228241
{
229242
throw errort().with_location(declarator.source_location())
@@ -315,7 +328,15 @@ void verilog_typecheckt::collect_symbols(const verilog_declt &decl)
315328
<< "empty symbol name";
316329
}
317330

318-
symbol.type = type;
331+
if(declarator.type().is_nil())
332+
symbol.type = type;
333+
else if(declarator.type().id() == ID_verilog_unpacked_array)
334+
symbol.type = unpacked_array_type(declarator.type(), type);
335+
else
336+
{
337+
throw errort().with_location(declarator.source_location())
338+
<< "unexpected type on declarator";
339+
}
319340

320341
symbol.name = hierarchical_identifier(symbol.base_name);
321342

@@ -401,8 +422,8 @@ void verilog_typecheckt::collect_symbols(const verilog_declt &decl)
401422

402423
if(declarator.type().is_nil())
403424
symbol.type = type;
404-
else if(declarator.type().id() == ID_array)
405-
symbol.type = array_type(declarator.type(), type);
425+
else if(declarator.type().id() == ID_verilog_unpacked_array)
426+
symbol.type = unpacked_array_type(declarator.type(), type);
406427
else
407428
{
408429
throw errort().with_location(symbol.location)
@@ -468,8 +489,8 @@ void verilog_typecheckt::collect_symbols(const verilog_declt &decl)
468489

469490
if(declarator.type().is_nil())
470491
symbol.type = type;
471-
else if(declarator.type().id() == ID_array)
472-
symbol.type = array_type(declarator.type(), type);
492+
else if(declarator.type().id() == ID_verilog_unpacked_array)
493+
symbol.type = unpacked_array_type(declarator.type(), type);
473494
else
474495
{
475496
throw errort().with_location(symbol.location)

‎src/verilog/verilog_typecheck.cpp‎

Lines changed: 0 additions & 74 deletions
Original file line numberDiff line numberDiff line change
@@ -28,80 +28,6 @@ Author: Daniel Kroening, [email protected]
2828

2929
/*******************************************************************\
3030
31-
Function: verilog_typecheckt::array_type
32-
33-
Inputs:
34-
35-
Outputs:
36-
37-
Purpose:
38-
39-
\*******************************************************************/
40-
41-
array_typet verilog_typecheckt::array_type(
42-
const irept &src,
43-
const typet &element_type)
44-
{
45-
// int whatnot[x:y];
46-
// 'src' is yet to be converted, but 'element_type' is already converted.
47-
PRECONDITION(src.id() == ID_array);
48-
49-
// Unpacked arrays may have a range [x:y],
50-
// or a size [s], equivalent to [0:s-1]
51-
const exprt &range_expr = static_cast<const exprt &>(src.find(ID_range));
52-
const exprt &size_expr = static_cast<const exprt &>(src.find(ID_size));
53-
54-
mp_integer size, offset;
55-
bool little_endian;
56-
57-
if(range_expr.is_not_nil())
58-
{
59-
// these may be negative
60-
mp_integer msb, lsb;
61-
convert_range(range_expr, msb, lsb);
62-
little_endian = (lsb <= msb);
63-
size = (little_endian ? msb - lsb : lsb - msb) + 1;
64-
offset = little_endian ? lsb : msb;
65-
}
66-
else if(size_expr.is_not_nil())
67-
{
68-
little_endian = true;
69-
size = convert_integer_constant_expression(size_expr);
70-
offset = 0;
71-
if(size < 0)
72-
{
73-
throw errort().with_location(size_expr.find_source_location())
74-
<< "array size must be nonnegative";
75-
}
76-
}
77-
else
78-
{
79-
throw errort() << "array must have range or size";
80-
}
81-
82-
const typet src_subtype =
83-
static_cast<const typet &>(src).has_subtype()
84-
? static_cast<const type_with_subtypet &>(src).subtype()
85-
: typet(ID_nil);
86-
87-
typet array_subtype;
88-
89-
// may need to go recursive
90-
if(src_subtype.is_nil())
91-
array_subtype=element_type;
92-
else
93-
array_subtype=array_type(src_subtype, element_type);
94-
95-
const exprt final_size_expr = from_integer(size, integer_typet());
96-
array_typet result(array_subtype, final_size_expr);
97-
result.set(ID_offset, from_integer(offset, integer_typet()));
98-
result.set(ID_C_little_endian, little_endian);
99-
100-
return result;
101-
}
102-
103-
/*******************************************************************\
104-
10531
Function: verilog_typecheckt::typecheck_port_connection
10632
10733
Inputs:

‎src/verilog/verilog_typecheck.h‎

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -125,10 +125,6 @@ class verilog_typecheckt:
125125
void interface_generate_block(const class verilog_generate_blockt &);
126126
void interface_statement(const class verilog_statementt &);
127127

128-
array_typet array_type(
129-
const irept &src,
130-
const typet &element_type);
131-
132128
// type checking
133129

134130
typedef enum { A_CONTINUOUS, A_BLOCKING, A_NON_BLOCKING } vassignt;

‎src/verilog/verilog_typecheck_expr.h‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -64,6 +64,7 @@ class verilog_typecheck_exprt:public verilog_typecheck_baset
6464

6565
typet convert_type(const typet &);
6666
typet convert_enum(const class verilog_enum_typet &);
67+
array_typet unpacked_array_type(const typet &src, const typet &element_type);
6768

6869
void convert_range(
6970
const exprt &range,

0 commit comments

Comments
 (0)