Skip to content

Commit 5f864c0

Browse files
tautschnigtautschnig
authored
Merge pull request #864 from diffblue/verilog-named-sequence
SystemVerilog: named sequences
2 parents 798b5e0 + 25636cf commit 5f864c0

File tree

11 files changed

+165
-1
lines changed

11 files changed

+165
-1
lines changed

‎CHANGELOG‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@
66
* BMC: support SVA sequence intersect
77
* SystemVerilog: streaming concatenation {<<{...}} and {>>{...}}
88
* SystemVerilog: set membership operator
9+
* SystemVerilog: named sequences
910

1011
# EBMC 5.3
1112

‎regression/verilog/SVA/named_sequence1.desc‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
named_sequence1.sv
3+
--bound 0
4+
^\[main\.assert\.1\] always main\.x_is_ten: PROVED up to bound 0$
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
--
8+
^warning: ignoring
9+
--

‎regression/verilog/SVA/named_sequence1.sv‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
module main(input clk);
2+
3+
wire [31:0] x = 10;
4+
5+
sequence x_is_ten;
6+
x == 10 ##1 x >= 0
7+
endsequence : x_is_ten
8+
9+
assert property (x_is_ten);
10+
11+
sequence x_is_twenty;
12+
// the ; is optional
13+
x == 20;
14+
endsequence : x_is_twenty
15+
16+
endmodule

‎src/hw_cbmc_irep_ids.h‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -96,6 +96,7 @@ IREP_ID_ONE(verilog_indexed_part_select_plus)
9696
IREP_ID_ONE(verilog_indexed_part_select_minus)
9797
IREP_ID_ONE(verilog_past)
9898
IREP_ID_ONE(verilog_property_declaration)
99+
IREP_ID_ONE(verilog_sequence_declaration)
99100
IREP_ID_ONE(verilog_value_range)
100101
IREP_ID_ONE(verilog_void)
101102
IREP_ID_ONE(verilog_streaming_concatenation_left_to_right)

‎src/verilog/parser.y‎

Lines changed: 45 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2245,11 +2245,12 @@ expect_property_statement: TOK_EXPECT '(' property_spec ')' action_block
22452245

22462246
assertion_item_declaration:
22472247
property_declaration
2248+
| sequence_declaration
22482249
;
22492250

22502251
property_declaration:
22512252
TOK_PROPERTY property_identifier property_port_list_paren_opt ';'
2252-
property_spec
2253+
property_spec semicolon_opt
22532254
TOK_ENDPROPERTY property_identifier_opt
22542255
{ init($$, ID_verilog_property_declaration);
22552256
stack_expr($$).set(ID_base_name, stack_expr($2).id());
@@ -2386,6 +2387,47 @@ property_case_item:
23862387
{ init($$, ID_case_item); mto($$, $3); }
23872388
;
23882389

2390+
sequence_declaration:
2391+
"sequence" { init($$, ID_verilog_sequence_declaration); }
2392+
sequence_identifier sequence_port_list_opt ';'
2393+
sequence_expr semicolon_opt
2394+
"endsequence" sequence_identifier_opt
2395+
{ $$=$2;
2396+
stack_expr($$).set(ID_base_name, stack_expr($3).id());
2397+
mto($$, $6);
2398+
}
2399+
;
2400+
2401+
sequence_port_list_opt:
2402+
/* Optional */
2403+
{ init($$); }
2404+
| '(' ')'
2405+
{ init($$); }
2406+
| '(' sequence_port_list ')'
2407+
{ $$=$2; }
2408+
;
2409+
2410+
sequence_port_list:
2411+
sequence_port_item
2412+
{ init($$); mto($$, $1); }
2413+
| sequence_port_list sequence_port_item
2414+
{ $$=$1; mto($$, $2); }
2415+
;
2416+
2417+
sequence_port_item:
2418+
formal_port_identifier
2419+
;
2420+
2421+
sequence_identifier_opt:
2422+
/* Optional */
2423+
| TOK_COLON sequence_identifier
2424+
;
2425+
2426+
semicolon_opt:
2427+
/* Optional */
2428+
| ';'
2429+
;
2430+
23892431
expression_or_dist_brace:
23902432
expression_or_dist
23912433
{ init($$, "patterns"); mto($$, $1); }
@@ -4202,6 +4244,8 @@ identifier: non_type_identifier;
42024244

42034245
property_identifier: TOK_NON_TYPE_IDENTIFIER;
42044246

4247+
sequence_identifier: TOK_NON_TYPE_IDENTIFIER;
4248+
42054249
variable_identifier: identifier;
42064250

42074251
%%

‎src/verilog/verilog_elaborate.cpp‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -118,6 +118,11 @@ void verilog_typecheckt::collect_symbols(
118118
{
119119
}
120120

121+
void verilog_typecheckt::collect_symbols(
122+
const verilog_sequence_declarationt &declaration)
123+
{
124+
}
125+
121126
void verilog_typecheckt::collect_symbols(const typet &type)
122127
{
123128
// These types are not yet converted.
@@ -843,6 +848,10 @@ void verilog_typecheckt::collect_symbols(
843848
{
844849
collect_symbols(to_verilog_property_declaration(module_item));
845850
}
851+
else if(module_item.id() == ID_verilog_sequence_declaration)
852+
{
853+
collect_symbols(to_verilog_sequence_declaration(module_item));
854+
}
846855
else
847856
DATA_INVARIANT(false, "unexpected module item: " + module_item.id_string());
848857
}

‎src/verilog/verilog_expr.h‎

Lines changed: 38 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2782,6 +2782,44 @@ to_verilog_property_declaration(exprt &expr)
27822782
return static_cast<verilog_property_declarationt &>(expr);
27832783
}
27842784

2785+
class verilog_sequence_declarationt : public verilog_module_itemt
2786+
{
2787+
public:
2788+
explicit verilog_sequence_declarationt(exprt sequence)
2789+
{
2790+
add_to_operands(std::move(sequence));
2791+
}
2792+
2793+
const irep_idt &base_name() const
2794+
{
2795+
return get(ID_base_name);
2796+
}
2797+
2798+
const exprt &sequence() const
2799+
{
2800+
return op0();
2801+
}
2802+
2803+
exprt &sequence()
2804+
{
2805+
return op0();
2806+
}
2807+
};
2808+
2809+
inline const verilog_sequence_declarationt &
2810+
to_verilog_sequence_declaration(const exprt &expr)
2811+
{
2812+
PRECONDITION(expr.id() == ID_verilog_sequence_declaration);
2813+
return static_cast<const verilog_sequence_declarationt &>(expr);
2814+
}
2815+
2816+
inline verilog_sequence_declarationt &
2817+
to_verilog_sequence_declaration(exprt &expr)
2818+
{
2819+
PRECONDITION(expr.id() == ID_verilog_sequence_declaration);
2820+
return static_cast<verilog_sequence_declarationt &>(expr);
2821+
}
2822+
27852823
class verilog_streaming_concatenation_exprt : public exprt
27862824
{
27872825
public:

‎src/verilog/verilog_interfaces.cpp‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -306,6 +306,9 @@ void verilog_typecheckt::interface_module_item(
306306
else if(module_item.id() == ID_verilog_property_declaration)
307307
{
308308
}
309+
else if(module_item.id() == ID_verilog_sequence_declaration)
310+
{
311+
}
309312
else
310313
{
311314
DATA_INVARIANT(false, "unexpected module item: " + module_item.id_string());

‎src/verilog/verilog_synthesis.cpp‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3305,6 +3305,9 @@ void verilog_synthesist::synth_module_item(
33053305
else if(module_item.id() == ID_verilog_property_declaration)
33063306
{
33073307
}
3308+
else if(module_item.id() == ID_verilog_sequence_declaration)
3309+
{
3310+
}
33083311
else
33093312
{
33103313
throw errort().with_location(module_item.source_location())

‎src/verilog/verilog_typecheck.cpp‎

Lines changed: 38 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1737,6 +1737,10 @@ void verilog_typecheckt::convert_module_item(
17371737
{
17381738
convert_property_declaration(to_verilog_property_declaration(module_item));
17391739
}
1740+
else if(module_item.id() == ID_verilog_sequence_declaration)
1741+
{
1742+
convert_sequence_declaration(to_verilog_sequence_declaration(module_item));
1743+
}
17401744
else
17411745
{
17421746
throw errort().with_location(module_item.source_location())
@@ -1781,6 +1785,40 @@ void verilog_typecheckt::convert_property_declaration(
17811785

17821786
/*******************************************************************\
17831787
1788+
Function: verilog_typecheckt::convert_sequence_declaration
1789+
1790+
Inputs:
1791+
1792+
Outputs:
1793+
1794+
Purpose:
1795+
1796+
\*******************************************************************/
1797+
1798+
void verilog_typecheckt::convert_sequence_declaration(
1799+
verilog_sequence_declarationt &declaration)
1800+
{
1801+
auto base_name = declaration.base_name();
1802+
auto full_identifier = hierarchical_identifier(base_name);
1803+
1804+
convert_sva(declaration.sequence());
1805+
1806+
auto type = bool_typet{};
1807+
type.set(ID_C_verilog_type, ID_verilog_sequence_declaration);
1808+
symbolt symbol{full_identifier, type, mode};
1809+
1810+
symbol.module = module_identifier;
1811+
symbol.base_name = base_name;
1812+
symbol.pretty_name = strip_verilog_prefix(symbol.name);
1813+
symbol.is_macro = true;
1814+
symbol.value = declaration.sequence();
1815+
symbol.location = declaration.source_location();
1816+
1817+
add_symbol(std::move(symbol));
1818+
}
1819+
1820+
/*******************************************************************\
1821+
17841822
Function: verilog_typecheckt::convert_statements
17851823
17861824
Inputs:

0 commit comments

Comments
 (0)