Merge pull request #1114 from diffblue/sva-to-ltl-and-or

SVA-to-LTL: sequence `and`/`or`

Author: kroening

regression/verilog/SVA/sequence_and2.bdd.desc

@@ -0,0 +1,11 @@
+CORE
+sequence_and2.sv
+--bdd
+\[.*\] \(1 and \(##2 1\)\) \|-> main\.x == 2: FAILURE: property not supported by BDD engine$
+\[.*\] \(\(##2 1\) and 1\) \|-> main\.x == 2: FAILURE: property not supported by BDD engine$
+\[.*\] \(\(##2 1\) and 1\) #-# main\.x == 2: PROVED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/SVA/sequence_and2.desc renamed to regression/verilog/SVA/sequence_and2.bmc.desc

@@ -3,6 +3,7 @@ sequence_and2.sv
 
 \[.*\] \(1 and \(##2 1\)\) \|-> main\.x == 2: PROVED up to bound 5$
 \[.*\] \(\(##2 1\) and 1\) \|-> main\.x == 2: PROVED up to bound 5$
+\[.*\] \(\(##2 1\) and 1\) #-# main\.x == 2: PROVED up to bound 5$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/SVA/sequence_and2.sv

@@ -11,4 +11,6 @@ module main(input clk);
 
   initial p2: assert property ((##2 1 and 1) |-> x == 2);
 
+  initial p3: assert property ((##2 1 and 1) #-# x == 2);
+
 endmodule

regression/verilog/SVA/sequence_or1.bdd.desc

@@ -0,0 +1,12 @@
+CORE
+sequence_or1.sv
+--bdd
+^\[main\.p0\] main\.x == 0 or main\.x == 1: PROVED$
+^\[main\.p1\] strong\(main\.x == 0 or main\.x == 1\): PROVED$
+^\[main\.p2\] main\.x == 0 or \(nexttime main\.x == 1\): FAILURE: property not supported by BDD engine$
+^\[main\.p3\] \(nexttime main\.x == 1\) or main\.x == 1: FAILURE: property not supported by BDD engine$
+^\[main\.p4\] \(main\.x == 0 or main\.x != 10\) |=> main\.x == 1: FAILURE: property not supported by BDD engine$
+^EXIT=10$
+^SIGNAL=0$
+--
+--

regression/verilog/SVA/sequence_or1.desc renamed to regression/verilog/SVA/sequence_or1.bmc.desc

@@ -166,6 +166,63 @@ std::vector<sva_sequence_matcht> LTL_sequence_matches(const exprt &sequence)
     else
       return {};
   }
+  else if(sequence.id() == ID_sva_and)
+  {
+    // IEEE 1800-2017 16.9.5
+    // 1. Both operands must match.
+    // 2. Both sequences start at the same time.
+    // 3. The end time of the composite sequence is
+    //    the end time of the operand sequence that completes last.
+    auto &and_expr = to_sva_and_expr(sequence);
+    auto matches_lhs = LTL_sequence_matches(and_expr.lhs());
+    auto matches_rhs = LTL_sequence_matches(and_expr.rhs());
+
+    if(matches_lhs.empty() || matches_rhs.empty())
+      return {};
+
+    std::vector<sva_sequence_matcht> result;
+
+    for(auto &match_lhs : matches_lhs)
+      for(auto &match_rhs : matches_rhs)
+      {
+        sva_sequence_matcht new_match;
+        auto new_length = std::max(match_lhs.length(), match_rhs.length());
+        new_match.cond_vector.resize(new_length);
+        for(std::size_t i = 0; i < new_length; i++)
+        {
+          exprt::operandst conjuncts;
+          if(i < match_lhs.cond_vector.size())
+            conjuncts.push_back(match_lhs.cond_vector[i]);
+
+          if(i < match_rhs.cond_vector.size())
+            conjuncts.push_back(match_rhs.cond_vector[i]);
+
+          new_match.cond_vector[i] = conjunction(conjuncts);
+        }
+
+        result.push_back(std::move(new_match));
+      }
+
+    return result;
+  }
+  else if(sequence.id() == ID_sva_or)
+  {
+    // IEEE 1800-2017 16.9.7
+    // The set of matches of a or b is the set union of the matches of a
+    // and the matches of b.
+    std::vector<sva_sequence_matcht> result;
+
+    for(auto &op : to_sva_or_expr(sequence).operands())
+    {
+      auto op_matches = LTL_sequence_matches(op);
+      if(op_matches.empty())
+        return {}; // not supported
+      for(auto &match : op_matches)
+        result.push_back(std::move(match));
+    }
+
+    return result;
+  }
   else
   {
     return {}; // unsupported