Merge pull request #558 from diffblue/verilog_expect_property

SystemVerilog: grammar for expect property

Author: tautschnig

regression/verilog/SVA/expect1.desc

@@ -0,0 +1,9 @@
+CORE
+expect1.sv
+
+^file expect1.sv line \d+: synthesis of expect property not supported$
+^EXIT=2$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/SVA/expect1.sv

@@ -0,0 +1,8 @@
+module main;
+
+  reg [31:0] x;
+  wire clk;
+
+  initial expect (x==0);
+
+endmodule

src/hw_cbmc_irep_ids.h

@@ -101,6 +101,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_expect_property)
 IREP_ID_ONE(verilog_smv_assert)
 IREP_ID_ONE(verilog_smv_assume)
 IREP_ID_ONE(verilog_always)

src/verilog/parser.y

@@ -2030,6 +2030,10 @@ cover_property_statement: TOK_COVER TOK_PROPERTY '(' property_spec ')' action_bl
 		{ init($$, ID_verilog_cover_property); mto($$, $4); mto($$, $6); }
 	;
 
+expect_property_statement: TOK_EXPECT '(' property_spec ')' action_block
+		{ init($$, ID_verilog_expect_property); mto($$, $3); mto($$, $5); }
+	;
+
 assertion_item_declaration:
 	  property_declaration
 	;
@@ -2876,6 +2880,7 @@ statement_item:
 	| seq_block
 	| wait_statement
 	| procedural_assertion_statement
+	| expect_property_statement
 	;
 
 function_statement: statement

src/verilog/verilog_elaborate.cpp

@@ -620,7 +620,8 @@ 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_cover_property)
+    statement.id() == ID_verilog_cover_property ||
+    statement.id() == ID_verilog_expect_property)
   {
   }
   else if(

src/verilog/verilog_synthesis.cpp

@@ -2952,6 +2952,11 @@ void verilog_synthesist::synth_statement(
     synth_assert_assume_cover(
       to_verilog_assert_assume_cover_statement(statement));
   }
+  else if(statement.id() == ID_verilog_expect_property)
+  {
+    throw errort().with_location(statement.source_location())
+      << "synthesis of expect property not supported";
+  }
   else if(statement.id()==ID_non_blocking_assign)
     synth_assign(statement, false);
   else if(statement.id()==ID_force)

src/verilog/verilog_typecheck.cpp

@@ -1439,6 +1439,9 @@ void verilog_typecheckt::convert_statement(
     convert_assert_assume_cover(
       to_verilog_assert_assume_cover_statement(statement));
   }
+  else if(statement.id() == ID_verilog_expect_property)
+  {
+  }
   else if(
     statement.id() == ID_verilog_immediate_assume ||
     statement.id() == ID_verilog_assume_property ||