Skip to content

Commit f4069fa

Browse files
tautschnigtautschnig
authored
Merge pull request #334 from diffblue/function_ports1
Verilog: function/task ports
2 parents bacc62d + b9dc889 commit f4069fa

File tree

6 files changed

+138
-17
lines changed

6 files changed

+138
-17
lines changed

‎regression/verilog/functioncall/function_ports1.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
function_ports1.v
3+
--module main --bound 0
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main\.property\.test16\] always .*: PROVED up to bound 0$
7+
--
8+
^warning: ignoring

‎regression/verilog/functioncall/function_ports1.v

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
module main;
2+
3+
function [31:0] clog2(input [63:0] value);
4+
reg [63:0] tmp;
5+
begin
6+
tmp = value - 1;
7+
for (clog2 = 0; tmp>0; clog2 = clog2 + 32'h1)
8+
tmp = tmp >> 1;
9+
end
10+
endfunction // clog2
11+
12+
wire [31:0] clog2_of_16 = clog2(16);
13+
14+
always assert test16: clog2_of_16 == 4;
15+
16+
endmodule

‎src/hw_cbmc_irep_ids.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -123,6 +123,7 @@ IREP_ID_ONE(verilog_longint)
123123
IREP_ID_ONE(verilog_byte)
124124
IREP_ID_ONE(verilog_bit)
125125
IREP_ID_ONE(verilog_logic)
126+
IREP_ID_ONE(verilog_ref)
126127
IREP_ID_ONE(verilog_reg)
127128
IREP_ID_ONE(verilog_integer)
128129
IREP_ID_ONE(verilog_time)

‎src/verilog/parser.y

Lines changed: 89 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -842,6 +842,17 @@ module_port_output_declaration:
842842
mto($$, $3); }
843843
;
844844

845+
port_direction:
846+
TOK_INPUT
847+
{ init($$, ID_input); }
848+
| TOK_OUTPUT
849+
{ init($$, ID_output); }
850+
| TOK_INOUT
851+
{ init($$, ID_inout); }
852+
| TOK_REF
853+
{ init($$, ID_verilog_ref); }
854+
;
855+
845856
// System Verilog standard 1800-2017
846857
// A.1.4 Module items
847858

@@ -1731,20 +1742,38 @@ struct_union:
17311742
// System Verilog standard 1800-2017
17321743
// A.2.6 Function declarations
17331744

1734-
function_declaration:
1735-
TOK_FUNCTION
1736-
automatic_opt signing_opt range_or_type_opt
1745+
function_declaration: TOK_FUNCTION automatic_opt function_body_declaration
1746+
{ $$ = $3; }
1747+
;
1748+
1749+
function_body_declaration:
1750+
signing_opt range_or_type_opt
17371751
function_identifier
1738-
{ push_scope(stack_expr($5).get(ID_identifier), "."); }
1739-
list_of_ports_opt ';'
1752+
{ push_scope(stack_expr($3).get(ID_identifier), "."); }
1753+
';'
17401754
tf_item_declaration_brace statement
17411755
TOK_ENDFUNCTION
17421756
{ init($$, ID_decl);
1743-
stack_expr($$).set(ID_class, ID_function);
1744-
addswap($$, ID_type, $4);
1745-
add_as_subtype(stack_type($4), stack_type($3));
1746-
addswap($$, ID_symbol, $5);
1747-
addswap($$, ID_ports, $7);
1757+
stack_expr($$).set(ID_class, ID_function);
1758+
addswap($$, ID_type, $2);
1759+
add_as_subtype(stack_type($2), stack_type($1));
1760+
addswap($$, ID_symbol, $3);
1761+
addswap($$, "declarations", $6);
1762+
addswap($$, ID_body, $7);
1763+
pop_scope();
1764+
}
1765+
| signing_opt range_or_type_opt
1766+
function_identifier
1767+
{ push_scope(stack_expr($3).get(ID_identifier), "."); }
1768+
'(' tf_port_list_opt ')' ';'
1769+
tf_item_declaration_brace statement
1770+
TOK_ENDFUNCTION
1771+
{ init($$, ID_decl);
1772+
stack_expr($$).set(ID_class, ID_function);
1773+
addswap($$, ID_type, $2);
1774+
add_as_subtype(stack_type($2), stack_type($1));
1775+
addswap($$, ID_symbol, $3);
1776+
addswap($$, ID_ports, $6);
17481777
addswap($$, "declarations", $9);
17491778
addswap($$, ID_body, $10);
17501779
pop_scope();
@@ -1793,22 +1822,67 @@ function_prototype: TOK_FUNCTION data_type_or_void function_identifier
17931822
task_declaration:
17941823
TOK_TASK task_identifier
17951824
{ push_scope(stack_expr($2).get(ID_identifier), "."); }
1796-
list_of_ports_opt ';'
1825+
';'
17971826
tf_item_declaration_brace
17981827
statement_or_null TOK_ENDTASK
17991828
{ init($$, ID_decl);
1800-
stack_expr($$).set(ID_class, ID_task);
1829+
stack_expr($$).set(ID_class, ID_task);
18011830
addswap($$, ID_symbol, $2);
1802-
addswap($$, ID_ports, $4);
1803-
addswap($$, "declarations", $6);
1804-
addswap($$, ID_body, $7);
1831+
addswap($$, "declarations", $5);
1832+
addswap($$, ID_body, $6);
1833+
pop_scope();
1834+
}
1835+
| TOK_TASK task_identifier
1836+
{ push_scope(stack_expr($2).get(ID_identifier), "."); }
1837+
'(' tf_port_list_opt ')' ';'
1838+
tf_item_declaration_brace
1839+
statement_or_null TOK_ENDTASK
1840+
{ init($$, ID_decl);
1841+
stack_expr($$).set(ID_class, ID_task);
1842+
addswap($$, ID_symbol, $2);
1843+
addswap($$, ID_ports, $5);
1844+
addswap($$, "declarations", $8);
1845+
addswap($$, ID_body, $9);
18051846
pop_scope();
18061847
}
18071848
;
18081849

18091850
task_prototype: TOK_TASK task_identifier
18101851
;
18111852

1853+
tf_port_list_opt:
1854+
/* Optional */
1855+
{ init($$); }
1856+
| tf_port_list
1857+
;
1858+
1859+
tf_port_list:
1860+
tf_port_item
1861+
{ init($$); mts($$, $1); }
1862+
| tf_port_list ',' tf_port_item
1863+
{ $$ = $1; mts($$, $3); }
1864+
;
1865+
1866+
tf_port_item:
1867+
attribute_instance_brace
1868+
tf_port_direction_opt
1869+
data_type_or_implicit
1870+
port_identifier
1871+
variable_dimension_brace
1872+
{ init($$, ID_decl);
1873+
addswap($$, ID_class, $2);
1874+
addswap($$, ID_type, $3);
1875+
stack_expr($4).id(ID_declarator);
1876+
mto($$, $4); }
1877+
;
1878+
1879+
tf_port_direction_opt:
1880+
/* Optional */
1881+
| port_direction
1882+
| TOK_CONST TOK_REF
1883+
{ $$ = $2; }
1884+
;
1885+
18121886
// System Verilog standard 1800-2017
18131887
// A.2.8 Block item declarations
18141888

‎src/verilog/verilog_elaborate.cpp

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -532,6 +532,15 @@ void verilog_typecheckt::collect_symbols(const verilog_declt &decl)
532532

533533
function_or_task_name = symbol.name;
534534

535+
// do the ANSI-style ports, if applicable
536+
for(auto &port_decl : decl.ports())
537+
{
538+
// These must have one declarator exactly.
539+
DATA_INVARIANT(
540+
port_decl.declarators().size() == 1, "must have one port declarator");
541+
collect_symbols(port_decl); // rec. call
542+
}
543+
535544
// add a symbol for the return value of functions, if applicable
536545

537546
if(decl_class == ID_function)

‎src/verilog/verilog_expr.h

Lines changed: 15 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -689,8 +689,9 @@ class verilog_declt:public verilog_statementt
689689

690690
// Function and task declarations have:
691691
// a) an identifier,
692-
// b) further declarations,
693-
// c) a body.
692+
// b) an optional list of ANSI-style ports,
693+
// c) further declarations,
694+
// d) a body.
694695
irep_idt get_identifier() const
695696
{
696697
return find(ID_symbol).get(ID_identifier);
@@ -701,6 +702,18 @@ class verilog_declt:public verilog_statementt
701702
add(ID_symbol).set(ID_identifier, identifier);
702703
}
703704

705+
using portst = std::vector<verilog_declt>;
706+
707+
portst &ports()
708+
{
709+
return (portst &)(add(ID_ports).get_sub());
710+
}
711+
712+
const portst &ports() const
713+
{
714+
return (const portst &)(find(ID_ports).get_sub());
715+
}
716+
704717
using declarationst = std::vector<verilog_declt>;
705718

706719
declarationst &declarations()

0 commit comments

Comments
 (0)