Skip to content

SystemVerilog: restrict statement #676

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Sep 10, 2024
Merged

SystemVerilog: restrict statement #676

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 10 additions & 0 deletions regression/verilog/SVA/restrict1.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
CORE
restrict1.sv
--module main --bound 10
^\[main\.p0\] always main\.x != 5: ASSUMED$
^\[main\.p1\] always main\.x != 6: PROVED up to bound 10$
^EXIT=0$
^SIGNAL=0$
--
^warning: ignoring
--
15 changes: 15 additions & 0 deletions regression/verilog/SVA/restrict1.sv
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
module main(input clk, input en);

reg [31:0] x;

initial x=0;

always @(posedge clk)
if(en)
x<=x+1;

p0: restrict property (x!=5);

p1: assert property (x!=6);

endmodule
1 change: 1 addition & 0 deletions src/hw_cbmc_irep_ids.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -135,6 +135,7 @@ IREP_ID_ONE(verilog_assert_property)
IREP_ID_ONE(verilog_assume_property)
IREP_ID_ONE(verilog_cover_property)
IREP_ID_ONE(verilog_covergroup)
IREP_ID_ONE(verilog_restrict_property)
IREP_ID_ONE(verilog_expect_property)
IREP_ID_ONE(verilog_smv_assert)
IREP_ID_ONE(verilog_smv_assume)
Expand Down
5 changes: 5 additions & 0 deletions src/verilog/parser.y
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2022,6 +2022,7 @@ concurrent_assertion_statement:
assert_property_statement
| assume_property_statement
| cover_property_statement
| restrict_property_statement
;

/* This one mimicks functionality in Cadence SMV */
Expand Down Expand Up @@ -2083,6 +2084,10 @@ cover_property_statement: TOK_COVER TOK_PROPERTY '(' property_spec ')' action_bl
{ init($$, ID_verilog_cover_property); mto($$, $4); mto($$, $6); }
;

restrict_property_statement: TOK_RESTRICT TOK_PROPERTY '(' property_spec ')' ';'
{ init($$, ID_verilog_restrict_property); mto($$, $4); mto($$, $6); }
;

expect_property_statement: TOK_EXPECT '(' property_spec ')' action_block
{ init($$, ID_verilog_expect_property); mto($$, $3); mto($$, $5); }
;
Expand Down
2 changes: 2 additions & 0 deletions src/verilog/verilog_elaborate.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -630,6 +630,7 @@ void verilog_typecheckt::collect_symbols(const verilog_statementt &statement)
else if(
statement.id() == ID_verilog_assert_property ||
statement.id() == ID_verilog_assume_property ||
statement.id() == ID_verilog_restrict_property ||
statement.id() == ID_verilog_cover_property ||
statement.id() == ID_verilog_expect_property)
{
Expand Down Expand Up @@ -791,6 +792,7 @@ void verilog_typecheckt::collect_symbols(
else if(
module_item.id() == ID_verilog_assert_property ||
module_item.id() == ID_verilog_assume_property ||
module_item.id() == ID_verilog_restrict_property ||
module_item.id() == ID_verilog_cover_property)
{
}
Expand Down
30 changes: 30 additions & 0 deletions src/verilog/verilog_expr.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1798,6 +1798,7 @@ to_verilog_assert_assume_cover_module_item(
PRECONDITION(
module_item.id() == ID_verilog_assert_property ||
module_item.id() == ID_verilog_assume_property ||
module_item.id() == ID_verilog_restrict_property ||
module_item.id() == ID_verilog_cover_property);
binary_exprt::check(module_item);
return static_cast<const verilog_assert_assume_cover_module_itemt &>(
Expand All @@ -1810,6 +1811,7 @@ to_verilog_assert_assume_cover_module_item(verilog_module_itemt &module_item)
PRECONDITION(
module_item.id() == ID_verilog_assert_property ||
module_item.id() == ID_verilog_assume_property ||
module_item.id() == ID_verilog_restrict_property ||
module_item.id() == ID_verilog_cover_property);
binary_exprt::check(module_item);
return static_cast<verilog_assert_assume_cover_module_itemt &>(module_item);
Expand Down Expand Up @@ -1857,6 +1859,7 @@ to_verilog_assert_assume_cover_statement(const verilog_statementt &statement)
statement.id() == ID_verilog_smv_assert ||
statement.id() == ID_verilog_immediate_assume ||
statement.id() == ID_verilog_assume_property ||
statement.id() == ID_verilog_restrict_property ||
statement.id() == ID_verilog_smv_assume ||
statement.id() == ID_verilog_immediate_cover ||
statement.id() == ID_verilog_cover_property);
Expand All @@ -1873,6 +1876,7 @@ to_verilog_assert_assume_cover_statement(verilog_statementt &statement)
statement.id() == ID_verilog_smv_assert ||
statement.id() == ID_verilog_immediate_assume ||
statement.id() == ID_verilog_assume_property ||
statement.id() == ID_verilog_restrict_property ||
statement.id() == ID_verilog_smv_assume ||
statement.id() == ID_verilog_immediate_cover ||
statement.id() == ID_verilog_cover_property);
Expand Down Expand Up @@ -1980,6 +1984,32 @@ to_verilog_assume_statement(verilog_statementt &statement)
return static_cast<verilog_assume_statementt &>(statement);
}

class verilog_restrict_statementt
: public verilog_assert_assume_cover_statementt
{
public:
verilog_restrict_statementt()
: verilog_assert_assume_cover_statementt(ID_verilog_restrict_property)
{
}
};

inline const verilog_restrict_statementt &
to_verilog_restrict_statement(const verilog_statementt &statement)
{
PRECONDITION(statement.id() == ID_verilog_restrict_property);
binary_exprt::check(statement);
return static_cast<const verilog_restrict_statementt &>(statement);
}

inline verilog_restrict_statementt &
to_verilog_restrict_statement(verilog_statementt &statement)
{
PRECONDITION(statement.id() == ID_verilog_restrict_property);
binary_exprt::check(statement);
return static_cast<verilog_restrict_statementt &>(statement);
}

class verilog_module_sourcet : public irept
{
public:
Expand Down
1 change: 1 addition & 0 deletions src/verilog/verilog_interfaces.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -267,6 +267,7 @@ void verilog_typecheckt::interface_module_item(
else if(
module_item.id() == ID_verilog_assert_property ||
module_item.id() == ID_verilog_assume_property ||
module_item.id() == ID_verilog_restrict_property ||
module_item.id() == ID_verilog_cover_property)
{
// done later
Expand Down
14 changes: 11 additions & 3 deletions src/verilog/verilog_synthesis.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2561,6 +2561,7 @@ void verilog_synthesist::synth_assert_assume_cover(
// mark 'assume' and 'cover' properties as such
if(
statement.id() == ID_verilog_assume_property ||
statement.id() == ID_verilog_restrict_property ||
statement.id() == ID_verilog_immediate_assume ||
statement.id() == ID_verilog_smv_assume)
{
Expand Down Expand Up @@ -2616,6 +2617,7 @@ void verilog_synthesist::synth_assert_assume_cover(
// mark 'assume' and 'cover' properties as such
if(
statement.id() == ID_verilog_assume_property ||
statement.id() == ID_verilog_restrict_property ||
statement.id() == ID_verilog_immediate_assume ||
statement.id() == ID_verilog_smv_assume)
{
Expand Down Expand Up @@ -2654,7 +2656,8 @@ void verilog_synthesist::synth_assert_assume_cover(

if(
module_item.id() == ID_verilog_assert_property ||
module_item.id() == ID_verilog_assume_property)
module_item.id() == ID_verilog_assume_property ||
module_item.id() == ID_verilog_restrict_property)
{
// Concurrent assertions and assumptions come with an implicit 'always'
// (1800-2017 Sec 16.12.11).
Expand All @@ -2681,7 +2684,9 @@ void verilog_synthesist::synth_assert_assume_cover(
if(cond.id() != ID_sva_always)
cond = sva_always_exprt{cond};
}
else if(module_item.id() == ID_verilog_assume_property)
else if(
module_item.id() == ID_verilog_assume_property ||
module_item.id() == ID_verilog_restrict_property)
{
// Concurrent assumptions come with an implicit 'always'
// (1800-2017 Sec 16.12.11).
Expand Down Expand Up @@ -3427,6 +3432,7 @@ void verilog_synthesist::synth_statement(
else if(
statement.id() == ID_verilog_immediate_assume ||
statement.id() == ID_verilog_assume_property ||
statement.id() == ID_verilog_restrict_property ||
statement.id() == ID_verilog_smv_assume)
{
synth_assert_assume_cover(
Expand Down Expand Up @@ -3537,7 +3543,9 @@ void verilog_synthesist::synth_module_item(
synth_assert_assume_cover(
to_verilog_assert_assume_cover_module_item(module_item));
}
else if(module_item.id() == ID_verilog_assume_property)
else if(
module_item.id() == ID_verilog_assume_property ||
module_item.id() == ID_verilog_restrict_property)
{
synth_assert_assume_cover(
to_verilog_assert_assume_cover_module_item(module_item));
Expand Down
3 changes: 3 additions & 0 deletions src/verilog/verilog_typecheck.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1484,6 +1484,7 @@ void verilog_typecheckt::convert_statement(
else if(
statement.id() == ID_verilog_immediate_assume ||
statement.id() == ID_verilog_assume_property ||
statement.id() == ID_verilog_restrict_property ||
statement.id() == ID_verilog_smv_assume)
{
convert_assert_assume_cover(to_verilog_assume_statement(statement));
Expand Down Expand Up @@ -1531,6 +1532,7 @@ void verilog_typecheckt::convert_statement(
if(
sub_statement.id() == ID_verilog_assert_property ||
sub_statement.id() == ID_verilog_assume_property ||
sub_statement.id() == ID_verilog_restrict_property ||
sub_statement.id() == ID_verilog_cover_property)
{
sub_statement.set(ID_identifier, label_statement.label());
Expand Down Expand Up @@ -1587,6 +1589,7 @@ void verilog_typecheckt::convert_module_item(
else if(
module_item.id() == ID_verilog_assert_property ||
module_item.id() == ID_verilog_assume_property ||
module_item.id() == ID_verilog_restrict_property ||
module_item.id() == ID_verilog_cover_property)
{
convert_assert_assume_cover(
Expand Down