Merge pull request #1169 from diffblue/sva-sequence-methods

SVA: `sequence()` methods for first_match and throughout

Author: tautschnig

src/trans-word-level/sequence.cpp

@@ -220,14 +220,14 @@ sequence_matchest instantiate_sequence(
   {
     auto &first_match = to_sva_sequence_first_match_expr(expr);
 
-    const auto lhs_matches =
-      instantiate_sequence(first_match.lhs(), semantics, t, no_timeframes);
+    const auto matches =
+      instantiate_sequence(first_match.sequence(), semantics, t, no_timeframes);
 
     // the match of seq with the earliest ending clock tick is a
     // match of first_match (seq)
     std::optional<mp_integer> earliest;
 
-    for(auto &match : lhs_matches)
+    for(auto &match : matches)
     {
       if(!earliest.has_value() || earliest.value() > match.end_time)
         earliest = match.end_time;
@@ -238,7 +238,7 @@ sequence_matchest instantiate_sequence(
 
     sequence_matchest result;
 
-    for(auto &match : lhs_matches)
+    for(auto &match : matches)
     {
       // Earliest?
       if(match.end_time == earliest.value())
@@ -257,23 +257,23 @@ sequence_matchest instantiate_sequence(
     // - exp evaluates to true at each clock tick of the interval.
     auto &throughout = to_sva_sequence_throughout_expr(expr);
 
-    const auto rhs_matches =
-      instantiate_sequence(throughout.rhs(), semantics, t, no_timeframes);
+    const auto matches =
+      instantiate_sequence(throughout.sequence(), semantics, t, no_timeframes);
 
     sequence_matchest result;
 
-    for(auto &rhs_match : rhs_matches)
+    for(auto &match : matches)
     {
-      exprt::operandst conjuncts = {rhs_match.condition()};
+      exprt::operandst conjuncts = {match.condition()};
 
-      for(mp_integer new_t = t; new_t <= rhs_match.end_time; ++new_t)
+      for(mp_integer new_t = t; new_t <= match.end_time; ++new_t)
       {
         auto obligations =
           property_obligations(throughout.lhs(), new_t, no_timeframes);
         conjuncts.push_back(obligations.conjunction().second);
       }
 
-      result.emplace_back(rhs_match.end_time, conjunction(conjuncts));
+      result.emplace_back(match.end_time, conjunction(conjuncts));
     }
 
     return result;

src/verilog/sva_expr.h

@@ -1746,6 +1746,16 @@ class sva_sequence_throughout_exprt : public binary_exprt
     : binary_exprt(std::move(op0), ID_sva_sequence_throughout, std::move(op1))
   {
   }
+
+  const exprt &sequence() const
+  {
+    return op1();
+  }
+
+  exprt &sequence()
+  {
+    return op1();
+  }
 };
 
 static inline const sva_sequence_throughout_exprt &
@@ -1780,6 +1790,16 @@ class sva_sequence_first_match_exprt : public binary_exprt
         std::move(action))
   {
   }
+
+  const exprt &sequence() const
+  {
+    return op0();
+  }
+
+  exprt &sequence()
+  {
+    return op0();
+  }
 };
 
 static inline const sva_sequence_first_match_exprt &

src/verilog/verilog_typecheck_sva.cpp

@@ -264,8 +264,8 @@ exprt verilog_typecheck_exprt::convert_binary_sva(binary_exprt expr)
   {
     auto &first_match_expr = to_sva_sequence_first_match_expr(expr);
 
-    convert_sva(first_match_expr.lhs());
-    require_sva_sequence(first_match_expr.lhs());
+    convert_sva(first_match_expr.sequence());
+    require_sva_sequence(first_match_expr.sequence());
 
     if(first_match_expr.rhs().is_not_nil())
       convert_expr(first_match_expr.rhs());