Verilog: introduce sva_and_exprt, sva_or_exprt, sva_not_exprt

kroening · kroening · commit 3294afef6da6 · 2024-07-31T18:59:40.000-07:00
The SVA operators and, or differ from their standard Boolean counterparts
when applied to SVA sequences.  This introduces a separate IR for them.

This also introduces a separate IR for SVA not, for the benefit of
pretty-printing SVA formulas.
diff --git a/regression/ebmc/ring_buffer_bdd/ring_buffer.sv b/regression/ebmc/ring_buffer_bdd/ring_buffer.sv
@@ -19,8 +19,8 @@ module ring_buffer(input clk, input read, input write);
   wire full=count==15;
   wire empty=count==0;
 
-  assume property (empty -> !read);
-  assume property (full -> !write);
+  assume property (empty |-> !read);
+  assume property (full |-> !write);
 
   assert property (((writeptr-readptr)&'b1111)==count);
 
diff --git a/regression/ebmc/ring_buffer_induction/ring_buffer.sv b/regression/ebmc/ring_buffer_induction/ring_buffer.sv
@@ -19,8 +19,8 @@ module ring_buffer(input clk, input read, input write);
   wire full=count==15;
   wire empty=count==0;
 
-  assume property (empty -> !read);
-  assume property (full -> !write);
+  assume property (empty |-> !read);
+  assume property (full |-> !write);
 
   assert property (((writeptr-readptr)&'b1111)==count);
 
diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h
@@ -44,6 +44,9 @@ IREP_ID_ONE(sva_overlapped_followed_by)
 IREP_ID_ONE(sva_nonoverlapped_followed_by)
 IREP_ID_ONE(sva_overlapped_implication)
 IREP_ID_ONE(sva_non_overlapped_implication)
+IREP_ID_ONE(sva_and)
+IREP_ID_ONE(sva_not)
+IREP_ID_ONE(sva_or)
 IREP_ID_ONE(module_instance)
 IREP_ID_TWO(C_offset, #offset)
 IREP_ID_TWO(C_big_endian, #big_endian)
diff --git a/src/temporal-logic/normalize_property.cpp b/src/temporal-logic/normalize_property.cpp
@@ -14,6 +14,7 @@ Author: Daniel Kroening, dkr@amazon.com
 #include <verilog/sva_expr.h>
 
 #include "temporal_expr.h"
+#include "temporal_logic.h"
 
 exprt normalize_pre_not(not_exprt expr)
 {
@@ -61,6 +62,51 @@ exprt normalize_pre_implies(implies_exprt expr)
   return or_exprt{not_exprt{expr.lhs()}, expr.rhs()};
 }
 
+exprt normalize_pre_sva_overlapped_implication(
+  sva_overlapped_implication_exprt expr)
+{
+  // Same as regular implication if lhs and rhs are not
+  // sequences.
+  if(!is_SVA_sequence(expr.lhs()) && !is_SVA_sequence(expr.rhs()))
+    return or_exprt{not_exprt{expr.lhs()}, expr.rhs()};
+  else
+    return std::move(expr);
+}
+
+exprt normalize_pre_sva_non_overlapped_implication(
+  sva_non_overlapped_implication_exprt expr)
+{
+  // Same as a->Xb if lhs and rhs are not sequences.
+  if(!is_SVA_sequence(expr.lhs()) && !is_SVA_sequence(expr.rhs()))
+    return or_exprt{not_exprt{expr.lhs()}, X_exprt{expr.rhs()}};
+  else
+    return std::move(expr);
+}
+
+exprt normalize_pre_sva_not(sva_not_exprt expr)
+{
+  // Same as regular 'not'. These do not apply to sequences.
+  return not_exprt{expr.op()};
+}
+
+exprt normalize_pre_sva_and(sva_and_exprt expr)
+{
+  // Same as a ∧ b if lhs and rhs are not sequences.
+  if(!is_SVA_sequence(expr.lhs()) && !is_SVA_sequence(expr.rhs()))
+    return and_exprt{expr.lhs(), expr.rhs()};
+  else
+    return std::move(expr);
+}
+
+exprt normalize_pre_sva_or(sva_or_exprt expr)
+{
+  // Same as a ∧ b if lhs or rhs are not sequences.
+  if(!is_SVA_sequence(expr.lhs()) && !is_SVA_sequence(expr.rhs()))
+    return or_exprt{expr.lhs(), expr.rhs()};
+  else
+    return std::move(expr);
+}
+
 exprt normalize_pre_sva_cycle_delay(sva_cycle_delay_exprt expr)
 {
   if(expr.is_unbounded())
@@ -91,6 +137,18 @@ exprt normalize_property(exprt expr)
     expr = normalize_pre_implies(to_implies_expr(expr));
   else if(expr.id() == ID_sva_cover)
     expr = G_exprt{not_exprt{to_sva_cover_expr(expr).op()}};
+  else if(expr.id() == ID_sva_overlapped_implication)
+    expr = normalize_pre_sva_overlapped_implication(
+      to_sva_overlapped_implication_expr(expr));
+  else if(expr.id() == ID_sva_non_overlapped_implication)
+    expr = normalize_pre_sva_non_overlapped_implication(
+      to_sva_non_overlapped_implication_expr(expr));
+  else if(expr.id() == ID_sva_and)
+    expr = normalize_pre_sva_and(to_sva_and_expr(expr));
+  else if(expr.id() == ID_sva_not)
+    expr = normalize_pre_sva_not(to_sva_not_expr(expr));
+  else if(expr.id() == ID_sva_or)
+    expr = normalize_pre_sva_or(to_sva_or_expr(expr));
   else if(expr.id() == ID_sva_nexttime)
   {
     if(!to_sva_nexttime_expr(expr).is_indexed())
diff --git a/src/temporal-logic/normalize_property.h b/src/temporal-logic/normalize_property.h
@@ -16,6 +16,11 @@ Author: Daniel Kroening, dkr@amazon.com
 /// ¬(a ∨ b) --> ¬a ∧ ¬b
 /// ¬(a ∧ b) --> ¬a ∨ ¬b
 /// (a -> b) --> ¬a ∨ b
+/// sva_not a --> ¬a
+/// a sva_and b --> a ∧ b                       if a and b are not SVA sequences
+/// a sva_or b --> a ∨ b                        if a and b are not SVA sequences
+/// sva_overlapped_implication --> ¬a ∨ b       if a and b are not SVA sequences
+/// sva_non_overlapped_implication --> ¬a ∨ Xb  if a and b are not SVA sequences
 /// sva_nexttime φ --> Xφ
 /// sva_s_nexttime φ --> Xφ
 /// sva_if --> ? :
diff --git a/src/temporal-logic/temporal_logic.cpp b/src/temporal-logic/temporal_logic.cpp
@@ -71,7 +71,9 @@ bool is_SVA_sequence(const exprt &expr)
   auto id = expr.id();
   // Note that ID_sva_overlapped_followed_by and ID_sva_nonoverlapped_followed_by
   // are property expressions, not sequence expressions.
-  return id == ID_sva_overlapped_implication ||
+  // Note that ID_sva_not does not yield a sequence expression.
+  return id == ID_sva_and || id == ID_sva_or ||
+         id == ID_sva_overlapped_implication ||
          id == ID_sva_non_overlapped_implication || id == ID_sva_cycle_delay ||
          id == ID_sva_sequence_concatenation ||
          id == ID_sva_sequence_intersect || id == ID_sva_sequence_first_match ||
diff --git a/src/trans-word-level/instantiate_word_level.cpp b/src/trans-word-level/instantiate_word_level.cpp
@@ -9,6 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "instantiate_word_level.h"
 
 #include <util/ebmc_util.h>
+#include <util/expr_util.h>
 
 #include <temporal-logic/temporal_expr.h>
 #include <temporal-logic/temporal_logic.h>
@@ -240,6 +241,7 @@ wl_instantiatet::instantiate_sequence(exprt expr, const mp_integer &t) const
   }
   else if(expr.id() == ID_sva_sequence_intersect)
   {
+    // IEEE 1800-2017 16.9.6
     PRECONDITION(false);
   }
   else if(expr.id() == ID_sva_sequence_first_match)
@@ -254,6 +256,35 @@ wl_instantiatet::instantiate_sequence(exprt expr, const mp_integer &t) const
   {
     PRECONDITION(false);
   }
+  else if(expr.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.
+    // Condition (3) is TBD.
+    exprt::operandst conjuncts;
+
+    for(auto &op : expr.operands())
+      conjuncts.push_back(instantiate_rec(op, t).second);
+
+    exprt condition = conjunction(conjuncts);
+    return {{t, condition}};
+  }
+  else if(expr.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<std::pair<mp_integer, exprt>> result;
+
+    for(auto &op : expr.operands())
+      for(auto &match_point : instantiate_sequence(op, t))
+        result.push_back(match_point);
+
+    return result;
+  }
   else
   {
     // not a sequence, evaluate as state predicate
diff --git a/src/verilog/expr2verilog.cpp b/src/verilog/expr2verilog.cpp
@@ -1217,6 +1217,9 @@ expr2verilogt::convert(const exprt &src, verilog_precedencet &precedence)
     return convert_unary(
       to_not_expr(src), "!", precedence = verilog_precedencet::NOT);
 
+  else if(src.id() == ID_sva_not)
+    return convert_sva_unary("not", to_sva_not_expr(src));
+
   else if(src.id()==ID_bitnot)
     return convert_unary(
       to_bitnot_expr(src), "~", precedence = verilog_precedencet::NOT);
@@ -1228,6 +1231,9 @@ expr2verilogt::convert(const exprt &src, verilog_precedencet &precedence)
     return convert_binary(
       to_multi_ary_expr(src), "&&", precedence = verilog_precedencet::AND);
 
+  else if(src.id() == ID_sva_and)
+    return convert_sva_binary("and", to_sva_and_expr(src));
+
   else if(src.id()==ID_power)
     return convert_binary(
       to_multi_ary_expr(src), "**", precedence = verilog_precedencet::POWER);
@@ -1252,6 +1258,9 @@ expr2verilogt::convert(const exprt &src, verilog_precedencet &precedence)
     return convert_binary(
       to_multi_ary_expr(src), "||", precedence = verilog_precedencet::OR);
 
+  else if(src.id() == ID_sva_or)
+    return convert_sva_binary("or", to_sva_or_expr(src));
+
   else if(src.id()==ID_bitor)
     return convert_binary(
       to_multi_ary_expr(src), "|", precedence = verilog_precedencet::BITOR);
diff --git a/src/verilog/parser.y b/src/verilog/parser.y
@@ -2100,11 +2100,11 @@ property_expr_proper:
 	| '(' property_expr_proper ')'
 		{ $$ = $2; }
 	| "not" property_expr
-		{ init($$, ID_not); mto($$, $2); }
+		{ init($$, ID_sva_not); mto($$, $2); }
 	| property_expr "or" property_expr
-		{ init($$, ID_or); mto($$, $1); mto($$, $3); }
+		{ init($$, ID_sva_or); mto($$, $1); mto($$, $3); }
 	| property_expr "and" property_expr
-		{ init($$, ID_and); mto($$, $1); mto($$, $3); }
+		{ init($$, ID_sva_and); mto($$, $1); mto($$, $3); }
 	| property_expr "|->" property_expr
 		{ init($$, ID_sva_overlapped_implication); mto($$, $1); mto($$, $3); }
 	| property_expr "|=>" property_expr
diff --git a/src/verilog/sva_expr.h b/src/verilog/sva_expr.h
@@ -500,6 +500,75 @@ to_sva_non_overlapped_implication_expr(exprt &expr)
   return static_cast<sva_non_overlapped_implication_exprt &>(expr);
 }
 
+class sva_not_exprt : public unary_predicate_exprt
+{
+public:
+  explicit sva_not_exprt(exprt op)
+    : unary_predicate_exprt(ID_sva_not, std::move(op))
+  {
+  }
+};
+
+static inline const sva_not_exprt &to_sva_not_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_sva_not);
+  sva_not_exprt::check(expr);
+  return static_cast<const sva_not_exprt &>(expr);
+}
+
+static inline sva_not_exprt &to_sva_not_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_sva_not);
+  sva_not_exprt::check(expr);
+  return static_cast<sva_not_exprt &>(expr);
+}
+
+class sva_and_exprt : public binary_predicate_exprt
+{
+public:
+  explicit sva_and_exprt(exprt op0, exprt op1)
+    : binary_predicate_exprt(std::move(op0), ID_sva_and, std::move(op1))
+  {
+  }
+};
+
+static inline const sva_and_exprt &to_sva_and_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_sva_and);
+  sva_and_exprt::check(expr, validation_modet::INVARIANT);
+  return static_cast<const sva_and_exprt &>(expr);
+}
+
+static inline sva_and_exprt &to_sva_and_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_sva_and);
+  sva_and_exprt::check(expr, validation_modet::INVARIANT);
+  return static_cast<sva_and_exprt &>(expr);
+}
+
+class sva_or_exprt : public binary_predicate_exprt
+{
+public:
+  explicit sva_or_exprt(exprt op0, exprt op1)
+    : binary_predicate_exprt(std::move(op0), ID_sva_or, std::move(op1))
+  {
+  }
+};
+
+static inline const sva_or_exprt &to_sva_or_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_sva_or);
+  sva_or_exprt::check(expr, validation_modet::INVARIANT);
+  return static_cast<const sva_or_exprt &>(expr);
+}
+
+static inline sva_or_exprt &to_sva_or_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_sva_or);
+  sva_or_exprt::check(expr, validation_modet::INVARIANT);
+  return static_cast<sva_or_exprt &>(expr);
+}
+
 class sva_cycle_delay_exprt : public ternary_exprt
 {
 public:
