SystemVerilog: SVA abort properties

regression/verilog/SVA/sva_abort1.desc

@@ -0,0 +1,13 @@
+CORE
+sva_abort1.sv
+--module main --bound 10
+^\[main\.p0\] always \(accept_on \(main\.counter == 0\) main\.counter != 0\): PROVED up to bound 10$
+^\[main\.p1\] always \(accept_on \(1\) 0\): PROVED up to bound 10$
+^\[main\.p2\] always \(accept_on \(main\.counter == 1\) main\.counter == 0\): REFUTED$
+^\[main\.p3\] always \(reject_on \(main\.counter != 0\) 1\): REFUTED$
+^\[main\.p4\] always \(reject_on \(1\) 1\): REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/SVA/sva_abort1.sv

@@ -0,0 +1,24 @@
+module main(input clk);
+
+  // count up
+  reg [7:0] counter = 0;
+
+  always_ff @(posedge clk)
+    counter++;
+
+  // expected to pass
+  p0: assert property (@(posedge clk) accept_on (counter == 0) counter != 0);
+
+  // expected to pass vacuously
+  p1: assert property (@(posedge clk) accept_on (1) 0);
+
+  // expected to fail when counter reaches 2
+  p2: assert property (@(posedge clk) accept_on (counter == 1) counter == 0);
+
+  // expected to fail when counter reaches 2
+  p3: assert property (@(posedge clk) reject_on (counter != 0) 1);
+
+  // expected to fail
+  p4: assert property (@(posedge clk) reject_on (1) 1);
+
+endmodule

src/hw_cbmc_irep_ids.h

@@ -15,6 +15,10 @@ IREP_ID_ONE(F)
 IREP_ID_ONE(E)
 IREP_ID_ONE(G)
 IREP_ID_ONE(X)
+IREP_ID_ONE(sva_accept_on)
+IREP_ID_ONE(sva_reject_on)
+IREP_ID_ONE(sva_sync_accept_on)
+IREP_ID_ONE(sva_sync_reject_on)
 IREP_ID_ONE(sva_strong)
 IREP_ID_ONE(sva_weak)
 IREP_ID_ONE(sva_if)

src/temporal-logic/normalize_property.cpp

@@ -120,6 +120,17 @@ exprt normalize_property(exprt expr)
     auto &disable_iff_expr = to_sva_disable_iff_expr(expr);
     expr = or_exprt{disable_iff_expr.lhs(), disable_iff_expr.rhs()};
   }
+  else if(expr.id() == ID_sva_accept_on || expr.id() == ID_sva_sync_accept_on)
+  {
+    auto &sva_abort_expr = to_sva_abort_expr(expr);
+    expr = or_exprt{sva_abort_expr.condition(), sva_abort_expr.property()};
+  }
+  else if(expr.id() == ID_sva_reject_on || expr.id() == ID_sva_sync_reject_on)
+  {
+    auto &sva_abort_expr = to_sva_abort_expr(expr);
+    expr = and_exprt{
+      not_exprt{sva_abort_expr.condition()}, sva_abort_expr.property()};
+  }
   else if(expr.id() == ID_sva_strong)
   {
     expr = to_sva_strong_expr(expr).op();

src/temporal-logic/normalize_property.h

@@ -20,6 +20,10 @@ Author: Daniel Kroening, [email protected]
 /// sva_s_nexttime φ --> Xφ
 /// sva_if --> ? :
 /// a sva_disable_iff b --> a ∨ b
+/// a sva_accept_on b --> a ∨ b
+/// a sva_reject_on b --> ¬a ∧ b
+/// a sva_sync_accept_on b --> a ∨ b
+/// a sva_sync_reject_on b --> ¬a ∧ b
 /// ¬Xφ --> X¬φ
 /// ¬¬φ --> φ
 /// ¬Gφ --> F¬φ

src/temporal-logic/temporal_logic.cpp

@@ -14,13 +14,14 @@ bool is_temporal_operator(const exprt &expr)
 {
   return is_CTL_operator(expr) || is_LTL_operator(expr) ||
          is_SVA_sequence(expr) || expr.id() == ID_A || expr.id() == ID_E ||
-         expr.id() == ID_sva_disable_iff || expr.id() == ID_sva_always ||
-         expr.id() == ID_sva_always || expr.id() == ID_sva_ranged_always ||
-         expr.id() == ID_sva_nexttime || expr.id() == ID_sva_s_nexttime ||
-         expr.id() == ID_sva_until || expr.id() == ID_sva_s_until ||
-         expr.id() == ID_sva_until_with || expr.id() == ID_sva_s_until_with ||
-         expr.id() == ID_sva_eventually || expr.id() == ID_sva_s_eventually ||
-         expr.id() == ID_sva_cycle_delay ||
+         expr.id() == ID_sva_disable_iff || expr.id() == ID_sva_accept_on ||
+         expr.id() == ID_sva_reject_on || expr.id() == ID_sva_sync_accept_on ||
+         expr.id() == ID_sva_sync_reject_on || expr.id() == ID_sva_always ||
+         expr.id() == ID_sva_ranged_always || expr.id() == ID_sva_nexttime ||
+         expr.id() == ID_sva_s_nexttime || expr.id() == ID_sva_until ||
+         expr.id() == ID_sva_s_until || expr.id() == ID_sva_until_with ||
+         expr.id() == ID_sva_s_until_with || expr.id() == ID_sva_eventually ||
+         expr.id() == ID_sva_s_eventually || expr.id() == ID_sva_cycle_delay ||
          expr.id() == ID_sva_overlapped_followed_by ||
          expr.id() == ID_sva_nonoverlapped_followed_by;
 }

src/verilog/expr2verilog.cpp

@@ -475,7 +475,7 @@ std::string expr2verilogt::convert_sva_binary(
 
 /*******************************************************************\
 
-Function: expr2verilogt::convert_sva_disable_iff
+Function: expr2verilogt::convert_sva_abort
 
   Inputs:
 
@@ -485,16 +485,17 @@ Function: expr2verilogt::convert_sva_disable_iff
 
 \*******************************************************************/
 
-std::string
-expr2verilogt::convert_sva_disable_iff(const sva_disable_iff_exprt &expr)
+std::string expr2verilogt::convert_sva_abort(
+  const std::string &text,
+  const sva_abort_exprt &expr)
 {
   verilog_precedencet p0;
   auto s0 = convert(expr.condition(), p0);
 
   verilog_precedencet p1;
-  auto s1 = convert(expr.rhs(), p1);
+  auto s1 = convert(expr.property(), p1);
 
-  return "disable iff (" + s0 + ") " + s1;
+  return text + " (" + s0 + ") " + s1;
 }
 
 /*******************************************************************\
@@ -1428,13 +1429,29 @@ expr2verilogt::convert(const exprt &src, verilog_precedencet &precedence)
     return precedence = verilog_precedencet::MIN,
            convert_sva_unary("assume", to_sva_assume_expr(src));
 
+  else if(src.id() == ID_sva_accept_on)
+    return precedence = verilog_precedencet::MIN,
+           convert_sva_abort("accept_on", to_sva_abort_expr(src));
+
+  else if(src.id() == ID_sva_reject_on)
+    return precedence = verilog_precedencet::MIN,
+           convert_sva_abort("reject_on", to_sva_abort_expr(src));
+
+  else if(src.id() == ID_sva_sync_accept_on)
+    return precedence = verilog_precedencet::MIN,
+           convert_sva_abort("sync_accept_on", to_sva_abort_expr(src));
+
+  else if(src.id() == ID_sva_sync_reject_on)
+    return precedence = verilog_precedencet::MIN,
+           convert_sva_abort("sync_reject_on", to_sva_abort_expr(src));
+
   else if(src.id()==ID_sva_nexttime)
     return precedence = verilog_precedencet::MIN,
            convert_sva_indexed_binary("nexttime", to_sva_nexttime_expr(src));
 
   else if(src.id() == ID_sva_disable_iff)
     return precedence = verilog_precedencet::MIN,
-           convert_sva_disable_iff(to_sva_disable_iff_expr(src));
+           convert_sva_abort("disable iff", to_sva_abort_expr(src));
 
   else if(src.id()==ID_sva_s_nexttime)
     return precedence = verilog_precedencet::MIN,

src/verilog/expr2verilog_class.h

@@ -12,8 +12,8 @@ Author: Daniel Kroening, [email protected]
 #include <util/bitvector_expr.h>
 #include <util/std_expr.h>
 
+class sva_abort_exprt;
 class sva_case_exprt;
-class sva_disable_iff_exprt;
 class sva_if_exprt;
 class sva_ranged_predicate_exprt;
 
@@ -121,9 +121,10 @@ class expr2verilogt
   std::string convert_sva_binary(const std::string &name, const binary_exprt &);
 
   std::string
-  convert_sva_indexed_binary(const std::string &name, const binary_exprt &);
+  convert_sva_abort(const std::string &name, const sva_abort_exprt &);
 
-  std::string convert_sva_disable_iff(const sva_disable_iff_exprt &);
+  std::string
+  convert_sva_indexed_binary(const std::string &name, const binary_exprt &);
 
   virtual std::string
   convert_replication(const replication_exprt &, verilog_precedencet);

src/verilog/parser.y

@@ -531,6 +531,7 @@ int yyverilogerror(const char *error)
 // whereas the table gives them in decreasing order.
 // The precendence of the assertion operators is lower than
 // those in Table 11-2.
+%nonassoc "property_expr_abort" // accept_on, reject_on, ...
 %nonassoc "property_expr_clocking_event" // @(...) property_expr
 %nonassoc "always" "s_always" "eventually" "s_eventually"
 %nonassoc "accept_on" "reject_on"
@@ -2157,14 +2158,14 @@ property_expr_proper:
 		{ init($$, ID_implies); mto($$, $1); mto($$, $3); }
 	| property_expr "iff" property_expr
 		{ init($$, ID_iff); mto($$, $1); mto($$, $3); }
-	| "accept_on" '(' expression_or_dist ')'
-		{ init($$, "sva_accept_on"); mto($$, $3); }
-	| "reject_on" '(' expression_or_dist ')'
-		{ init($$, "sva_reject_on"); mto($$, $3); }
-	| "sync_accept_on" '(' expression_or_dist ')'
-		{ init($$, "sva_sync_accept_on"); mto($$, $3); }
-	| "sync_reject_on" '(' expression_or_dist ')'
-		{ init($$, "sva_sync_reject_on"); mto($$, $3); }
+	| "accept_on" '(' expression_or_dist ')' property_expr %prec "property_expr_abort"
+		{ init($$, ID_sva_accept_on); mto($$, $3); mto($$, $5); }
+	| "reject_on" '(' expression_or_dist ')' property_expr %prec "property_expr_abort"
+		{ init($$, ID_sva_reject_on); mto($$, $3); mto($$, $5); }
+	| "sync_accept_on" '(' expression_or_dist ')' property_expr %prec "property_expr_abort"
+		{ init($$, ID_sva_sync_accept_on); mto($$, $3); mto($$, $5); }
+	| "sync_reject_on" '(' expression_or_dist ')' property_expr %prec "property_expr_abort"
+		{ init($$, ID_sva_sync_reject_on); mto($$, $3); mto($$, $5); }
 	| clocking_event property_expr { $$=$2; } %prec "property_expr_clocking_event"
 	;
 

src/verilog/sva_expr.h

@@ -11,14 +11,12 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/std_expr.h>
 
-class sva_disable_iff_exprt : public binary_predicate_exprt
+/// accept_on, reject_on, sync_accept_on, sync_reject_on, disable_iff
+class sva_abort_exprt : public binary_predicate_exprt
 {
 public:
-  explicit sva_disable_iff_exprt(exprt condition, exprt property)
-    : binary_predicate_exprt(
-        std::move(condition),
-        ID_sva_disable_iff,
-        std::move(property))
+  sva_abort_exprt(irep_idt id, exprt condition, exprt property)
+    : binary_predicate_exprt(std::move(condition), id, std::move(property))
   {
   }
 
@@ -47,6 +45,30 @@ class sva_disable_iff_exprt : public binary_predicate_exprt
   using binary_predicate_exprt::op1;
 };
 
+static inline const sva_abort_exprt &to_sva_abort_expr(const exprt &expr)
+{
+  sva_abort_exprt::check(expr, validation_modet::INVARIANT);
+  return static_cast<const sva_abort_exprt &>(expr);
+}
+
+static inline sva_abort_exprt &to_sva_abort_expr(exprt &expr)
+{
+  sva_abort_exprt::check(expr, validation_modet::INVARIANT);
+  return static_cast<sva_abort_exprt &>(expr);
+}
+
+class sva_disable_iff_exprt : public sva_abort_exprt
+{
+public:
+  sva_disable_iff_exprt(exprt condition, exprt property)
+    : sva_abort_exprt(
+        ID_sva_disable_iff,
+        std::move(condition),
+        std::move(property))
+  {
+  }
+};
+
 static inline const sva_disable_iff_exprt &
 to_sva_disable_iff_expr(const exprt &expr)
 {

src/verilog/verilog_typecheck_expr.cpp

@@ -2578,12 +2578,15 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr)
 
     return std::move(expr);
   }
-  else if(expr.id() == ID_sva_disable_iff)
-  {
-    convert_expr(to_sva_disable_iff_expr(expr).condition());
-    make_boolean(to_sva_disable_iff_expr(expr).condition());
-    convert_expr(to_sva_disable_iff_expr(expr).property());
-    make_boolean(to_sva_disable_iff_expr(expr).property());
+  else if(
+    expr.id() == ID_sva_disable_iff || expr.id() == ID_sva_accept_on ||
+    expr.id() == ID_sva_reject_on || expr.id() == ID_sva_sync_accept_on ||
+    expr.id() == ID_sva_sync_reject_on)
+  {
+    convert_expr(to_sva_abort_expr(expr).condition());
+    make_boolean(to_sva_abort_expr(expr).condition());
+    convert_expr(to_sva_abort_expr(expr).property());
+    make_boolean(to_sva_abort_expr(expr).property());
     expr.type() = bool_typet();
     return std::move(expr);
   }