Skip to content

Commit 43e8ead

Browse files
kroeningkroening
committed
SystemVerilog: restrict statement
This adds the SystemVerilog restrict statement.
1 parent 03d9ee4 commit 43e8ead

File tree

7 files changed

+53
-3
lines changed

7 files changed

+53
-3
lines changed

‎src/hw_cbmc_irep_ids.h‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -131,6 +131,7 @@ IREP_ID_ONE(verilog_assert_property)
131131
IREP_ID_ONE(verilog_assume_property)
132132
IREP_ID_ONE(verilog_cover_property)
133133
IREP_ID_ONE(verilog_covergroup)
134+
IREP_ID_ONE(verilog_restrict_property)
134135
IREP_ID_ONE(verilog_expect_property)
135136
IREP_ID_ONE(verilog_smv_assert)
136137
IREP_ID_ONE(verilog_smv_assume)

‎src/verilog/parser.y‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2020,6 +2020,7 @@ concurrent_assertion_statement:
20202020
assert_property_statement
20212021
| assume_property_statement
20222022
| cover_property_statement
2023+
| restrict_property_statement
20232024
;
20242025

20252026
/* This one mimicks functionality in Cadence SMV */
@@ -2081,6 +2082,10 @@ cover_property_statement: TOK_COVER TOK_PROPERTY '(' property_spec ')' action_bl
20812082
{ init($$, ID_verilog_cover_property); mto($$, $4); mto($$, $6); }
20822083
;
20832084

2085+
restrict_property_statement: TOK_RESTRICT TOK_PROPERTY '(' property_spec ')' ';'
2086+
{ init($$, ID_verilog_restrict_property); mto($$, $4); mto($$, $6); }
2087+
;
2088+
20842089
expect_property_statement: TOK_EXPECT '(' property_spec ')' action_block
20852090
{ init($$, ID_verilog_expect_property); mto($$, $3); mto($$, $5); }
20862091
;

‎src/verilog/verilog_elaborate.cpp‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -630,6 +630,7 @@ void verilog_typecheckt::collect_symbols(const verilog_statementt &statement)
630630
else if(
631631
statement.id() == ID_verilog_assert_property ||
632632
statement.id() == ID_verilog_assume_property ||
633+
statement.id() == ID_verilog_restrict_property ||
633634
statement.id() == ID_verilog_cover_property ||
634635
statement.id() == ID_verilog_expect_property)
635636
{
@@ -791,6 +792,7 @@ void verilog_typecheckt::collect_symbols(
791792
else if(
792793
module_item.id() == ID_verilog_assert_property ||
793794
module_item.id() == ID_verilog_assume_property ||
795+
module_item.id() == ID_verilog_restrict_property ||
794796
module_item.id() == ID_verilog_cover_property)
795797
{
796798
}

‎src/verilog/verilog_expr.h‎

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1754,6 +1754,7 @@ to_verilog_assert_assume_cover_module_item(
17541754
PRECONDITION(
17551755
module_item.id() == ID_verilog_assert_property ||
17561756
module_item.id() == ID_verilog_assume_property ||
1757+
module_item.id() == ID_verilog_restrict_property ||
17571758
module_item.id() == ID_verilog_cover_property);
17581759
binary_exprt::check(module_item);
17591760
return static_cast<const verilog_assert_assume_cover_module_itemt &>(
@@ -1766,6 +1767,7 @@ to_verilog_assert_assume_cover_module_item(verilog_module_itemt &module_item)
17661767
PRECONDITION(
17671768
module_item.id() == ID_verilog_assert_property ||
17681769
module_item.id() == ID_verilog_assume_property ||
1770+
module_item.id() == ID_verilog_restrict_property ||
17691771
module_item.id() == ID_verilog_cover_property);
17701772
binary_exprt::check(module_item);
17711773
return static_cast<verilog_assert_assume_cover_module_itemt &>(module_item);
@@ -1813,6 +1815,7 @@ to_verilog_assert_assume_cover_statement(const verilog_statementt &statement)
18131815
statement.id() == ID_verilog_smv_assert ||
18141816
statement.id() == ID_verilog_immediate_assume ||
18151817
statement.id() == ID_verilog_assume_property ||
1818+
statement.id() == ID_verilog_restrict_property ||
18161819
statement.id() == ID_verilog_smv_assume ||
18171820
statement.id() == ID_verilog_immediate_cover ||
18181821
statement.id() == ID_verilog_cover_property);
@@ -1829,6 +1832,7 @@ to_verilog_assert_assume_cover_statement(verilog_statementt &statement)
18291832
statement.id() == ID_verilog_smv_assert ||
18301833
statement.id() == ID_verilog_immediate_assume ||
18311834
statement.id() == ID_verilog_assume_property ||
1835+
statement.id() == ID_verilog_restrict_property ||
18321836
statement.id() == ID_verilog_smv_assume ||
18331837
statement.id() == ID_verilog_immediate_cover ||
18341838
statement.id() == ID_verilog_cover_property);
@@ -1936,6 +1940,32 @@ to_verilog_assume_statement(verilog_statementt &statement)
19361940
return static_cast<verilog_assume_statementt &>(statement);
19371941
}
19381942

1943+
class verilog_restrict_statementt
1944+
: public verilog_assert_assume_cover_statementt
1945+
{
1946+
public:
1947+
verilog_restrict_statementt()
1948+
: verilog_assert_assume_cover_statementt(ID_verilog_restrict_property)
1949+
{
1950+
}
1951+
};
1952+
1953+
inline const verilog_restrict_statementt &
1954+
to_verilog_restrict_statement(const verilog_statementt &statement)
1955+
{
1956+
PRECONDITION(statement.id() == ID_verilog_restrict_property);
1957+
binary_exprt::check(statement);
1958+
return static_cast<const verilog_restrict_statementt &>(statement);
1959+
}
1960+
1961+
inline verilog_restrict_statementt &
1962+
to_verilog_restrict_statement(verilog_statementt &statement)
1963+
{
1964+
PRECONDITION(statement.id() == ID_verilog_restrict_property);
1965+
binary_exprt::check(statement);
1966+
return static_cast<verilog_restrict_statementt &>(statement);
1967+
}
1968+
19391969
class verilog_module_sourcet : public irept
19401970
{
19411971
public:

‎src/verilog/verilog_interfaces.cpp‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -267,6 +267,7 @@ void verilog_typecheckt::interface_module_item(
267267
else if(
268268
module_item.id() == ID_verilog_assert_property ||
269269
module_item.id() == ID_verilog_assume_property ||
270+
module_item.id() == ID_verilog_restrict_property ||
270271
module_item.id() == ID_verilog_cover_property)
271272
{
272273
// done later

‎src/verilog/verilog_synthesis.cpp‎

Lines changed: 11 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -2549,6 +2549,7 @@ void verilog_synthesist::synth_assert_assume_cover(
25492549
// mark 'assume' and 'cover' properties as such
25502550
if(
25512551
statement.id() == ID_verilog_assume_property ||
2552+
statement.id() == ID_verilog_restrict_property ||
25522553
statement.id() == ID_verilog_immediate_assume ||
25532554
statement.id() == ID_verilog_smv_assume)
25542555
{
@@ -2604,6 +2605,7 @@ void verilog_synthesist::synth_assert_assume_cover(
26042605
// mark 'assume' and 'cover' properties as such
26052606
if(
26062607
statement.id() == ID_verilog_assume_property ||
2608+
statement.id() == ID_verilog_restrict_property ||
26072609
statement.id() == ID_verilog_immediate_assume ||
26082610
statement.id() == ID_verilog_smv_assume)
26092611
{
@@ -2642,7 +2644,8 @@ void verilog_synthesist::synth_assert_assume_cover(
26422644

26432645
if(
26442646
module_item.id() == ID_verilog_assert_property ||
2645-
module_item.id() == ID_verilog_assume_property)
2647+
module_item.id() == ID_verilog_assume_property ||
2648+
module_item.id() == ID_verilog_restrict_property)
26462649
{
26472650
// Concurrent assertions and assumptions come with an implicit 'always'
26482651
// (1800-2017 Sec 16.12.11).
@@ -2669,7 +2672,9 @@ void verilog_synthesist::synth_assert_assume_cover(
26692672
if(cond.id() != ID_sva_always)
26702673
cond = sva_always_exprt{cond};
26712674
}
2672-
else if(module_item.id() == ID_verilog_assume_property)
2675+
else if(
2676+
module_item.id() == ID_verilog_assume_property ||
2677+
module_item.id() == ID_verilog_restrict_property)
26732678
{
26742679
// Concurrent assumptions come with an implicit 'always'
26752680
// (1800-2017 Sec 16.12.11).
@@ -3415,6 +3420,7 @@ void verilog_synthesist::synth_statement(
34153420
else if(
34163421
statement.id() == ID_verilog_immediate_assume ||
34173422
statement.id() == ID_verilog_assume_property ||
3423+
statement.id() == ID_verilog_restrict_property ||
34183424
statement.id() == ID_verilog_smv_assume)
34193425
{
34203426
synth_assert_assume_cover(
@@ -3525,7 +3531,9 @@ void verilog_synthesist::synth_module_item(
35253531
synth_assert_assume_cover(
35263532
to_verilog_assert_assume_cover_module_item(module_item));
35273533
}
3528-
else if(module_item.id() == ID_verilog_assume_property)
3534+
else if(
3535+
module_item.id() == ID_verilog_assume_property ||
3536+
module_item.id() == ID_verilog_restrict_property)
35293537
{
35303538
synth_assert_assume_cover(
35313539
to_verilog_assert_assume_cover_module_item(module_item));

‎src/verilog/verilog_typecheck.cpp‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1484,6 +1484,7 @@ void verilog_typecheckt::convert_statement(
14841484
else if(
14851485
statement.id() == ID_verilog_immediate_assume ||
14861486
statement.id() == ID_verilog_assume_property ||
1487+
statement.id() == ID_verilog_restrict_property ||
14871488
statement.id() == ID_verilog_smv_assume)
14881489
{
14891490
convert_assert_assume_cover(to_verilog_assume_statement(statement));
@@ -1531,6 +1532,7 @@ void verilog_typecheckt::convert_statement(
15311532
if(
15321533
sub_statement.id() == ID_verilog_assert_property ||
15331534
sub_statement.id() == ID_verilog_assume_property ||
1535+
sub_statement.id() == ID_verilog_restrict_property ||
15341536
sub_statement.id() == ID_verilog_cover_property)
15351537
{
15361538
sub_statement.set(ID_identifier, label_statement.label());
@@ -1587,6 +1589,7 @@ void verilog_typecheckt::convert_module_item(
15871589
else if(
15881590
module_item.id() == ID_verilog_assert_property ||
15891591
module_item.id() == ID_verilog_assume_property ||
1592+
module_item.id() == ID_verilog_restrict_property ||
15901593
module_item.id() == ID_verilog_cover_property)
15911594
{
15921595
convert_assert_assume_cover(

0 commit comments

Comments
 (0)