Merge pull request #617 from diffblue/disable_iff1

SystemVerilog: disable iff

Author: tautschnig

regression/verilog/SVA/disable_iff1.desc

@@ -0,0 +1,12 @@
+CORE
+disable_iff1.sv
+--module main --bound 10 --numbered-trace
+^\[main\.p0\] always \(disable iff \(main.counter == 0\) main\.counter != 0\): PROVED up to bound 10$
+^\[main\.p1\] always \(disable iff \(1\) 0\): PROVED up to bound 10$
+^\[main\.p2\] always \(disable iff \(main\.counter == 1\) main\.counter == 0\): REFUTED$
+^Counterexample with 3 states:$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/SVA/disable_iff1.sv

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

src/hw_cbmc_irep_ids.h

@@ -22,6 +22,7 @@ IREP_ID_ONE(sva_case)
 IREP_ID_ONE(sva_cycle_delay)
 IREP_ID_ONE(sva_cycle_delay_star)
 IREP_ID_ONE(sva_cycle_delay_plus)
+IREP_ID_ONE(sva_disable_iff)
 IREP_ID_ONE(sva_sequence_concatenation)
 IREP_ID_ONE(sva_sequence_consecutive_repetition)
 IREP_ID_ONE(sva_sequence_first_match)

src/temporal-logic/normalize_property.cpp

@@ -115,6 +115,11 @@ exprt normalize_property(exprt expr)
                         : sva_if_expr.false_case();
     expr = if_exprt{sva_if_expr.cond(), sva_if_expr.true_case(), false_case};
   }
+  else if(expr.id() == ID_sva_disable_iff)
+  {
+    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_strong)
   {
     expr = to_sva_strong_expr(expr).op();

src/temporal-logic/normalize_property.h

@@ -19,6 +19,7 @@ Author: Daniel Kroening, dkr@amazon.com
 /// sva_nexttime φ --> Xφ
 /// sva_s_nexttime φ --> Xφ
 /// sva_if --> ? :
+/// a sva_disable_iff b --> a ∨ b
 /// ¬Xφ --> X¬φ
 /// ¬¬φ --> φ
 /// ¬Gφ --> F¬φ

src/temporal-logic/temporal_logic.cpp

@@ -14,12 +14,13 @@ 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_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_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_overlapped_followed_by ||
          expr.id() == ID_sva_nonoverlapped_followed_by;
 }

src/verilog/expr2verilog.cpp

@@ -475,6 +475,30 @@ std::string expr2verilogt::convert_sva_binary(
 
 /*******************************************************************\
 
+Function: expr2verilogt::convert_sva_disable_iff
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+std::string
+expr2verilogt::convert_sva_disable_iff(const sva_disable_iff_exprt &expr)
+{
+  verilog_precedencet p0;
+  auto s0 = convert(expr.condition(), p0);
+
+  verilog_precedencet p1;
+  auto s1 = convert(expr.rhs(), p1);
+
+  return "disable iff (" + s0 + ") " + s1;
+}
+
+/*******************************************************************\
+
 Function: expr2verilogt::convert_sva_indexed_binary
 
   Inputs:
@@ -1408,6 +1432,10 @@ expr2verilogt::convert(const exprt &src, verilog_precedencet &precedence)
     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));
+
   else if(src.id()==ID_sva_s_nexttime)
     return precedence = verilog_precedencet::MIN,
            convert_sva_indexed_binary(

src/verilog/expr2verilog_class.h

@@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/std_expr.h>
 
 class sva_case_exprt;
+class sva_disable_iff_exprt;
 class sva_if_exprt;
 class sva_ranged_predicate_exprt;
 
@@ -122,6 +123,8 @@ class expr2verilogt
   std::string
   convert_sva_indexed_binary(const std::string &name, const binary_exprt &);
 
+  std::string convert_sva_disable_iff(const sva_disable_iff_exprt &);
+
   virtual std::string
   convert_replication(const replication_exprt &, verilog_precedencet);
 

src/verilog/parser.y

@@ -531,7 +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_event_control" // @(...) property_expr
+%nonassoc "property_expr_clocking_event" // @(...) property_expr
 %nonassoc "always" "s_always" "eventually" "s_eventually"
 %nonassoc "accept_on" "reject_on"
 %nonassoc "sync_accept_on" "sync_reject_on"
@@ -2081,8 +2081,10 @@ property_formal_type:
 	;
 
 property_spec:
-	  TOK_DISABLE TOK_IFF '(' expression ')' property_expr
-		{ $$=$6; }
+	  clocking_event TOK_DISABLE TOK_IFF '(' expression ')' property_expr
+		{ init($$, ID_sva_disable_iff); mto($$, $5); mto($$, $7); }
+	| TOK_DISABLE TOK_IFF '(' expression ')' property_expr
+		{ init($$, ID_sva_disable_iff); mto($$, $4); mto($$, $6); }
 	| property_expr
 	;
 
@@ -2163,7 +2165,7 @@ property_expr_proper:
 		{ init($$, "sva_sync_accept_on"); mto($$, $3); }
 	| "sync_reject_on" '(' expression_or_dist ')'
 		{ init($$, "sva_sync_reject_on"); mto($$, $3); }
-	| event_control property_expr { $$=$2; } %prec "property_expr_event_control"
+	| clocking_event property_expr { $$=$2; } %prec "property_expr_clocking_event"
 	;
 
 property_case_item_brace:

src/verilog/sva_expr.h

@@ -11,6 +11,57 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/std_expr.h>
 
+class sva_disable_iff_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))
+  {
+  }
+
+  const exprt &condition() const
+  {
+    return op0();
+  }
+
+  exprt &condition()
+  {
+    return op0();
+  }
+
+  const exprt &property() const
+  {
+    return op1();
+  }
+
+  exprt &property()
+  {
+    return op1();
+  }
+
+protected:
+  using binary_predicate_exprt::op0;
+  using binary_predicate_exprt::op1;
+};
+
+static inline const sva_disable_iff_exprt &
+to_sva_disable_iff_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_sva_disable_iff);
+  sva_disable_iff_exprt::check(expr, validation_modet::INVARIANT);
+  return static_cast<const sva_disable_iff_exprt &>(expr);
+}
+
+static inline sva_disable_iff_exprt &to_sva_disable_iff_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_sva_disable_iff);
+  sva_disable_iff_exprt::check(expr, validation_modet::INVARIANT);
+  return static_cast<sva_disable_iff_exprt &>(expr);
+}
+
 class sva_nexttime_exprt : public binary_predicate_exprt
 {
 public: