Merge pull request #844 from diffblue/instrument_past

Instrumentation for `$past`

CHANGELOG

@@ -2,6 +2,7 @@
 
 * Verilog: bugfix for $onehot0
 * Verilog: fix for primitive gates with more than two inputs
+* Verilog: Support $past when using AIG-based engines
 
 # EBMC 5.4
 

regression/verilog/system-functions/past-instrumentation1.desc

@@ -0,0 +1,8 @@
+CORE
+past-instrumentation1.sv
+--bound 10 --aig
+^\[.*\] always main\.counter >= 1 -> \$past\(main\.counter, 1\) == main\.counter - 1: PROVED up to bound 10$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/verilog/system-functions/past-instrumentation1.sv

@@ -0,0 +1,18 @@
+module main(input clk);
+
+  reg [31:0] counter = 0;
+
+  always @(posedge clk)
+    counter++;
+
+  assert property ($past(counter, 0) == counter);
+
+  assert property (counter >= 1 -> $past(counter, 1) == counter - 1);
+
+  assert property (counter >= 2 -> $past(counter, 2) == counter - 2);
+
+  assert property (counter == 0 -> $past(counter, 1) == 0);
+
+  assert property (counter == 1 -> $past(counter, 2) == 0);
+
+endmodule

regression/verilog/system-functions/past-instrumentation2.desc

@@ -0,0 +1,12 @@
+CORE
+past-instrumentation2.sv
+--bdd
+\[main\.assert\.1\] always \$past\(main\.counter, 0\) == main\.counter: PROVED$
+\[main\.assert\.2\] always main\.counter >= 1 -> \$past\(main\.counter, 1\) == main\.counter - 1: PROVED$
+\[main\.assert\.3\] always main\.counter >= 2 -> \$past\(main\.counter, 2\) == main\.counter - 2: PROVED$
+\[main\.assert\.4\] always main\.counter == 0 -> \$past\(main\.counter, 1\) == 0: REFUTED$
+\[main\.assert\.5\] always main\.counter == 1 -> \$past\(main\.counter, 2\) == 0: REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/verilog/system-functions/past-instrumentation2.sv

@@ -0,0 +1,20 @@
+module main(input clk);
+
+  reg [3:0] counter = 0;
+
+  always @(posedge clk)
+    counter++;
+
+  assert property ($past(counter, 0) == counter);
+
+  assert property (counter >= 1 -> $past(counter, 1) == counter - 1);
+
+  assert property (counter >= 2 -> $past(counter, 2) == counter - 2);
+
+  // expected to fail -- the counter can wrap around
+  assert property (counter == 0 -> $past(counter, 1) == 0);
+
+  // expected to fail -- the counter can wrap around
+  assert property (counter == 1 -> $past(counter, 2) == 0);
+
+endmodule

regression/verilog/system-functions/past-instrumentation3.desc

@@ -0,0 +1,8 @@
+CORE
+past-instrumentation3.sv
+--bdd
+\[.*\] always main\.counter >= 2 -> \$past\(main\.counter, 2\) == main\.counter - 2: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/verilog/system-functions/past-instrumentation3.sv

@@ -0,0 +1,11 @@
+module main(input clk);
+
+  reg [3:0] counter = 0;
+
+  always @(posedge clk)
+    counter++;
+
+  // $past(counter, 1) is deliberately not used
+  assert property (counter >= 2 -> $past(counter, 2) == counter - 2);
+
+endmodule

regression/verilog/system-functions/past2.desc

@@ -1,8 +1,8 @@
 CORE
 past2.sv
 --bdd
-^\[main\.p0\] always \(main\.counter == 0 \|-> \$past\(main\.counter, 1\) == 0\): FAILURE: property not supported by BDD engine$
-^EXIT=10$
+^\[main\.p0\] always \(main\.counter == 0 \|-> \$past\(main\.counter, 1\) == 0\): PROVED$
+^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring

regression/verilog/system-functions/past2.sv

@@ -1,12 +1,12 @@
 module main(input clk);
 
-  reg [31:0] counter = 0;
+  reg [3:0] counter = 0;
 
   always @(posedge clk)
     if(counter < 10)
       counter++;
 
   p0: assert property (counter == 0 |-> $past(counter, 1) == 0);
-//  p1: assert property (counter != 0 && counter != 10 |-> $past(counter, 1) == counter - 1);
+  p1: assert property (counter != 0 && counter != 10 |-> $past(counter, 1) == counter - 1);
 
 endmodule

src/ebmc/Makefile

@@ -15,6 +15,7 @@ SRC = \
       ebmc_parse_options.cpp \
       ebmc_properties.cpp \
       ebmc_solver_factory.cpp \
+      instrument_past.cpp \
       k_induction.cpp \
       liveness_to_safety.cpp \
       live_signal.cpp \

src/ebmc/bdd_engine.cpp

@@ -179,13 +179,6 @@ property_checker_resultt bdd_enginet::operator()()
 {
   try
   {
-    for(auto &property : properties.properties)
-    {
-      // no support for $past
-      if(has_subexpr(property.normalized_expr, ID_verilog_past))
-        property.failure("property not supported by BDD engine");
-    }
-
     // any properties left?
     if(!properties.has_unknown_property())
       return property_checker_resultt{properties};

src/ebmc/instrument_past.cpp

@@ -0,0 +1,201 @@
+/*******************************************************************\
+
+Module: $past Instrumentation
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#include "instrument_past.h"
+
+#include <util/arith_tools.h>
+#include <util/expr_iterator.h>
+#include <util/replace_expr.h>
+
+#include <verilog/verilog_expr.h>
+
+#include "ebmc_error.h"
+
+#include <set>
+
+// The set is ordered to get a stable numbering
+using past_sett = std::set<verilog_past_exprt>;
+
+void collect_past(const exprt &expr, past_sett &past_set)
+{
+  for(auto it = expr.depth_begin(); it != expr.depth_end(); ++it)
+  {
+    if(it->id() == ID_verilog_past)
+      past_set.insert(to_verilog_past_expr(*it));
+  }
+}
+
+void collect_past(transition_systemt &transition_system, past_sett &past_set)
+{
+  collect_past(transition_system.trans_expr, past_set);
+}
+
+void collect_past(ebmc_propertiest &properties, past_sett &past_set)
+{
+  for(auto &property : properties.properties)
+  {
+    collect_past(property.normalized_expr, past_set);
+  }
+}
+
+/// Adds missing $past(x, y) when $past(x, z) with z>y exists.
+void complete_past_set(past_sett &past_set)
+{
+  past_sett new_entries;
+
+  for(const auto &past_expr : past_set)
+  {
+    auto ticks_int_opt = numeric_cast<mp_integer>(past_expr.ticks());
+    if(!ticks_int_opt.has_value())
+      throw ebmc_errort() << "$past with non-constant number of ticks";
+
+    for(mp_integer i = 1; i < *ticks_int_opt; ++i)
+    {
+      auto new_past_expr = past_expr;
+      new_past_expr.ticks() = from_integer(i, new_past_expr.ticks().type());
+      new_entries.insert(new_past_expr);
+    }
+  }
+
+  // now merge in the new entries
+  past_set.insert(new_entries.begin(), new_entries.end());
+}
+
+replace_mapt
+model_past(const past_sett &past_set, transition_systemt &transition_system)
+{
+  replace_mapt past_map;
+  std::size_t number = 0;
+
+  for(auto &past_expr : past_set)
+  {
+    auto ticks_int_opt = numeric_cast<mp_integer>(past_expr.ticks());
+    if(!ticks_int_opt.has_value())
+      throw ebmc_errort() << "$past with non-constant number of ticks";
+
+    if(*ticks_int_opt == 0)
+    {
+      past_map[past_expr] = past_expr.what();
+    }
+    else if(*ticks_int_opt >= 1)
+    {
+      // construct a fresh symbol
+      number++;
+      const irep_idt identifier = "ebmc::$past" + std::to_string(number) + "@" +
+                                  integer2string(*ticks_int_opt);
+      const symbol_exprt symbol_expr(identifier, past_expr.type());
+
+      // add to symbol table
+      {
+        symbolt symbol{
+          identifier, past_expr.type(), transition_system.main_symbol->mode};
+        symbol.is_state_var = true;
+        symbol.module = transition_system.main_symbol->module;
+        transition_system.symbol_table.add(std::move(symbol));
+      }
+
+      past_map[past_expr] = symbol_expr;
+    }
+  }
+
+  // Now generate constraints
+  exprt::operandst init_conjuncts;
+
+  for(auto &past_expr : past_set)
+  {
+    auto ticks_int_opt = numeric_cast<mp_integer>(past_expr.ticks());
+    if(!ticks_int_opt.has_value())
+      throw ebmc_errort() << "$past with non-constant number of ticks";
+
+    if(*ticks_int_opt >= 1)
+    {
+      auto symbol_expr = past_map[past_expr];
+
+      // These start with zero
+      init_conjuncts.push_back(
+        equal_exprt{symbol_expr, past_expr.default_value()});
+    }
+  }
+
+  if(!init_conjuncts.empty())
+    transition_system.trans_expr.init() = and_exprt{
+      transition_system.trans_expr.init(), conjunction(init_conjuncts)};
+
+  exprt::operandst trans_conjuncts;
+
+  for(auto &past_expr : past_set)
+  {
+    auto ticks_int_opt = numeric_cast<mp_integer>(past_expr.ticks());
+    if(!ticks_int_opt.has_value())
+      throw ebmc_errort() << "$past with non-constant number of ticks";
+
+    if(*ticks_int_opt >= 1)
+    {
+      auto symbol_expr = past_map[past_expr];
+
+      exprt next_symbol_expr = to_symbol_expr(symbol_expr);
+      next_symbol_expr.id(ID_next_symbol);
+
+      exprt rhs;
+
+      if(*ticks_int_opt == 1)
+        rhs = past_expr.what();
+      else
+      {
+        auto new_past_expr = past_expr;
+        new_past_expr.ticks() =
+          from_integer(*ticks_int_opt - 1, new_past_expr.ticks().type());
+        // Must be in map, guaranteed by complete_past_set
+        auto map_entry = past_map.find(new_past_expr);
+        CHECK_RETURN(map_entry != past_map.end());
+        rhs = map_entry->second;
+      }
+
+      trans_conjuncts.push_back(equal_exprt{next_symbol_expr, rhs});
+    }
+  }
+
+  if(!trans_conjuncts.empty())
+    transition_system.trans_expr.trans() = and_exprt{
+      transition_system.trans_expr.trans(), conjunction(trans_conjuncts)};
+
+  return past_map;
+}
+
+void instrument_past_model(
+  const replace_mapt &past_map,
+  transition_systemt &transition_system)
+{
+  replace_expr(past_map, transition_system.trans_expr);
+}
+
+void instrument_past_model(
+  const replace_mapt &past_map,
+  ebmc_propertiest &properties)
+{
+  for(auto &property : properties.properties)
+  {
+    replace_expr(past_map, property.normalized_expr);
+  }
+}
+
+void instrument_past(
+  transition_systemt &transition_system,
+  ebmc_propertiest &properties)
+{
+  past_sett past_set;
+  collect_past(transition_system, past_set);
+  collect_past(properties, past_set);
+
+  complete_past_set(past_set);
+
+  auto past_map = model_past(past_set, transition_system);
+
+  instrument_past_model(past_map, transition_system);
+  instrument_past_model(past_map, properties);
+}

src/ebmc/instrument_past.h

@@ -0,0 +1,20 @@
+/*******************************************************************\
+
+Module: $past Instrumentation
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+/// \file
+/// $past Instrumentation
+
+#ifndef EBMC_INSTRUMENT_PAST_H
+#define EBMC_INSTRUMENT_PAST_H
+
+#include "ebmc_properties.h"
+#include "transition_system.h"
+
+void instrument_past(transition_systemt &, ebmc_propertiest &);
+
+#endif // EBMC_INSTRUMENT_PAST_H

src/ebmc/netlist.cpp

@@ -11,11 +11,15 @@ Author: Daniel Kroening, [email protected]
 #include <trans-netlist/netlist.h>
 #include <trans-netlist/trans_to_netlist.h>
 
+#include "instrument_past.h"
+
 netlistt make_netlist(
   transition_systemt &transition_system,
   ebmc_propertiest &properties,
   message_handlert &message_handler)
 {
+  instrument_past(transition_system, properties);
+
   netlistt netlist;
 
   convert_trans_to_netlist(