SystemVerilog: named sequences

CHANGELOG

@@ -6,6 +6,7 @@
 * BMC: support SVA sequence intersect
 * SystemVerilog: streaming concatenation {<<{...}} and {>>{...}}
 * SystemVerilog: set membership operator
+* SystemVerilog: named sequences
 
 # EBMC 5.3
 

regression/verilog/SVA/named_sequence1.desc

@@ -0,0 +1,9 @@
+CORE
+named_sequence1.sv
+--bound 0
+^\[main\.assert\.1\] always main\.x_is_ten: PROVED up to bound 0$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/SVA/named_sequence1.sv

@@ -0,0 +1,16 @@
+module main(input clk);
+
+  wire [31:0] x = 10;
+
+  sequence x_is_ten;
+    x == 10 ##1 x >= 0
+  endsequence : x_is_ten
+
+  assert property (x_is_ten);
+
+  sequence x_is_twenty;
+    // the ; is optional
+    x == 20;
+  endsequence : x_is_twenty
+
+endmodule

src/hw_cbmc_irep_ids.h

@@ -96,6 +96,7 @@ IREP_ID_ONE(verilog_indexed_part_select_plus)
 IREP_ID_ONE(verilog_indexed_part_select_minus)
 IREP_ID_ONE(verilog_past)
 IREP_ID_ONE(verilog_property_declaration)
+IREP_ID_ONE(verilog_sequence_declaration)
 IREP_ID_ONE(verilog_value_range)
 IREP_ID_ONE(verilog_void)
 IREP_ID_ONE(verilog_streaming_concatenation_left_to_right)

src/verilog/parser.y

@@ -2245,11 +2245,12 @@ expect_property_statement: TOK_EXPECT '(' property_spec ')' action_block
 
 assertion_item_declaration:
 	  property_declaration
+	| sequence_declaration
 	;
 
 property_declaration:
           TOK_PROPERTY property_identifier property_port_list_paren_opt ';'
-          property_spec
+          property_spec semicolon_opt
           TOK_ENDPROPERTY property_identifier_opt
 		{ init($$, ID_verilog_property_declaration);
 		  stack_expr($$).set(ID_base_name, stack_expr($2).id());
@@ -2386,6 +2387,47 @@ property_case_item:
 		{ init($$, ID_case_item); mto($$, $3); }
 	;
 
+sequence_declaration:
+	  "sequence" { init($$, ID_verilog_sequence_declaration); }
+	  sequence_identifier sequence_port_list_opt ';'
+	  sequence_expr semicolon_opt
+	  "endsequence" sequence_identifier_opt
+		{ $$=$2;
+		  stack_expr($$).set(ID_base_name, stack_expr($3).id());
+		  mto($$, $6);
+		}
+	;
+
+sequence_port_list_opt:
+	  /* Optional */
+		{ init($$); }
+	| '(' ')'
+		{ init($$); }
+	| '(' sequence_port_list ')'
+		{ $$=$2; }
+	;
+
+sequence_port_list:
+	  sequence_port_item
+		{ init($$); mto($$, $1); }
+	| sequence_port_list sequence_port_item
+		{ $$=$1; mto($$, $2); }
+	;
+
+sequence_port_item:
+	  formal_port_identifier
+	;
+
+sequence_identifier_opt:
+	  /* Optional */
+	| TOK_COLON sequence_identifier
+	;
+
+semicolon_opt:
+	  /* Optional */
+	| ';'
+	;
+
 expression_or_dist_brace:
 	  expression_or_dist
 		{ init($$, "patterns"); mto($$, $1); }
@@ -4190,6 +4232,8 @@ identifier: non_type_identifier;
 
 property_identifier: TOK_NON_TYPE_IDENTIFIER;
 
+sequence_identifier: TOK_NON_TYPE_IDENTIFIER;
+
 variable_identifier: identifier;
 
 %%

src/verilog/verilog_elaborate.cpp

@@ -118,6 +118,11 @@ void verilog_typecheckt::collect_symbols(
 {
 }
 
+void verilog_typecheckt::collect_symbols(
+  const verilog_sequence_declarationt &declaration)
+{
+}
+
 void verilog_typecheckt::collect_symbols(const typet &type)
 {
   // These types are not yet converted.
@@ -834,6 +839,10 @@ void verilog_typecheckt::collect_symbols(
   {
     collect_symbols(to_verilog_property_declaration(module_item));
   }
+  else if(module_item.id() == ID_verilog_sequence_declaration)
+  {
+    collect_symbols(to_verilog_sequence_declaration(module_item));
+  }
   else
     DATA_INVARIANT(false, "unexpected module item: " + module_item.id_string());
 }

src/verilog/verilog_expr.h

@@ -2620,6 +2620,44 @@ to_verilog_property_declaration(exprt &expr)
   return static_cast<verilog_property_declarationt &>(expr);
 }
 
+class verilog_sequence_declarationt : public verilog_module_itemt
+{
+public:
+  explicit verilog_sequence_declarationt(exprt sequence)
+  {
+    add_to_operands(std::move(sequence));
+  }
+
+  const irep_idt &base_name() const
+  {
+    return get(ID_base_name);
+  }
+
+  const exprt &sequence() const
+  {
+    return op0();
+  }
+
+  exprt &sequence()
+  {
+    return op0();
+  }
+};
+
+inline const verilog_sequence_declarationt &
+to_verilog_sequence_declaration(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_verilog_sequence_declaration);
+  return static_cast<const verilog_sequence_declarationt &>(expr);
+}
+
+inline verilog_sequence_declarationt &
+to_verilog_sequence_declaration(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_verilog_sequence_declaration);
+  return static_cast<verilog_sequence_declarationt &>(expr);
+}
+
 class verilog_streaming_concatenation_exprt : public exprt
 {
 public:

src/verilog/verilog_interfaces.cpp

@@ -306,6 +306,9 @@ void verilog_typecheckt::interface_module_item(
   else if(module_item.id() == ID_verilog_property_declaration)
   {
   }
+  else if(module_item.id() == ID_verilog_sequence_declaration)
+  {
+  }
   else
   {
     DATA_INVARIANT(false, "unexpected module item: " + module_item.id_string());

src/verilog/verilog_synthesis.cpp

@@ -3290,6 +3290,9 @@ void verilog_synthesist::synth_module_item(
   else if(module_item.id() == ID_verilog_property_declaration)
   {
   }
+  else if(module_item.id() == ID_verilog_sequence_declaration)
+  {
+  }
   else
   {
     throw errort().with_location(module_item.source_location())

src/verilog/verilog_typecheck.cpp

@@ -1699,6 +1699,10 @@ void verilog_typecheckt::convert_module_item(
   {
     convert_property_declaration(to_verilog_property_declaration(module_item));
   }
+  else if(module_item.id() == ID_verilog_sequence_declaration)
+  {
+    convert_sequence_declaration(to_verilog_sequence_declaration(module_item));
+  }
   else
   {
     throw errort().with_location(module_item.source_location())
@@ -1743,6 +1747,40 @@ void verilog_typecheckt::convert_property_declaration(
 
 /*******************************************************************\
 
+Function: verilog_typecheckt::convert_sequence_declaration
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void verilog_typecheckt::convert_sequence_declaration(
+  verilog_sequence_declarationt &declaration)
+{
+  auto base_name = declaration.base_name();
+  auto full_identifier = hierarchical_identifier(base_name);
+
+  convert_sva(declaration.sequence());
+
+  auto type = bool_typet{};
+  type.set(ID_C_verilog_type, ID_verilog_sequence_declaration);
+  symbolt symbol{full_identifier, type, mode};
+
+  symbol.module = module_identifier;
+  symbol.base_name = base_name;
+  symbol.pretty_name = strip_verilog_prefix(symbol.name);
+  symbol.is_macro = true;
+  symbol.value = declaration.sequence();
+  symbol.location = declaration.source_location();
+
+  add_symbol(std::move(symbol));
+}
+
+/*******************************************************************\
+
 Function: verilog_typecheckt::convert_statements
 
   Inputs:

src/verilog/verilog_typecheck.h

@@ -106,6 +106,7 @@ class verilog_typecheckt:
   void collect_symbols(const verilog_lett &);
   void collect_symbols(const verilog_statementt &);
   void collect_symbols(const verilog_property_declarationt &);
+  void collect_symbols(const verilog_sequence_declarationt &);
   void
   collect_symbols(const typet &, const verilog_parameter_declt::declaratort &);
   void collect_port_symbols(const verilog_declt &);
@@ -187,6 +188,7 @@ class verilog_typecheckt:
   void convert_module_item(class verilog_module_itemt &);
   void convert_parameter_override(const class verilog_parameter_overridet &);
   void convert_property_declaration(class verilog_property_declarationt &);
+  void convert_sequence_declaration(class verilog_sequence_declarationt &);
 
   void integer_expr(exprt &expr);