Merge pull request #403 from diffblue/SVA-eventually

Verilog: support for weak eventually

Author: kroening

regression/verilog/SVA/eventually1.desc

@@ -0,0 +1,8 @@
+CORE
+eventually1.sv
+--bound 20
+^\[main\.property\.p0\] always \(main\.counter == 1 |-> eventually \[1:2\] main\.counter == 3\): PROVED up to bound 20$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/verilog/SVA/eventually1.sv

@@ -0,0 +1,14 @@
+module main(input clk, input reset);
+
+  // count up from 0 to 10
+  reg [7:0] counter;
+  initial counter = 0;
+
+  always @(posedge clk)
+    if(counter != 10)
+      counter = counter + 1;
+
+  // expected to pass
+  p0: assert property (counter == 1 implies eventually [1:2] counter == 3);
+
+endmodule

regression/verilog/SVA/eventually2.desc

@@ -0,0 +1,8 @@
+CORE
+eventually2.sv
+--bound 20
+^\[main\.property\.p0\] always \(eventually \[0:2\] main\.counter == 3\): REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/verilog/SVA/eventually2.sv

@@ -0,0 +1,10 @@
+module main(input clk, input reset);
+
+  reg [7:0] counter;
+  initial counter = 0;
+  always @(posedge clk) counter = 0;
+
+  // expected to fail
+  p0: assert property (eventually [0:2] counter == 3);
+
+endmodule

src/trans-word-level/instantiate_word_level.cpp

@@ -240,9 +240,34 @@ exprt wl_instantiatet::instantiate_rec(exprt expr, const mp_integer &t) const
     else
       return true_exprt(); // works on NNF only
   }
+  else if(expr.id() == ID_sva_eventually)
+  {
+    const auto &eventually_expr = to_sva_eventually_expr(expr);
+    const auto &range = eventually_expr.range();
+    const auto &op = eventually_expr.op();
+
+    mp_integer lower;
+    if(to_integer_non_constant(range.op0(), lower))
+      throw "failed to convert sva_eventually index";
+
+    mp_integer upper;
+    if(to_integer_non_constant(range.op1(), upper))
+      throw "failed to convert sva_eventually index";
+
+    // This is weak, and passes if any of the timeframes
+    // does not exist.
+    if(t + lower >= no_timeframes || t + upper >= no_timeframes)
+      return true_exprt();
+
+    exprt::operandst disjuncts = {};
+
+    for(mp_integer u = t + lower; u <= t + upper; ++u)
+      disjuncts.push_back(instantiate_rec(op, u));
+
+    return disjunction(disjuncts);
+  }
   else if(
-    expr.id() == ID_sva_eventually || expr.id() == ID_sva_s_eventually ||
-    expr.id() == ID_F || expr.id() == ID_AF)
+    expr.id() == ID_sva_s_eventually || expr.id() == ID_F || expr.id() == ID_AF)
   {
     const auto &p = to_unary_expr(expr).op();
 

src/verilog/expr2verilog.cpp

@@ -17,6 +17,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/std_expr.h>
 #include <util/symbol.h>
 
+#include "sva_expr.h"
 #include "verilog_expr.h"
 #include "verilog_types.h"
 
@@ -385,35 +386,53 @@ Function: expr2verilogt::convert_sva
 
 std::string expr2verilogt::convert_sva(
   const std::string &name,
-  const exprt &src)
+  const std::optional<exprt> &range,
+  const exprt &op)
 {
-  if(src.operands().size()==1)
+  std::string range_str;
+
+  if(range.has_value())
   {
-    auto &op = to_unary_expr(src).op();
-    unsigned p;
-    auto s = convert(op, p);
-    if(p == 0 && op.operands().size() >= 2)
-      s = "(" + s + ")";
-    return name + " " + s;
+    auto &range_binary = to_binary_expr(range.value());
+    range_str = "[" + convert(range_binary.lhs()) + ':' +
+                convert(range_binary.rhs()) + "] ";
   }
-  else if(src.operands().size()==2)
-  {
-    auto &binary_expr = to_binary_expr(src);
 
-    unsigned p0;
-    auto s0 = convert(binary_expr.op0(), p0);
-    if(p0 == 0)
-      s0 = "(" + s0 + ")";
+  unsigned p;
+  auto s = convert(op, p);
+  if(p == 0 && op.operands().size() >= 2)
+    s = "(" + s + ")";
+  return name + " " + range_str + s;
+}
 
-    unsigned p1;
-    auto s1 = convert(binary_expr.op1(), p1);
-    if(p1 == 0)
-      s1 = "(" + s1 + ")";
+/*******************************************************************\
 
-    return s0 + " " + name + " " + s1;
-  }
-  else
-    return "?";
+Function: expr2verilogt::convert_sva
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+std::string expr2verilogt::convert_sva(
+  const exprt &lhs,
+  const std::string &name,
+  const exprt &rhs)
+{
+  unsigned p0;
+  auto s0 = convert(lhs, p0);
+  if(p0 == 0)
+    s0 = "(" + s0 + ")";
+
+  unsigned p1;
+  auto s1 = convert(rhs, p1);
+  if(p1 == 0)
+    s1 = "(" + s1 + ")";
+
+  return s0 + " " + name + " " + s1;
 }
 
 /*******************************************************************\
@@ -1046,10 +1065,16 @@ std::string expr2verilogt::convert(
     return convert_function("$onehot0", src);
 
   else if(src.id()==ID_sva_overlapped_implication)
-    return precedence = 0, convert_sva("|->", src);
+  {
+    auto &binary = to_binary_expr(src);
+    return precedence = 0, convert_sva(binary.lhs(), "|->", binary.rhs());
+  }
 
   else if(src.id()==ID_sva_non_overlapped_implication)
-    return precedence = 0, convert_sva("|=>", src);
+  {
+    auto &binary = to_binary_expr(src);
+    return precedence = 0, convert_sva(binary.lhs(), "|=>", binary.rhs());
+  }
 
   else if(src.id()==ID_sva_cycle_delay)
     return convert_sva_cycle_delay(to_ternary_expr(src), precedence = 0);
@@ -1061,31 +1086,49 @@ std::string expr2verilogt::convert(
     // not sure about precedence
 
   else if(src.id()==ID_sva_always)
-    return precedence = 0, convert_sva("always", src);
+    return precedence = 0, convert_sva("always", to_sva_always_expr(src).op());
 
   else if(src.id()==ID_sva_nexttime)
-    return precedence = 0, convert_sva("nexttime", src);
+    return precedence = 0,
+           convert_sva("nexttime", to_sva_nexttime_expr(src).op());
 
   else if(src.id()==ID_sva_s_nexttime)
-    return precedence = 0, convert_sva("s_nexttime", src);
+    return precedence = 0,
+           convert_sva("s_nexttime", to_sva_s_nexttime_expr(src).op());
 
   else if(src.id()==ID_sva_eventually)
-    return precedence = 0, convert_sva("eventually", src);
+    return precedence = 0, convert_sva(
+                             "eventually",
+                             to_sva_eventually_expr(src).range(),
+                             to_sva_eventually_expr(src).op());
 
   else if(src.id()==ID_sva_s_eventually)
-    return precedence = 0, convert_sva("s_eventually", src);
+    return precedence = 0,
+           convert_sva("s_eventually", to_sva_s_eventually_expr(src).op());
 
   else if(src.id()==ID_sva_until)
-    return precedence = 0, convert_sva("until", src);
+    return precedence = 0, convert_sva(
+                             to_sva_until_expr(src).lhs(),
+                             "until",
+                             to_sva_until_expr(src).rhs());
 
   else if(src.id()==ID_sva_s_until)
-    return precedence = 0, convert_sva("s_until", src);
+    return precedence = 0, convert_sva(
+                             to_sva_s_until_expr(src).lhs(),
+                             "s_until",
+                             to_sva_s_until_expr(src).rhs());
 
   else if(src.id()==ID_sva_until_with)
-    return precedence = 0, convert_sva("until_with", src);
+    return precedence = 0, convert_sva(
+                             to_sva_until_with_expr(src).lhs(),
+                             "until_with",
+                             to_sva_until_with_expr(src).rhs());
 
   else if(src.id()==ID_sva_s_until_with)
-    return precedence = 0, convert_sva("s_until_with", src);
+    return precedence = 0, convert_sva(
+                             to_sva_s_until_with_expr(src).lhs(),
+                             "s_until_with",
+                             to_sva_s_until_with_expr(src).rhs());
 
   else if(src.id()==ID_function_call)
     return convert_function_call(to_function_call_expr(src));

src/verilog/expr2verilog_class.h

@@ -82,9 +82,18 @@ class expr2verilogt
     const std::string &name,
     const exprt &src);
 
-  virtual std::string convert_sva(
+  std::string convert_sva(
     const std::string &name,
-    const exprt &src);
+    const std::optional<exprt> &range,
+    const exprt &op);
+
+  std::string convert_sva(const std::string &name, const exprt &op)
+  {
+    return convert_sva(name, {}, op);
+  }
+
+  std::string
+  convert_sva(const exprt &lhs, const std::string &name, const exprt &rhs);
 
   virtual std::string
   convert_replication(const replication_exprt &, unsigned precedence);

src/verilog/sva_expr.h

@@ -69,15 +69,15 @@ class sva_eventually_exprt : public binary_predicate_exprt
   {
   }
 
-  // These come with a range
-  const exprt &range() const
+  // These come with a range, which is binary
+  const binary_exprt &range() const
   {
-    return op0();
+    return static_cast<const binary_exprt &>(op0());
   }
 
-  exprt &range()
+  binary_exprt &range()
   {
-    return op0();
+    return static_cast<binary_exprt &>(op0());
   }
 
   const exprt &op() const
@@ -95,6 +95,14 @@ class sva_eventually_exprt : public binary_predicate_exprt
   const exprt &rhs() const = delete;
   exprt &rhs() = delete;
 
+  static void check(
+    const exprt &expr,
+    const validation_modet vm = validation_modet::INVARIANT)
+  {
+    binary_exprt::check(expr, vm);
+    binary_exprt::check(to_binary_expr(expr).op0(), vm);
+  }
+
 protected:
   using binary_predicate_exprt::op0;
   using binary_predicate_exprt::op1;

src/verilog/verilog_typecheck_expr.cpp

@@ -6,9 +6,7 @@ Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
-#include <cctype>
-#include <cstdlib>
-#include <algorithm>
+#include "verilog_typecheck_expr.h"
 
 #include <util/bitvector_expr.h>
 #include <util/ebmc_util.h>
@@ -20,10 +18,14 @@ Author: Daniel Kroening, [email protected]
 #include <util/std_expr.h>
 
 #include "expr2verilog.h"
+#include "sva_expr.h"
 #include "verilog_expr.h"
-#include "verilog_typecheck_expr.h"
-#include "vtype.h"
 #include "verilog_types.h"
+#include "vtype.h"
+
+#include <algorithm>
+#include <cctype>
+#include <cstdlib>
 
 /*******************************************************************\
 
@@ -1853,11 +1855,9 @@ exprt verilog_typecheck_exprt::convert_unary_expr(unary_exprt expr)
     no_bool_ops(expr);
     expr.type() = expr.op().type();
   }
-  else if(expr.id()==ID_sva_always ||
-          expr.id()==ID_sva_nexttime ||
-          expr.id()==ID_sva_s_nexttime ||
-          expr.id()==ID_sva_eventually ||
-          expr.id()==ID_sva_s_eventually)
+  else if(
+    expr.id() == ID_sva_always || expr.id() == ID_sva_nexttime ||
+    expr.id() == ID_sva_s_nexttime || expr.id() == ID_sva_s_eventually)
   {
     assert(expr.operands().size()==1);
     convert_expr(expr.op());
@@ -2167,6 +2167,28 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr)
 
     return std::move(expr);
   }
+  else if(expr.id() == ID_sva_eventually)
+  {
+    auto &range = to_binary_expr(expr.op0());
+    auto lower = convert_integer_constant_expression(range.op0());
+    auto upper = convert_integer_constant_expression(range.op1());
+    if(lower > upper)
+    {
+      throw errort().with_location(expr.source_location())
+        << "range must be lower <= upper";
+    }
+
+    range.op0() = from_integer(lower, natural_typet())
+                    .with_source_location<exprt>(range.op0());
+    range.op1() = from_integer(upper, natural_typet())
+                    .with_source_location<exprt>(range.op1());
+
+    convert_expr(expr.op1());
+    make_boolean(expr.op1());
+    expr.type() = bool_typet();
+
+    return std::move(expr);
+  }
   else if(expr.id()==ID_hierarchical_identifier)
   {
     return convert_hierarchical_identifier(