From 04d4dbc287e286a8ef5f061dfb065fcb064b2fe6 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 8 Sep 2024 15:46:25 -0700 Subject: [PATCH] SystemVerilog: restrict statement This adds the SystemVerilog restrict statement. --- regression/verilog/SVA/restrict1.desc | 10 +++++++++ regression/verilog/SVA/restrict1.sv | 15 ++++++++++++++ src/hw_cbmc_irep_ids.h | 1 + src/verilog/parser.y | 5 +++++ src/verilog/verilog_elaborate.cpp | 2 ++ src/verilog/verilog_expr.h | 30 +++++++++++++++++++++++++++ src/verilog/verilog_interfaces.cpp | 1 + src/verilog/verilog_synthesis.cpp | 14 ++++++++++--- src/verilog/verilog_typecheck.cpp | 3 +++ 9 files changed, 78 insertions(+), 3 deletions(-) create mode 100644 regression/verilog/SVA/restrict1.desc create mode 100644 regression/verilog/SVA/restrict1.sv diff --git a/regression/verilog/SVA/restrict1.desc b/regression/verilog/SVA/restrict1.desc new file mode 100644 index 000000000..168d20408 --- /dev/null +++ b/regression/verilog/SVA/restrict1.desc @@ -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 +-- diff --git a/regression/verilog/SVA/restrict1.sv b/regression/verilog/SVA/restrict1.sv new file mode 100644 index 000000000..2c8338a7a --- /dev/null +++ b/regression/verilog/SVA/restrict1.sv @@ -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 diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h index 5839c0b1a..c8343a7a0 100644 --- a/src/hw_cbmc_irep_ids.h +++ b/src/hw_cbmc_irep_ids.h @@ -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) diff --git a/src/verilog/parser.y b/src/verilog/parser.y index b4682e493..c87acbd2c 100644 --- a/src/verilog/parser.y +++ b/src/verilog/parser.y @@ -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 */ @@ -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); } ; diff --git a/src/verilog/verilog_elaborate.cpp b/src/verilog/verilog_elaborate.cpp index b5119f6f1..45528face 100644 --- a/src/verilog/verilog_elaborate.cpp +++ b/src/verilog/verilog_elaborate.cpp @@ -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) { @@ -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) { } diff --git a/src/verilog/verilog_expr.h b/src/verilog/verilog_expr.h index fb62cdaa9..3c93a54e3 100644 --- a/src/verilog/verilog_expr.h +++ b/src/verilog/verilog_expr.h @@ -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( @@ -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(module_item); @@ -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); @@ -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); @@ -1980,6 +1984,32 @@ to_verilog_assume_statement(verilog_statementt &statement) return static_cast(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(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(statement); +} + class verilog_module_sourcet : public irept { public: diff --git a/src/verilog/verilog_interfaces.cpp b/src/verilog/verilog_interfaces.cpp index ce70d35bb..2cd7a5a43 100644 --- a/src/verilog/verilog_interfaces.cpp +++ b/src/verilog/verilog_interfaces.cpp @@ -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 diff --git a/src/verilog/verilog_synthesis.cpp b/src/verilog/verilog_synthesis.cpp index 0af39d168..2b997afd1 100644 --- a/src/verilog/verilog_synthesis.cpp +++ b/src/verilog/verilog_synthesis.cpp @@ -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) { @@ -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) { @@ -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). @@ -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). @@ -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( @@ -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)); diff --git a/src/verilog/verilog_typecheck.cpp b/src/verilog/verilog_typecheck.cpp index bbf5d2594..76e939740 100644 --- a/src/verilog/verilog_typecheck.cpp +++ b/src/verilog/verilog_typecheck.cpp @@ -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)); @@ -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()); @@ -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(