Merge pull request #511 from diffblue/sva_sequence_operators

tautschnig · web-flow · commit e6f106054d62 · 2024-05-19T13:23:46.000+03:00
SystemVerilog: error for unsupported sequence operators
diff --git a/regression/verilog/SVA/sequence_first_match1.desc b/regression/verilog/SVA/sequence_first_match1.desc
@@ -0,0 +1,9 @@
+CORE
+sequence_first_match1.sv
+
+^file .* line \d+: no support for 'first_match'$
+^EXIT=2$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/verilog/SVA/sequence_first_match1.sv b/regression/verilog/SVA/sequence_first_match1.sv
@@ -0,0 +1,10 @@
+module main(input clk);
+
+  reg [31:0] x = 0;
+
+  always @(posedge clk)
+    x<=x+1;
+
+  initial p0: assert property (first_match(x == 0));
+
+endmodule
diff --git a/regression/verilog/SVA/sequence_intersect1.desc b/regression/verilog/SVA/sequence_intersect1.desc
@@ -0,0 +1,9 @@
+CORE
+sequence_intersect1.sv
+
+^file .* line \d+: no support for 'intersect'$
+^EXIT=2$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/verilog/SVA/sequence_intersect1.sv b/regression/verilog/SVA/sequence_intersect1.sv
@@ -0,0 +1,10 @@
+module main(input clk);
+
+  reg [31:0] x = 0;
+
+  always @(posedge clk)
+    x<=x+1;
+
+  initial p0: assert property (x == 0 intersect x == 1);
+
+endmodule
diff --git a/regression/verilog/SVA/sequence_throughout1.desc b/regression/verilog/SVA/sequence_throughout1.desc
@@ -0,0 +1,9 @@
+CORE
+sequence_throughout1.sv
+
+^file .* line \d+: no support for 'throughout'$
+^EXIT=2$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/verilog/SVA/sequence_throughout1.sv b/regression/verilog/SVA/sequence_throughout1.sv
@@ -0,0 +1,10 @@
+module main(input clk);
+
+  reg [31:0] x = 0;
+
+  always @(posedge clk)
+    x<=x+1;
+
+  initial p0: assert property (x == 0 throughout x == 1);
+
+endmodule
diff --git a/regression/verilog/SVA/sequence_within1.desc b/regression/verilog/SVA/sequence_within1.desc
@@ -0,0 +1,9 @@
+CORE
+sequence_within1.sv
+
+^file .* line \d+: no support for 'within'$
+^EXIT=2$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/verilog/SVA/sequence_within1.sv b/regression/verilog/SVA/sequence_within1.sv
@@ -0,0 +1,10 @@
+module main(input clk);
+
+  reg [31:0] x = 0;
+
+  always @(posedge clk)
+    x<=x+1;
+
+  initial p0: assert property (x == 0 within x == 1);
+
+endmodule
diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h
@@ -16,9 +16,11 @@ IREP_ID_ONE(E)
 IREP_ID_ONE(G)
 IREP_ID_ONE(X)
 IREP_ID_ONE(sva_cycle_delay)
-IREP_ID_ONE(sva_sequence_throughout)
 IREP_ID_ONE(sva_sequence_concatenation)
 IREP_ID_ONE(sva_sequence_first_match)
+IREP_ID_ONE(sva_sequence_intersect)
+IREP_ID_ONE(sva_sequence_throughout)
+IREP_ID_ONE(sva_sequence_within)
 IREP_ID_ONE(sva_always)
 IREP_ID_ONE(sva_ranged_always)
 IREP_ID_ONE(sva_s_always)
diff --git a/src/verilog/expr2verilog.cpp b/src/verilog/expr2verilog.cpp
@@ -440,18 +440,17 @@ Function: expr2verilogt::convert_sva
 
 \*******************************************************************/
 
-std::string expr2verilogt::convert_sva(
-  const exprt &lhs,
+std::string expr2verilogt::convert_sva_binary(
   const std::string &name,
-  const exprt &rhs)
+  const binary_exprt &expr)
 {
   unsigned p0;
-  auto s0 = convert(lhs, p0);
+  auto s0 = convert(expr.lhs(), p0);
   if(p0 == 0)
     s0 = "(" + s0 + ")";
 
   unsigned p1;
-  auto s1 = convert(rhs, p1);
+  auto s1 = convert(expr.rhs(), p1);
   if(p1 == 0)
     s1 = "(" + s1 + ")";
 
@@ -1091,16 +1090,10 @@ std::string expr2verilogt::convert(
     return convert_function("$onehot0", src);
 
   else if(src.id()==ID_sva_overlapped_implication)
-  {
-    auto &binary = to_binary_expr(src);
-    return precedence = 0, convert_sva(binary.lhs(), "|->", binary.rhs());
-  }
+    return precedence = 0, convert_sva_binary("|->", to_binary_expr(src));
 
   else if(src.id()==ID_sva_non_overlapped_implication)
-  {
-    auto &binary = to_binary_expr(src);
-    return precedence = 0, convert_sva(binary.lhs(), "|=>", binary.rhs());
-  }
+    return precedence = 0, convert_sva_binary("|=>", to_binary_expr(src));
 
   else if(src.id()==ID_sva_cycle_delay)
     return convert_sva_cycle_delay(to_ternary_expr(src), precedence = 0);
@@ -1110,7 +1103,24 @@ std::string expr2verilogt::convert(
     return convert_sva_sequence_concatenation(
       to_binary_expr(src), precedence = 0);
     // not sure about precedence
-    
+
+  else if(src.id() == ID_sva_sequence_first_match)
+    return convert_function("first_match", src);
+
+  else if(src.id() == ID_sva_sequence_intersect)
+    return precedence = 0, convert_sva_binary("intersect", to_binary_expr(src));
+  // not sure about precedence
+
+  else if(src.id() == ID_sva_sequence_within)
+    return convert_sva_sequence_concatenation(
+      to_binary_expr(src), precedence = 0);
+  // not sure about precedence
+
+  else if(src.id() == ID_sva_sequence_throughout)
+    return convert_sva_sequence_concatenation(
+      to_binary_expr(src), precedence = 0);
+  // not sure about precedence
+
   else if(src.id()==ID_sva_always)
     return precedence = 0, convert_sva_unary("always", to_sva_always_expr(src));
 
@@ -1151,28 +1161,19 @@ std::string expr2verilogt::convert(
            convert_sva_unary("s_eventually", to_sva_s_eventually_expr(src));
 
   else if(src.id()==ID_sva_until)
-    return precedence = 0, convert_sva(
-                             to_sva_until_expr(src).lhs(),
-                             "until",
-                             to_sva_until_expr(src).rhs());
+    return precedence = 0, convert_sva_binary("until", to_sva_until_expr(src));
 
   else if(src.id()==ID_sva_s_until)
-    return precedence = 0, convert_sva(
-                             to_sva_s_until_expr(src).lhs(),
-                             "s_until",
-                             to_sva_s_until_expr(src).rhs());
+    return precedence = 0,
+           convert_sva_binary("s_until", to_sva_s_until_expr(src));
 
   else if(src.id()==ID_sva_until_with)
-    return precedence = 0, convert_sva(
-                             to_sva_until_with_expr(src).lhs(),
-                             "until_with",
-                             to_sva_until_with_expr(src).rhs());
+    return precedence = 0,
+           convert_sva_binary("until_with", to_sva_until_with_expr(src));
 
   else if(src.id()==ID_sva_s_until_with)
-    return precedence = 0, convert_sva(
-                             to_sva_s_until_with_expr(src).lhs(),
-                             "s_until_with",
-                             to_sva_s_until_with_expr(src).rhs());
+    return precedence = 0,
+           convert_sva_binary("s_until_with", to_sva_s_until_with_expr(src));
 
   else if(src.id()==ID_function_call)
     return convert_function_call(to_function_call_expr(src));
diff --git a/src/verilog/expr2verilog_class.h b/src/verilog/expr2verilog_class.h
@@ -90,8 +90,7 @@ class expr2verilogt
 
   std::string convert_sva_unary(const std::string &name, const unary_exprt &);
 
-  std::string
-  convert_sva(const exprt &lhs, const std::string &name, const exprt &rhs);
+  std::string convert_sva_binary(const std::string &name, const binary_exprt &);
 
   virtual std::string
   convert_replication(const replication_exprt &, unsigned precedence);
diff --git a/src/verilog/parser.y b/src/verilog/parser.y
@@ -2091,10 +2091,14 @@ sequence_expr:
                 { $$=$1; mto($$, $2); }
         | expression cycle_delay_range sequence_expr
                 { init($$, ID_sva_sequence_concatenation); mto($$, $1); mto($2, $3); mto($$, $2); }
+	| expression "intersect" sequence_expr
+                { init($$, ID_sva_sequence_intersect); mto($$, $1); mto($$, $3); }
         | "first_match" '(' sequence_expr ')'
                 { init($$, ID_sva_sequence_first_match); mto($$, $3); }
         | expression "throughout" sequence_expr
                 { init($$, ID_sva_sequence_throughout); mto($$, $1); mto($$, $3); }
+        | expression "within" sequence_expr
+                { init($$, ID_sva_sequence_within); mto($$, $1); mto($$, $3); }
         ;
 
 cycle_delay_range:
diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp
@@ -1899,6 +1899,11 @@ exprt verilog_typecheck_exprt::convert_unary_expr(unary_exprt expr)
     make_boolean(expr.op());
     expr.type()=bool_typet();
   }
+  else if(expr.id() == ID_sva_sequence_first_match)
+  {
+    throw errort().with_location(expr.source_location())
+      << "no support for 'first_match'";
+  }
   else if(expr.id() == ID_verilog_explicit_cast)
   {
     // SystemVerilog has got type'(expr). This is an explicit
@@ -2231,6 +2236,21 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr)
 
     return std::move(expr);
   }
+  else if(expr.id() == ID_sva_sequence_intersect)
+  {
+    throw errort().with_location(expr.source_location())
+      << "no support for 'intersect'";
+  }
+  else if(expr.id() == ID_sva_sequence_throughout)
+  {
+    throw errort().with_location(expr.source_location())
+      << "no support for 'throughout'";
+  }
+  else if(expr.id() == ID_sva_sequence_within)
+  {
+    throw errort().with_location(expr.source_location())
+      << "no support for 'within'";
+  }
   else if(expr.id()==ID_hierarchical_identifier)
   {
     return convert_hierarchical_identifier(
