Skip to content

Commit 3a3a576

Browse files
committed
SystemVerilog: package scope operator
This adds the SystemVerilog package scope operator ::.
1 parent 129c081 commit 3a3a576

14 files changed

+119
-53
lines changed

CHANGELOG

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@
99
* SystemVerilog: $bitstoreal/$bitstoshortreal, $realtobits/$shortrealtobits
1010
* SystemVerilog: $itor, $rtoi
1111
* SystemVerilog: chandle, event
12+
* SystemVerilog: package scope operator
1213

1314
# EBMC 5.4
1415

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
package2.sv
3+
4+
^^\[.*\] always main\.Q == 123: PROVED$
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
--
Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
package moo;
2+
3+
parameter P = 123;
4+
5+
endpackage
6+
7+
module main;
8+
9+
import moo::*;
10+
11+
parameter Q = moo::P;
12+
13+
assert final (Q == 123);
14+
15+
endmodule

src/hw_cbmc_irep_ids.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -250,6 +250,7 @@ IREP_ID_ONE(verilog_class)
250250
IREP_ID_ONE(verilog_module)
251251
IREP_ID_ONE(verilog_package)
252252
IREP_ID_ONE(verilog_package_import)
253+
IREP_ID_ONE(verilog_package_scope)
253254
IREP_ID_ONE(verilog_program)
254255
IREP_ID_ONE(verilog_udp)
255256
IREP_ID_ONE(module_source)

src/verilog/parser.y

Lines changed: 13 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1355,9 +1355,13 @@ package_import_item_brace:
13551355

13561356
package_import_item:
13571357
package_identifier "::" identifier
1358-
{ init($$, ID_verilog_import_item); mto($$, $1); mto($$, $3); }
1358+
{ init($$, ID_verilog_import_item);
1359+
stack_expr($$).set(ID_verilog_package, stack_expr($1).id());
1360+
stack_expr($$).set(ID_identifier, stack_expr($3).id()); }
13591361
| package_identifier "::" "*"
1360-
{ init($$, ID_verilog_import_item); mto($$, $1); }
1362+
{ init($$, ID_verilog_import_item);
1363+
stack_expr($$).set(ID_verilog_package, stack_expr($1).id());
1364+
stack_expr($$).set(ID_identifier, "*"); }
13611365
;
13621366

13631367
genvar_declaration:
@@ -4032,6 +4036,10 @@ part_select_range:
40324036

40334037
primary: primary_literal
40344038
| hierarchical_identifier_select
4039+
| package_scope hierarchical_identifier_select
4040+
{ init($$, ID_verilog_package_scope);
4041+
mto($$, $1);
4042+
mto($$, $2); }
40354043
| concatenation
40364044
| multiple_concatenation
40374045
| function_subroutine_call
@@ -4209,6 +4217,9 @@ net_identifier: identifier;
42094217

42104218
package_identifier: TOK_NON_TYPE_IDENTIFIER;
42114219

4220+
package_scope: package_identifier "::"
4221+
;
4222+
42124223
param_identifier: TOK_NON_TYPE_IDENTIFIER;
42134224

42144225
port_identifier: identifier;

src/verilog/verilog_expr.cpp

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -100,6 +100,14 @@ static void dependencies_rec(
100100
{
101101
dependencies_rec(to_verilog_generate_for(module_item).body(), dest);
102102
}
103+
else if(module_item.id() == ID_verilog_package_import)
104+
{
105+
for(auto &import_item : module_item.get_sub())
106+
{
107+
dest.push_back(
108+
verilog_package_identifier(import_item.get(ID_verilog_package)));
109+
}
110+
}
103111
}
104112

105113
std::vector<irep_idt> verilog_item_containert::dependencies() const

src/verilog/verilog_language.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -132,7 +132,7 @@ void verilog_languaget::dependencies(
132132
std::set<std::string> &dependency_set)
133133
{
134134
verilog_parse_treet::item_mapt::const_iterator it =
135-
parse_tree.item_map.find(id2string(verilog_module_name(module)));
135+
parse_tree.item_map.find(id2string(verilog_item_key(module)));
136136

137137
if(it != parse_tree.item_map.end())
138138
{

src/verilog/verilog_parse_tree.cpp

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -62,8 +62,15 @@ void verilog_parse_treet::modules_provided(
6262
for(auto &item : items)
6363
{
6464
if(item.id() == ID_verilog_module)
65+
{
6566
module_set.insert(id2string(
6667
verilog_module_symbol(to_verilog_module_source(item).base_name())));
68+
}
69+
else if(item.id() == ID_verilog_package)
70+
{
71+
module_set.insert(id2string(verilog_package_identifier(
72+
to_verilog_module_source(item).base_name())));
73+
}
6774
}
6875
}
6976

src/verilog/verilog_parse_tree.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -75,7 +75,7 @@ class verilog_parse_treet
7575

7676
// An index into the items list.
7777
// The key is
78-
// package::name for pagages
78+
// package::name for packages
7979
// name for modules, etc.
8080
// as packages have a separate name space (1800-2017 3.13).
8181
typedef std::

src/verilog/verilog_typecheck.cpp

Lines changed: 12 additions & 36 deletions
Original file line numberDiff line numberDiff line change
@@ -1947,55 +1947,27 @@ Function: verilog_typecheck
19471947
bool verilog_typecheck(
19481948
const verilog_parse_treet &parse_tree,
19491949
symbol_table_baset &symbol_table,
1950-
const std::string &module,
1950+
const irep_idt &module_identifier,
19511951
bool warn_implicit_nets,
19521952
message_handlert &message_handler)
19531953
{
19541954
verilog_parse_treet::item_mapt::const_iterator it =
1955-
parse_tree.item_map.find(id2string(verilog_module_name(module)));
1955+
parse_tree.item_map.find(id2string(verilog_item_key(module_identifier)));
19561956

19571957
if(it == parse_tree.item_map.end())
19581958
{
19591959
messaget message(message_handler);
1960-
message.error() << "module `" << module
1961-
<< "' not found" << messaget::eom;
1960+
message.error() << "module `" << module_identifier << "' not found"
1961+
<< messaget::eom;
19621962
return true;
19631963
}
19641964

1965-
auto &module_source = to_verilog_module_source(*it->second);
1966-
1967-
return verilog_typecheck(
1968-
symbol_table,
1969-
module_source,
1970-
parse_tree.standard,
1971-
warn_implicit_nets,
1972-
message_handler);
1973-
}
1974-
1975-
/*******************************************************************\
1976-
1977-
Function: verilog_typecheck
1978-
1979-
Inputs:
1980-
1981-
Outputs:
1982-
1983-
Purpose:
1984-
1985-
\*******************************************************************/
1986-
1987-
bool verilog_typecheck(
1988-
symbol_table_baset &symbol_table,
1989-
const verilog_module_sourcet &verilog_module_source,
1990-
verilog_standardt standard,
1991-
bool warn_implicit_nets,
1992-
message_handlert &message_handler)
1993-
{
1994-
// create symbol
1965+
auto &verilog_module_source = to_verilog_module_source(*it->second);
19951966

1967+
// create the symbol
19961968
irep_idt base_name = verilog_module_source.base_name();
19971969

1998-
symbolt symbol{verilog_module_symbol(base_name), module_typet{}, ID_Verilog};
1970+
symbolt symbol{module_identifier, module_typet{}, ID_Verilog};
19991971

20001972
symbol.base_name = base_name;
20011973
symbol.pretty_name = base_name;
@@ -2017,7 +1989,11 @@ bool verilog_typecheck(
20171989
}
20181990

20191991
verilog_typecheckt verilog_typecheck(
2020-
standard, warn_implicit_nets, *new_symbol, symbol_table, message_handler);
1992+
parse_tree.standard,
1993+
warn_implicit_nets,
1994+
*new_symbol,
1995+
symbol_table,
1996+
message_handler);
20211997

20221998
return verilog_typecheck.typecheck_main();
20231999
}

0 commit comments

Comments
 (0)