Skip to content

Commit 25636cf

Browse files
kroeningkroening
committed
SystemVerilog: named sequences
This adds SystemVerilog named sequences.
1 parent 341268f commit 25636cf

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); }
@@ -4190,6 +4232,8 @@ identifier: non_type_identifier;
41904232

41914233
property_identifier: TOK_NON_TYPE_IDENTIFIER;
41924234

4235+
sequence_identifier: TOK_NON_TYPE_IDENTIFIER;
4236+
41934237
variable_identifier: identifier;
41944238

41954239
%%

‎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.
@@ -834,6 +839,10 @@ void verilog_typecheckt::collect_symbols(
834839
{
835840
collect_symbols(to_verilog_property_declaration(module_item));
836841
}
842+
else if(module_item.id() == ID_verilog_sequence_declaration)
843+
{
844+
collect_symbols(to_verilog_sequence_declaration(module_item));
845+
}
837846
else
838847
DATA_INVARIANT(false, "unexpected module item: " + module_item.id_string());
839848
}

‎src/verilog/verilog_expr.h‎

Lines changed: 38 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2620,6 +2620,44 @@ to_verilog_property_declaration(exprt &expr)
26202620
return static_cast<verilog_property_declarationt &>(expr);
26212621
}
26222622

2623+
class verilog_sequence_declarationt : public verilog_module_itemt
2624+
{
2625+
public:
2626+
explicit verilog_sequence_declarationt(exprt sequence)
2627+
{
2628+
add_to_operands(std::move(sequence));
2629+
}
2630+
2631+
const irep_idt &base_name() const
2632+
{
2633+
return get(ID_base_name);
2634+
}
2635+
2636+
const exprt &sequence() const
2637+
{
2638+
return op0();
2639+
}
2640+
2641+
exprt &sequence()
2642+
{
2643+
return op0();
2644+
}
2645+
};
2646+
2647+
inline const verilog_sequence_declarationt &
2648+
to_verilog_sequence_declaration(const exprt &expr)
2649+
{
2650+
PRECONDITION(expr.id() == ID_verilog_sequence_declaration);
2651+
return static_cast<const verilog_sequence_declarationt &>(expr);
2652+
}
2653+
2654+
inline verilog_sequence_declarationt &
2655+
to_verilog_sequence_declaration(exprt &expr)
2656+
{
2657+
PRECONDITION(expr.id() == ID_verilog_sequence_declaration);
2658+
return static_cast<verilog_sequence_declarationt &>(expr);
2659+
}
2660+
26232661
class verilog_streaming_concatenation_exprt : public exprt
26242662
{
26252663
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
@@ -3290,6 +3290,9 @@ void verilog_synthesist::synth_module_item(
32903290
else if(module_item.id() == ID_verilog_property_declaration)
32913291
{
32923292
}
3293+
else if(module_item.id() == ID_verilog_sequence_declaration)
3294+
{
3295+
}
32933296
else
32943297
{
32953298
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
@@ -1699,6 +1699,10 @@ void verilog_typecheckt::convert_module_item(
16991699
{
17001700
convert_property_declaration(to_verilog_property_declaration(module_item));
17011701
}
1702+
else if(module_item.id() == ID_verilog_sequence_declaration)
1703+
{
1704+
convert_sequence_declaration(to_verilog_sequence_declaration(module_item));
1705+
}
17021706
else
17031707
{
17041708
throw errort().with_location(module_item.source_location())
@@ -1743,6 +1747,40 @@ void verilog_typecheckt::convert_property_declaration(
17431747

17441748
/*******************************************************************\
17451749
1750+
Function: verilog_typecheckt::convert_sequence_declaration
1751+
1752+
Inputs:
1753+
1754+
Outputs:
1755+
1756+
Purpose:
1757+
1758+
\*******************************************************************/
1759+
1760+
void verilog_typecheckt::convert_sequence_declaration(
1761+
verilog_sequence_declarationt &declaration)
1762+
{
1763+
auto base_name = declaration.base_name();
1764+
auto full_identifier = hierarchical_identifier(base_name);
1765+
1766+
convert_sva(declaration.sequence());
1767+
1768+
auto type = bool_typet{};
1769+
type.set(ID_C_verilog_type, ID_verilog_sequence_declaration);
1770+
symbolt symbol{full_identifier, type, mode};
1771+
1772+
symbol.module = module_identifier;
1773+
symbol.base_name = base_name;
1774+
symbol.pretty_name = strip_verilog_prefix(symbol.name);
1775+
symbol.is_macro = true;
1776+
symbol.value = declaration.sequence();
1777+
symbol.location = declaration.source_location();
1778+
1779+
add_symbol(std::move(symbol));
1780+
}
1781+
1782+
/*******************************************************************\
1783+
17461784
Function: verilog_typecheckt::convert_statements
17471785
17481786
Inputs:

0 commit comments

Comments
 (0)