Merge pull request #226 from diffblue/fix-lasso

ebmc: fix encoding of 'eventually'

Author: kroening

regression/verilog/system_verilog_assertion/eventually2.desc

@@ -0,0 +1,7 @@
+CORE
+eventually2.sv
+--module main --bound 20
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/verilog/system_verilog_assertion/eventually2.sv

@@ -0,0 +1,18 @@
+// count up from 0 to 10, with option to reset
+
+module main(input clk, input reset);
+
+  reg [7:0] counter;
+
+  initial counter = 0;
+
+  always @(posedge clk)
+    if(reset)
+      counter = 0;
+    else if(counter != 10)
+      counter = counter + 1;
+
+  // expected to pass for any bound
+  p0: assert property (eventually (reset || counter == 10));
+
+endmodule

regression/verilog/system_verilog_assertion/eventually3.desc

@@ -0,0 +1,8 @@
+CORE
+eventually3.sv
+--module main --bound 11
+^EXIT=10$
+^SIGNAL=0$
+^\[main\.property\.p0\] always \(eventually main\.counter <= 5\): FAILURE$
+--
+^warning: ignoring

regression/verilog/system_verilog_assertion/eventually3.sv

@@ -0,0 +1,16 @@
+module main(input clk);
+
+  reg [7:0] counter;
+
+  initial counter = 0;
+
+  always @(posedge clk)
+    if(counter < 10)
+      counter = counter + 1;
+    else
+      counter = 6;
+
+  // expected to fail with any bound greater or equal 11
+  p0: assert property (eventually counter<=5);
+
+endmodule

src/trans-word-level/instantiate_word_level.cpp

@@ -266,32 +266,36 @@ void wl_instantiatet::instantiate_rec(exprt &expr)
 
     // The following needs to be satisfied for a counterexample
     // to Fp:
-    // (1) No state up to the current state satisfies 'p'.
-    // (2) The current state is equal to some earlier state.
+    // (1) There is a loop from the current state i back to
+    //     some earlier state k < i.
+    // (1) No state j with k<=k<=i on the lasso satisfies 'p'.
     //
     // We look backwards instead of forwards so that 'current'
     // is the last state of the counterexample trace.
+    //
+    // Note that this is trivially true when current is zero,
+    // as a single state cannot demonstrate the loop.
 
-    if(current == 0)
-    {
-      // there is no counterexample to Fp with just one state
-      expr = true_exprt();
-    }
-    else
-    {
-      exprt::operandst conjuncts = {lasso_symbol(current)};
+    exprt::operandst conjuncts = {};
+    const std::size_t i = current;
 
-      // save the current time frame, we'll change it
-      save_currentt save_current(current);
+    for(std::size_t k = 0; k < i; k++)
+    {
+      exprt::operandst disjuncts = {not_exprt(lasso_symbol(k, i))};
 
-      for(; current<no_timeframes; current++)
+      for(std::size_t j = k; j <= i; j++)
       {
-        conjuncts.push_back(not_exprt(p));
-        instantiate_rec(conjuncts.back());
+        // save the current time frame, we'll change it
+        save_currentt save_current(current);
+        current = j;
+        disjuncts.push_back(p);
+        instantiate_rec(disjuncts.back());
       }
 
-      expr = not_exprt(conjunction(conjuncts));
+      conjuncts.push_back(disjunction(disjuncts));
     }
+
+    expr = conjunction(conjuncts);
   }
   else if(expr.id()==ID_sva_until ||
           expr.id()==ID_sva_s_until)

src/trans-word-level/property.cpp

@@ -78,10 +78,13 @@ Function: states_equal
 \*******************************************************************/
 
 exprt states_equal(
-  std::size_t i,
   std::size_t k,
+  std::size_t i,
   const std::vector<symbol_exprt> &variables_to_compare)
 {
+  // We require k<i to avoid the symmetric constraints.
+  PRECONDITION(k < i);
+
   exprt::operandst conjuncts;
   conjuncts.reserve(variables_to_compare.size());
 
@@ -107,9 +110,13 @@ Function: lasso_symbol
 
 \*******************************************************************/
 
-symbol_exprt lasso_symbol(std::size_t timeframe)
+symbol_exprt lasso_symbol(std::size_t k, std::size_t i)
 {
-  irep_idt lasso_identifier = "lasso::" + std::to_string(timeframe);
+  // True when states i and k are equal.
+  // We require k<i to avoid the symmetric constraints.
+  PRECONDITION(k < i);
+  irep_idt lasso_identifier =
+    "lasso::" + std::to_string(i) + "-back-to-" + std::to_string(k);
   return symbol_exprt(lasso_identifier, bool_typet());
 }
 
@@ -135,10 +142,10 @@ void lasso_constraints(
   // is an identical state s_k = s_i with k<i.
   // "Identical" is defined as "state variables and top-level inputs match".
 
-  // gather the state variables
   std::vector<symbol_exprt> variables_to_compare;
-  const symbol_tablet &symbol_table = ns.get_symbol_table();
 
+  // Gather the state variables.
+  const symbol_tablet &symbol_table = ns.get_symbol_table();
   auto lower = symbol_table.symbol_module_map.lower_bound(module_identifier);
   auto upper = symbol_table.symbol_module_map.upper_bound(module_identifier);
 
@@ -168,15 +175,13 @@ void lasso_constraints(
 
   for(std::size_t i = 1; i < no_timeframes; i++)
   {
-    // Is there a loop back to any time frame k with k<i?
-    exprt::operandst disjuncts;
-    disjuncts.reserve(i);
-
     for(std::size_t k = 0; k < i; k++)
-      disjuncts.push_back(states_equal(k, i, variables_to_compare));
-
-    auto lasso_symbol = ::lasso_symbol(i);
-    solver.set_to_true(equal_exprt(lasso_symbol, disjunction(disjuncts)));
+    {
+      // Is there a loop back from time frame i back to time frame k?
+      auto lasso_symbol = ::lasso_symbol(k, i);
+      auto equal = states_equal(k, i, variables_to_compare);
+      solver.set_to_true(equal_exprt(lasso_symbol, equal));
+    }
   }
 }
 

src/trans-word-level/property.h

@@ -31,7 +31,9 @@ void lasso_constraints(
   const namespacet &,
   const irep_idt &module_identifier);
 
-symbol_exprt lasso_symbol(std::size_t);
+/// Is there a loop from i back to k?
+/// Precondition: k<i
+symbol_exprt lasso_symbol(std::size_t k, std::size_t i);
 
 /// Returns true iff the given property requires lasso constraints.
 bool requires_lasso_constraints(const exprt &);