Skip to content

Commit c9b9f62

Browse files
tautschnigtautschnig
authored
Merge pull request #1262 from diffblue/verilog_function_declt
Verilog: split variable and function/task declaration classes
2 parents 15f8eea + 818bed5 commit c9b9f62

File tree

10 files changed

+161
-90
lines changed

10 files changed

+161
-90
lines changed

‎src/hw_cbmc_irep_ids.h‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -188,6 +188,8 @@ IREP_ID_ONE(verilog_blocking_assign_lshr)
188188
IREP_ID_ONE(verilog_blocking_assign_lshl)
189189
IREP_ID_ONE(verilog_blocking_assign_ashr)
190190
IREP_ID_ONE(verilog_blocking_assign_ashl)
191+
IREP_ID_ONE(verilog_function_decl)
192+
IREP_ID_ONE(verilog_task_decl)
191193
IREP_ID_ONE(release)
192194
IREP_ID_ONE(force)
193195
IREP_ID_ONE(deassign)

‎src/verilog/parser.y‎

Lines changed: 4 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -2166,8 +2166,7 @@ function_body_declaration:
21662166
';'
21672167
tf_item_declaration_brace statement
21682168
TOK_ENDFUNCTION
2169-
{ init($$, ID_decl);
2170-
stack_expr($$).set(ID_class, ID_function);
2169+
{ init($$, ID_verilog_function_decl);
21712170
addswap($$, ID_type, $1);
21722171
add_as_subtype(stack_type($1), stack_type($1));
21732172
addswap($$, ID_symbol, $2);
@@ -2181,8 +2180,7 @@ function_body_declaration:
21812180
'(' tf_port_list_opt ')' ';'
21822181
tf_item_declaration_brace statement
21832182
TOK_ENDFUNCTION
2184-
{ init($$, ID_decl);
2185-
stack_expr($$).set(ID_class, ID_function);
2183+
{ init($$, ID_verilog_function_decl);
21862184
addswap($$, ID_type, $1);
21872185
add_as_subtype(stack_type($1), stack_type($1));
21882186
addswap($$, ID_symbol, $2);
@@ -2222,8 +2220,7 @@ task_declaration:
22222220
';'
22232221
tf_item_declaration_brace
22242222
statement_or_null TOK_ENDTASK
2225-
{ init($$, ID_decl);
2226-
stack_expr($$).set(ID_class, ID_task);
2223+
{ init($$, ID_verilog_task_decl);
22272224
addswap($$, ID_symbol, $2);
22282225
addswap($$, ID_verilog_declarations, $5);
22292226
addswap($$, ID_body, $6);
@@ -2234,8 +2231,7 @@ task_declaration:
22342231
'(' tf_port_list_opt ')' ';'
22352232
tf_item_declaration_brace
22362233
statement_or_null TOK_ENDTASK
2237-
{ init($$, ID_decl);
2238-
stack_expr($$).set(ID_class, ID_task);
2234+
{ init($$, ID_verilog_task_decl);
22392235
addswap($$, ID_symbol, $2);
22402236
addswap($$, ID_ports, $5);
22412237
addswap($$, ID_verilog_declarations, $8);

‎src/verilog/verilog_elaborate.cpp‎

Lines changed: 60 additions & 54 deletions
Original file line numberDiff line numberDiff line change
@@ -537,76 +537,76 @@ void verilog_typecheckt::collect_symbols(const verilog_declt &decl)
537537
symbols_added.push_back(symbol.name);
538538
}
539539
}
540-
else if(decl_class == ID_function || decl_class == ID_task)
540+
else
541541
{
542-
typet return_type;
542+
DATA_INVARIANT(false, "unexpected decl class " + id2string(decl_class));
543+
}
544+
}
543545

544-
if(decl_class == ID_function)
545-
return_type = elaborate_type(decl.type());
546-
else
547-
return_type = empty_typet();
546+
void verilog_typecheckt::collect_symbols(
547+
const verilog_function_or_task_declt &decl)
548+
{
549+
typet return_type;
548550

549-
auto base_name = decl.get_identifier();
550-
auto identifier = hierarchical_identifier(base_name);
551-
symbolt symbol{identifier, code_typet{{}, std::move(return_type)}, mode};
551+
if(decl.id() == ID_verilog_function_decl)
552+
return_type = elaborate_type(decl.type());
553+
else
554+
return_type = empty_typet();
552555

553-
symbol.base_name = base_name;
554-
symbol.location = decl.source_location();
555-
symbol.pretty_name = strip_verilog_prefix(symbol.name);
556-
symbol.module = module_identifier;
557-
symbol.value = decl;
556+
auto base_name = decl.base_name();
557+
auto identifier = hierarchical_identifier(base_name);
558+
symbolt symbol{identifier, code_typet{{}, std::move(return_type)}, mode};
558559

559-
add_symbol(symbol);
560+
symbol.base_name = base_name;
561+
symbol.location = decl.source_location();
562+
symbol.pretty_name = strip_verilog_prefix(symbol.name);
563+
symbol.module = module_identifier;
564+
symbol.value = decl;
560565

561-
function_or_task_name = symbol.name;
566+
add_symbol(symbol);
562567

563-
// do the ANSI-style ports, if applicable
564-
for(auto &port_decl : decl.ports())
565-
{
566-
// These must have one declarator exactly.
567-
DATA_INVARIANT(
568-
port_decl.declarators().size() == 1, "must have one port declarator");
569-
collect_symbols(port_decl); // rec. call
570-
}
568+
function_or_task_name = symbol.name;
571569

572-
// add a symbol for the return value of functions, if applicable
570+
// do the ANSI-style ports, if applicable
571+
for(auto &port_decl : decl.ports())
572+
{
573+
// These must have one declarator exactly.
574+
DATA_INVARIANT(
575+
port_decl.declarators().size() == 1, "must have one port declarator");
576+
collect_symbols(port_decl); // rec. call
577+
}
573578

574-
if(
575-
decl_class == ID_function &&
576-
to_code_type(symbol.type).return_type().id() != ID_verilog_void)
577-
{
578-
symbolt return_symbol;
579-
return_symbol.is_state_var = true;
580-
return_symbol.is_lvalue = true;
581-
return_symbol.mode = symbol.mode;
582-
return_symbol.module = symbol.module;
583-
return_symbol.base_name = symbol.base_name;
584-
return_symbol.value = nil_exprt();
585-
return_symbol.type = to_code_type(symbol.type).return_type();
579+
// add a symbol for the return value of functions, if applicable
586580

587-
return_symbol.name =
588-
id2string(symbol.name) + "." + id2string(symbol.base_name);
581+
if(
582+
decl.id() == ID_verilog_function_decl &&
583+
to_code_type(symbol.type).return_type().id() != ID_verilog_void)
584+
{
585+
symbolt return_symbol;
586+
return_symbol.is_state_var = true;
587+
return_symbol.is_lvalue = true;
588+
return_symbol.mode = symbol.mode;
589+
return_symbol.module = symbol.module;
590+
return_symbol.base_name = symbol.base_name;
591+
return_symbol.value = nil_exprt();
592+
return_symbol.type = to_code_type(symbol.type).return_type();
589593

590-
return_symbol.pretty_name = strip_verilog_prefix(return_symbol.name);
594+
return_symbol.name =
595+
id2string(symbol.name) + "." + id2string(symbol.base_name);
591596

592-
symbol_table.add(return_symbol);
593-
}
597+
return_symbol.pretty_name = strip_verilog_prefix(return_symbol.name);
594598

595-
// collect symbols in the declarations within the task/function
596-
for(auto &decl : decl.declarations())
597-
collect_symbols(decl);
599+
symbol_table.add(return_symbol);
600+
}
598601

599-
collect_symbols(decl.body());
602+
// collect symbols in the declarations within the task/function
603+
for(auto &sub_decl : decl.declarations())
604+
collect_symbols(sub_decl);
600605

601-
function_or_task_name = "";
602-
}
603-
else
604-
{
605-
DATA_INVARIANT(false, "unexpected decl class " + id2string(decl_class));
606-
}
607-
}
606+
collect_symbols(decl.body());
608607

609-
#include <iostream>
608+
function_or_task_name = "";
609+
}
610610

611611
void verilog_typecheckt::collect_symbols(const verilog_lett &let)
612612
{
@@ -794,6 +794,12 @@ void verilog_typecheckt::collect_symbols(
794794
{
795795
collect_symbols(to_verilog_decl(module_item));
796796
}
797+
else if(
798+
module_item.id() == ID_verilog_function_decl ||
799+
module_item.id() == ID_verilog_task_decl)
800+
{
801+
collect_symbols(to_verilog_function_or_task_decl(module_item));
802+
}
797803
else if(
798804
module_item.id() == ID_verilog_always ||
799805
module_item.id() == ID_verilog_always_comb ||

‎src/verilog/verilog_expr.cpp‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -171,6 +171,11 @@ static void dependencies_rec(
171171
dependencies_rec(declarator.value(), dest);
172172
}
173173
}
174+
else if(
175+
module_item.id() == ID_verilog_function_decl ||
176+
module_item.id() == ID_verilog_task_decl)
177+
{
178+
}
174179
else if(
175180
module_item.id() == ID_verilog_always ||
176181
module_item.id() == ID_verilog_always_comb ||

‎src/verilog/verilog_expr.h‎

Lines changed: 34 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -996,7 +996,6 @@ class verilog_declt:public verilog_statementt
996996
set(ID_class, _class);
997997
}
998998

999-
// When it's not a function or task, there are declarators.
1000999
using declaratort = verilog_declaratort;
10011000
using declaratorst = verilog_declaratorst;
10021001

@@ -1009,15 +1008,36 @@ class verilog_declt:public verilog_statementt
10091008
{
10101009
return (const declaratorst &)operands();
10111010
}
1011+
};
1012+
1013+
inline const verilog_declt &to_verilog_decl(const irept &irep)
1014+
{
1015+
PRECONDITION(irep.id() == ID_decl);
1016+
return static_cast<const verilog_declt &>(irep);
1017+
}
1018+
1019+
inline verilog_declt &to_verilog_decl(exprt &irep)
1020+
{
1021+
PRECONDITION(irep.id() == ID_decl);
1022+
return static_cast<verilog_declt &>(irep);
1023+
}
1024+
1025+
/// function and task declarations
1026+
class verilog_function_or_task_declt : public verilog_module_itemt
1027+
{
1028+
public:
1029+
verilog_function_or_task_declt(irep_idt __id) : verilog_module_itemt(__id)
1030+
{
1031+
}
10121032

10131033
// Function and task declarations have:
1014-
// a) an identifier,
1034+
// a) an base name and identifier,
10151035
// b) an optional list of ANSI-style ports,
10161036
// c) further declarations,
10171037
// d) a body.
1018-
irep_idt get_identifier() const
1038+
irep_idt base_name() const
10191039
{
1020-
return find(ID_symbol).get(ID_identifier);
1040+
return find(ID_symbol).get(ID_base_name);
10211041
}
10221042

10231043
void set_identifier(const irep_idt &identifier)
@@ -1060,16 +1080,20 @@ class verilog_declt:public verilog_statementt
10601080
}
10611081
};
10621082

1063-
inline const verilog_declt &to_verilog_decl(const irept &irep)
1083+
inline const verilog_function_or_task_declt &
1084+
to_verilog_function_or_task_decl(const irept &irep)
10641085
{
1065-
PRECONDITION(irep.id() == ID_decl);
1066-
return static_cast<const verilog_declt &>(irep);
1086+
PRECONDITION(
1087+
irep.id() == ID_verilog_function_decl || irep.id() == ID_verilog_task_decl);
1088+
return static_cast<const verilog_function_or_task_declt &>(irep);
10671089
}
10681090

1069-
inline verilog_declt &to_verilog_decl(exprt &irep)
1091+
inline verilog_function_or_task_declt &
1092+
to_verilog_function_or_task_decl(exprt &irep)
10701093
{
1071-
PRECONDITION(irep.id() == ID_decl);
1072-
return static_cast<verilog_declt &>(irep);
1094+
PRECONDITION(
1095+
irep.id() == ID_verilog_function_decl || irep.id() == ID_verilog_task_decl);
1096+
return static_cast<verilog_function_or_task_declt &>(irep);
10731097
}
10741098

10751099
class verilog_initialt:public verilog_statementt

‎src/verilog/verilog_interfaces.cpp‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -243,6 +243,12 @@ void verilog_typecheckt::interface_module_item(
243243
if(module_item.id()==ID_decl)
244244
{
245245
}
246+
else if(module_item.id() == ID_verilog_function_decl)
247+
{
248+
}
249+
else if(module_item.id() == ID_verilog_task_decl)
250+
{
251+
}
246252
else if(module_item.id()==ID_parameter_decl ||
247253
module_item.id()==ID_local_parameter_decl)
248254
{

‎src/verilog/verilog_synthesis.cpp‎

Lines changed: 32 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -416,7 +416,7 @@ exprt verilog_synthesist::expand_function_call(
416416

417417
// this is essentially inlined
418418
const symbol_exprt &function=to_symbol_expr(call.function());
419-
419+
420420
const symbolt &symbol=ns.lookup(function);
421421

422422
if(symbol.type.id()!=ID_code)
@@ -2062,6 +2062,23 @@ void verilog_synthesist::synth_decl(const verilog_declt &statement) {
20622062

20632063
/*******************************************************************\
20642064
2065+
Function: verilog_synthesist::synth_function_or_task_decl
2066+
2067+
Inputs:
2068+
2069+
Outputs:
2070+
2071+
Purpose:
2072+
2073+
\*******************************************************************/
2074+
2075+
void verilog_synthesist::synth_function_or_task_decl(
2076+
const verilog_function_or_task_declt &statement)
2077+
{
2078+
}
2079+
2080+
/*******************************************************************\
2081+
20652082
Function: verilog_synthesist::synth_block
20662083
20672084
Inputs:
@@ -3125,7 +3142,7 @@ void verilog_synthesist::synth_function_call_or_task_enable(
31253142
else
31263143
{
31273144
const symbolt &symbol=ns.lookup(identifier);
3128-
3145+
31293146
if(symbol.type.id()!=ID_code)
31303147
{
31313148
throw errort().with_location(statement.source_location())
@@ -3283,6 +3300,11 @@ void verilog_synthesist::synth_statement(
32833300
{
32843301
synth_decl(to_verilog_decl(statement));
32853302
}
3303+
else if(
3304+
statement.id() == ID_verilog_function_decl ||
3305+
statement.id() == ID_verilog_task_decl)
3306+
{
3307+
}
32863308
else if(statement.id()==ID_skip)
32873309
{
32883310
// do nothing
@@ -3320,7 +3342,15 @@ void verilog_synthesist::synth_module_item(
33203342
{
33213343
}
33223344
else if(module_item.id()==ID_decl)
3345+
{
33233346
synth_decl(to_verilog_decl(module_item));
3347+
}
3348+
else if(
3349+
module_item.id() == ID_verilog_function_decl ||
3350+
module_item.id() == ID_verilog_task_decl)
3351+
{
3352+
synth_function_or_task_decl(to_verilog_function_or_task_decl(module_item));
3353+
}
33243354
else if(
33253355
module_item.id() == ID_parameter_decl ||
33263356
module_item.id() == ID_local_parameter_decl ||

‎src/verilog/verilog_synthesis_class.h‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -258,6 +258,7 @@ class verilog_synthesist:
258258
// statements
259259
void synth_statement(const verilog_statementt &);
260260
void synth_decl(const verilog_declt &);
261+
void synth_function_or_task_decl(const verilog_function_or_task_declt &);
261262
void synth_block(const verilog_blockt &);
262263
void synth_case(const verilog_statementt &);
263264
void synth_if(const verilog_ift &);

0 commit comments

Comments
 (0)