SystemVerilog: restrict statement

kroening · kroening · commit 04d4dbc287e2 · 2024-09-09T18:39:40.000-07:00
This adds the SystemVerilog restrict statement.
diff --git a/regression/verilog/SVA/restrict1.desc 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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 &>(
@@ -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);
@@ -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<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:
diff --git 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
@@ -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
@@ -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(

Original file line number	Diff line number	Diff line change
`@@ -2022,6 +2022,7 @@ concurrent_assertion_statement:`
`2022`	`2022`	`assert_property_statement`
`2023`	`2023`	`\| assume_property_statement`
`2024`	`2024`	`\| cover_property_statement`
	`2025`	`+ \| restrict_property_statement`
`2025`	`2026`	`;`
`2026`	`2027`
`2027`	`2028`	`/* This one mimicks functionality in Cadence SMV */`
`@@ -2083,6 +2084,10 @@ cover_property_statement: TOK_COVER TOK_PROPERTY '(' property_spec ')' action_bl`
`2083`	`2084`	`{ init($$, ID_verilog_cover_property); mto($$, $4); mto($$, $6); }`
`2084`	`2085`	`;`
`2085`	`2086`
	`2087`	`+restrict_property_statement: TOK_RESTRICT TOK_PROPERTY '(' property_spec ')' ';'`
	`2088`	`+ { init($$, ID_verilog_restrict_property); mto($$, $4); mto($$, $6); }`
	`2089`	`+ ;`
	`2090`	`+`
`2086`	`2091`	`expect_property_statement: TOK_EXPECT '(' property_spec ')' action_block`
`2087`	`2092`	`{ init($$, ID_verilog_expect_property); mto($$, $3); mto($$, $5); }`
`2088`	`2093`	`;`
Original file line number	Diff line number	Diff line change
`@@ -630,6 +630,7 @@ void verilog_typecheckt::collect_symbols(const verilog_statementt &statement)`
`630`	`630`	`else if(`
`631`	`631`	`statement.id() == ID_verilog_assert_property \|\|`
`632`	`632`	`statement.id() == ID_verilog_assume_property \|\|`
	`633`	`+ statement.id() == ID_verilog_restrict_property \|\|`
`633`	`634`	`statement.id() == ID_verilog_cover_property \|\|`
`634`	`635`	`statement.id() == ID_verilog_expect_property)`
`635`	`636`	`{`
`@@ -791,6 +792,7 @@ void verilog_typecheckt::collect_symbols(`
`791`	`792`	`else if(`
`792`	`793`	`module_item.id() == ID_verilog_assert_property \|\|`
`793`	`794`	`module_item.id() == ID_verilog_assume_property \|\|`
	`795`	`+ module_item.id() == ID_verilog_restrict_property \|\|`
`794`	`796`	`module_item.id() == ID_verilog_cover_property)`
`795`	`797`	`{`
`796`	`798`	`}`
Original file line number	Diff line number	Diff line change
`@@ -267,6 +267,7 @@ void verilog_typecheckt::interface_module_item(`
`267`	`267`	`else if(`
`268`	`268`	`module_item.id() == ID_verilog_assert_property \|\|`
`269`	`269`	`module_item.id() == ID_verilog_assume_property \|\|`
	`270`	`+ module_item.id() == ID_verilog_restrict_property \|\|`
`270`	`271`	`module_item.id() == ID_verilog_cover_property)`
`271`	`272`	`{`
`272`	`273`	`// done later`