Skip to content

Commit 578d1af

Browse files
kroeningkroening
authored
Merge pull request #968 from diffblue/verilog-package-dep
SystemVerilog: discover package dependencies in expressions and types
2 parents 5d9c77b + 6e562d3 commit 578d1af

File tree

9 files changed

+201
-10
lines changed

9 files changed

+201
-10
lines changed

‎regression/verilog/packages/package2.sv

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6,8 +6,6 @@ endpackage
66

77
module main;
88

9-
import moo::*;
10-
119
parameter Q = moo::P;
1210

1311
assert final (Q == 123);

‎regression/verilog/packages/package_typedef1.sv

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6,8 +6,6 @@ endpackage
66

77
module main;
88

9-
import moo::*;
10-
119
moo::my_type some_var;
1210

1311
assert final ($typename(some_var) == "bit signed[7:0]");

‎src/verilog/verilog_elaborate_type.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -160,7 +160,7 @@ Function: verilog_typecheck_exprt::elaborate_package_scope_typedef
160160
\*******************************************************************/
161161

162162
typet verilog_typecheck_exprt::elaborate_package_scope_typedef(
163-
const type_with_subtypest &src)
163+
const verilog_package_scope_typet &src)
164164
{
165165
auto location = src.source_location();
166166

@@ -445,7 +445,7 @@ typet verilog_typecheck_exprt::elaborate_type(const typet &src)
445445
else if(src.id() == ID_verilog_package_scope)
446446
{
447447
// package::typedef
448-
return elaborate_package_scope_typedef(to_type_with_subtypes(src));
448+
return elaborate_package_scope_typedef(to_verilog_package_scope_type(src));
449449
}
450450
else
451451
{

‎src/verilog/verilog_expr.cpp

Lines changed: 108 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
1111
#include <util/arith_tools.h>
1212
#include <util/bitvector_expr.h>
1313
#include <util/bitvector_types.h>
14+
#include <util/expr_iterator.h>
1415
#include <util/mathematical_types.h>
1516
#include <util/prefix.h>
1617

@@ -81,6 +82,33 @@ void verilog_module_sourcet::show(std::ostream &out) const
8182
out << '\n';
8283
}
8384

85+
static void
86+
dependencies_rec(const verilog_module_itemt &, std::vector<irep_idt> &);
87+
88+
static void dependencies_rec(const exprt &expr, std::vector<irep_idt> &dest)
89+
{
90+
for(const_depth_iteratort it = expr.depth_cbegin(); it != expr.depth_cend();
91+
++it)
92+
{
93+
if(it->id() == ID_verilog_package_scope)
94+
{
95+
auto &package_scope_expr = to_verilog_package_scope_expr(*it);
96+
dest.push_back(
97+
verilog_package_identifier(package_scope_expr.package_base_name()));
98+
}
99+
}
100+
}
101+
102+
static void dependencies_rec(const typet &type, std::vector<irep_idt> &dest)
103+
{
104+
if(type.id() == ID_verilog_package_scope)
105+
{
106+
auto &package_scope_type = to_verilog_package_scope_type(type);
107+
dest.push_back(
108+
verilog_package_identifier(package_scope_type.package_base_name()));
109+
}
110+
}
111+
84112
static void dependencies_rec(
85113
const verilog_module_itemt &module_item,
86114
std::vector<irep_idt> &dest)
@@ -114,6 +142,86 @@ static void dependencies_rec(
114142
verilog_package_identifier(import_item.get(ID_verilog_package)));
115143
}
116144
}
145+
else if(module_item.id() == ID_parameter_decl)
146+
{
147+
auto &parameter_decl = to_verilog_parameter_decl(module_item);
148+
for(auto &decl : parameter_decl.declarations())
149+
{
150+
dependencies_rec(decl.type(), dest);
151+
dependencies_rec(decl.value(), dest);
152+
}
153+
}
154+
else if(module_item.id() == ID_local_parameter_decl)
155+
{
156+
auto &localparam_decl = to_verilog_local_parameter_decl(module_item);
157+
for(auto &decl : localparam_decl.declarations())
158+
{
159+
dependencies_rec(decl.type(), dest);
160+
dependencies_rec(decl.value(), dest);
161+
}
162+
}
163+
else if(module_item.id() == ID_decl)
164+
{
165+
auto &decl = to_verilog_decl(module_item);
166+
dependencies_rec(decl.type(), dest);
167+
for(auto &declarator : decl.declarators())
168+
{
169+
dependencies_rec(declarator.type(), dest);
170+
dependencies_rec(declarator.value(), dest);
171+
}
172+
}
173+
else if(
174+
module_item.id() == ID_verilog_always ||
175+
module_item.id() == ID_verilog_always_comb ||
176+
module_item.id() == ID_verilog_always_ff ||
177+
module_item.id() == ID_verilog_always_latch)
178+
{
179+
dependencies_rec(to_verilog_always_base(module_item).statement(), dest);
180+
}
181+
else if(module_item.id() == ID_initial)
182+
{
183+
dependencies_rec(to_verilog_initial(module_item).statement(), dest);
184+
}
185+
else if(module_item.id() == ID_inst)
186+
{
187+
}
188+
else if(module_item.id() == ID_inst_builtin)
189+
{
190+
}
191+
else if(module_item.id() == ID_continuous_assign)
192+
{
193+
}
194+
else if(
195+
module_item.id() == ID_verilog_assert_property ||
196+
module_item.id() == ID_verilog_assume_property ||
197+
module_item.id() == ID_verilog_restrict_property ||
198+
module_item.id() == ID_verilog_cover_property)
199+
{
200+
}
201+
else if(module_item.id() == ID_verilog_assertion_item)
202+
{
203+
}
204+
else if(module_item.id() == ID_parameter_override)
205+
{
206+
}
207+
else if(module_item.id() == ID_verilog_final)
208+
{
209+
}
210+
else if(module_item.id() == ID_verilog_let)
211+
{
212+
// to_verilog_let(module_item));
213+
}
214+
else if(module_item.id() == ID_verilog_smv_assume)
215+
{
216+
}
217+
else if(module_item.id() == ID_verilog_property_declaration)
218+
{
219+
// to_verilog_property_declaration(module_item)
220+
}
221+
else if(module_item.id() == ID_verilog_sequence_declaration)
222+
{
223+
// to_verilog_sequence_declaration(module_item)
224+
}
117225
}
118226

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

‎src/verilog/verilog_expr.h

Lines changed: 35 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3011,4 +3011,39 @@ inline verilog_value_range_exprt &to_verilog_value_range_expr(exprt &expr)
30113011
return static_cast<verilog_value_range_exprt &>(expr);
30123012
}
30133013

3014+
/// package::identifier
3015+
class verilog_package_scope_exprt : public binary_exprt
3016+
{
3017+
public:
3018+
irep_idt package_base_name() const
3019+
{
3020+
return op0().id();
3021+
}
3022+
3023+
const exprt &identifier() const
3024+
{
3025+
return op1();
3026+
}
3027+
};
3028+
3029+
/// Cast a generic typet to a \ref verilog_package_scope_exprt. This is an unchecked
3030+
/// conversion. \a type must be known to be \ref verilog_package_scope_exprt.
3031+
/// \param type: Source type
3032+
/// \return Object of type \ref verilog_package_scope_exprt
3033+
inline const verilog_package_scope_exprt &
3034+
to_verilog_package_scope_expr(const exprt &expr)
3035+
{
3036+
PRECONDITION(expr.id() == ID_verilog_package_scope);
3037+
verilog_package_scope_exprt::check(expr);
3038+
return static_cast<const verilog_package_scope_exprt &>(expr);
3039+
}
3040+
3041+
/// \copydoc to_verilog_exprdef_expr(const exprt &)
3042+
inline verilog_package_scope_exprt &to_verilog_package_scope_expr(exprt &expr)
3043+
{
3044+
PRECONDITION(expr.id() == ID_verilog_package_scope);
3045+
verilog_package_scope_exprt::check(expr);
3046+
return static_cast<verilog_package_scope_exprt &>(expr);
3047+
}
3048+
30143049
#endif

‎src/verilog/verilog_typecheck_expr.cpp

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -2829,13 +2829,14 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr)
28292829
else if(expr.id() == ID_verilog_package_scope)
28302830
{
28312831
auto location = expr.source_location();
2832+
auto &package_scope = to_verilog_package_scope_expr(expr);
28322833

2833-
if(expr.rhs().id() != ID_symbol)
2834+
if(package_scope.identifier().id() != ID_symbol)
28342835
throw errort().with_location(location)
28352836
<< expr.id() << " expects symbol on the rhs";
28362837

2837-
auto package_base = expr.lhs().id();
2838-
auto rhs_base = expr.rhs().get(ID_base_name);
2838+
auto package_base = package_scope.package_base_name();
2839+
auto rhs_base = package_scope.identifier().get(ID_base_name);
28392840

28402841
// stitch together
28412842
irep_idt full_identifier =

‎src/verilog/verilog_typecheck_expr.h

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,7 @@ Author: Daniel Kroening, [email protected]
2020

2121
class function_call_exprt;
2222
class power_exprt;
23+
class verilog_package_scope_typet;
2324

2425
class verilog_typecheck_exprt:public verilog_typecheck_baset
2526
{
@@ -66,7 +67,7 @@ class verilog_typecheck_exprt:public verilog_typecheck_baset
6667
void propagate_type(exprt &expr, const typet &type);
6768

6869
typet elaborate_type(const typet &);
69-
typet elaborate_package_scope_typedef(const type_with_subtypest &);
70+
typet elaborate_package_scope_typedef(const verilog_package_scope_typet &);
7071
typet convert_enum(const class verilog_enum_typet &);
7172
array_typet convert_unpacked_array_type(const type_with_subtypet &);
7273
typet convert_packed_array_type(const type_with_subtypet &);

‎src/verilog/verilog_types.cpp

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -19,3 +19,15 @@ constant_exprt verilog_event_typet::null_expr() const
1919
{
2020
return encoding().all_zeros_expr();
2121
}
22+
23+
void verilog_package_scope_typet::check(
24+
const typet &type,
25+
const validation_modet vm)
26+
{
27+
PRECONDITION(type.id() == ID_verilog_package_scope);
28+
type_with_subtypest::check(type);
29+
DATA_CHECK(
30+
vm,
31+
to_type_with_subtypes(type).subtypes().size() == 2,
32+
"verilog_package_scope type must have two subtypes");
33+
}

‎src/verilog/verilog_types.h

Lines changed: 38 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -656,4 +656,42 @@ inline verilog_typedef_typet &to_verilog_typedef_type(typet &type)
656656
return static_cast<verilog_typedef_typet &>(type);
657657
}
658658

659+
/// package::type
660+
class verilog_package_scope_typet : public type_with_subtypest
661+
{
662+
public:
663+
irep_idt package_base_name() const
664+
{
665+
return subtypes()[0].id();
666+
}
667+
668+
const typet &typedef_type() const
669+
{
670+
return subtypes()[1];
671+
}
672+
673+
static void
674+
check(const typet &, const validation_modet = validation_modet::INVARIANT);
675+
};
676+
677+
/// Cast a generic typet to a \ref verilog_package_scope_typet. This is an unchecked
678+
/// conversion. \a type must be known to be \ref verilog_package_scope_typet.
679+
/// \param type: Source type
680+
/// \return Object of type \ref verilog_package_scope_typet
681+
inline const verilog_package_scope_typet &
682+
to_verilog_package_scope_type(const typet &type)
683+
{
684+
PRECONDITION(type.id() == ID_verilog_package_scope);
685+
verilog_package_scope_typet::check(type);
686+
return static_cast<const verilog_package_scope_typet &>(type);
687+
}
688+
689+
/// \copydoc to_verilog_typedef_type(const typet &)
690+
inline verilog_package_scope_typet &to_verilog_package_scope_type(typet &type)
691+
{
692+
PRECONDITION(type.id() == ID_verilog_package_scope);
693+
verilog_package_scope_typet::check(type);
694+
return static_cast<verilog_package_scope_typet &>(type);
695+
}
696+
659697
#endif

0 commit comments

Comments
 (0)