Merge pull request #535 from diffblue/sva-if

SVA if expressions

regression/verilog/SVA/if1.desc

@@ -0,0 +1,11 @@
+CORE broken-smt-backend
+if1.sv
+--bound 2
+^\[main\.property\.p0\] always if\(main\.counter == 0\) nexttime main\.counter == 1: PROVED up to bound 2$
+^\[main\.property\.p1\] always if\(main\.counter == 0\) nexttime main\.counter == 1 else nexttime main\.counter == 3: REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+SMT-back end doesn't do cast from bool to bool.

regression/verilog/SVA/if1.sv

@@ -0,0 +1,17 @@
+module main(input clk);
+
+  // count up from 0 to 10
+  reg [7:0] counter;
+
+  initial counter = 0;
+
+  always @(posedge clk)
+    counter = counter + 1;
+
+  // expected to pass
+  p0: assert property (if(counter == 0) nexttime counter == 1);
+
+  // expected to fail
+  p1: assert property (if(counter == 0) nexttime counter == 1 else nexttime counter == 3);
+
+endmodule

src/hw_cbmc_irep_ids.h

@@ -15,6 +15,7 @@ IREP_ID_ONE(F)
 IREP_ID_ONE(E)
 IREP_ID_ONE(G)
 IREP_ID_ONE(X)
+IREP_ID_ONE(sva_if)
 IREP_ID_ONE(sva_cycle_delay)
 IREP_ID_ONE(sva_cycle_delay_star)
 IREP_ID_ONE(sva_cycle_delay_plus)

src/temporal-logic/normalize_property.cpp

@@ -127,6 +127,14 @@ exprt normalize_property(exprt expr)
     expr = F_exprt{X_exprt{to_sva_cycle_delay_plus_expr(expr).op()}};
   else if(expr.id() == ID_sva_cycle_delay_star)
     expr = X_exprt{to_sva_cycle_delay_star_expr(expr).op()};
+  else if(expr.id() == ID_sva_if)
+  {
+    auto &sva_if_expr = to_sva_if_expr(expr);
+    auto false_case = sva_if_expr.false_case().is_nil()
+                        ? true_exprt{}
+                        : sva_if_expr.false_case();
+    expr = if_exprt{sva_if_expr.cond(), sva_if_expr.true_case(), false_case};
+  }
 
   // normalize the operands
   for(auto &op : expr.operands())

src/temporal-logic/normalize_property.h

@@ -20,6 +20,7 @@ Author: Daniel Kroening, [email protected]
 /// sva_non_overlapped_implication --> ¬a ∨ Xb
 /// sva_nexttime φ --> Xφ
 /// sva_s_nexttime φ --> Xφ
+/// sva_if --> ? :
 /// ¬Xφ --> X¬φ
 /// ¬¬φ --> φ
 /// ¬Gφ --> F¬φ

src/verilog/expr2verilog.cpp

@@ -488,6 +488,27 @@ std::string expr2verilogt::convert_sva_indexed_binary(
 
 /*******************************************************************\
 
+Function: expr2verilogt::convert_sva_if
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+std::string expr2verilogt::convert_sva_if(const sva_if_exprt &src)
+{
+  if(src.false_case().is_nil())
+    return "if(" + convert(src.cond()) + ") " + convert(src.true_case());
+  else
+    return "if(" + convert(src.cond()) + ") " + convert(src.true_case()) +
+           " else " + convert(src.false_case());
+}
+
+/*******************************************************************\
+
 Function: expr2verilogt::convert_replication
 
   Inputs:
@@ -1221,6 +1242,9 @@ std::string expr2verilogt::convert(
     return precedence = 0,
            convert_sva_binary("s_until_with", to_sva_s_until_with_expr(src));
 
+  else if(src.id() == ID_sva_if)
+    return precedence = 0, convert_sva_if(to_sva_if_expr(src));
+
   else if(src.id()==ID_function_call)
     return convert_function_call(to_function_call_expr(src));
 

src/verilog/expr2verilog_class.h

@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/bitvector_expr.h>
 #include <util/std_expr.h>
 
+class sva_if_exprt;
 class sva_ranged_predicate_exprt;
 
 class expr2verilogt
@@ -107,6 +108,8 @@ class expr2verilogt
   virtual std::string
   convert_sva_cycle_delay(const ternary_exprt &, unsigned precedence);
 
+  std::string convert_sva_if(const sva_if_exprt &);
+
   virtual std::string
   convert_sva_sequence_concatenation(const binary_exprt &, unsigned precedence);
 

src/verilog/parser.y

@@ -2059,6 +2059,10 @@ property_expr_proper:
         | property_expr "and" property_expr { init($$, ID_and); mto($$, $1); mto($$, $3); }
         | property_expr "|->" property_expr { init($$, ID_sva_overlapped_implication); mto($$, $1); mto($$, $3); }
         | property_expr "|=>" property_expr { init($$, ID_sva_non_overlapped_implication); mto($$, $1); mto($$, $3); }
+        | "if" '(' expression_or_dist ')' property_expr %prec LT_TOK_ELSE
+		{ init($$, ID_sva_if); mto($$, $3); mto($$, $5); stack_expr($$).add_to_operands(nil_exprt()); }
+        | "if" '(' expression_or_dist ')' property_expr "else" property_expr
+		{ init($$, ID_sva_if); mto($$, $3); mto($$, $5); mto($$, $7); }
         | "nexttime" property_expr
 		{ init($$, "sva_nexttime"); stack_expr($$).add_to_operands(nil_exprt()); mto($$, $2); }
         | "nexttime" '[' constant_expression ']' property_expr %prec "nexttime"

src/verilog/sva_expr.h

@@ -631,4 +631,68 @@ to_sva_cycle_delay_star_expr(exprt &expr)
   return static_cast<sva_cycle_delay_star_exprt &>(expr);
 }
 
+class sva_if_exprt : public ternary_exprt
+{
+public:
+  explicit sva_if_exprt(exprt __cond, exprt __true_case, exprt __false_case)
+    : ternary_exprt(
+        ID_sva_if,
+        std::move(__cond),
+        std::move(__true_case),
+        std::move(__false_case),
+        bool_typet())
+  {
+  }
+
+  const exprt &cond() const
+  {
+    return op0();
+  }
+
+  exprt &cond()
+  {
+    return op0();
+  }
+
+  const exprt &true_case() const
+  {
+    return op1();
+  }
+
+  exprt &true_case()
+  {
+    return op1();
+  }
+
+  // may be nil (in which case it defaults to 'true')
+  const exprt &false_case() const
+  {
+    return op2();
+  }
+
+  exprt &false_case()
+  {
+    return op2();
+  }
+
+protected:
+  using ternary_exprt::op0;
+  using ternary_exprt::op1;
+  using ternary_exprt::op2;
+};
+
+static inline const sva_if_exprt &to_sva_if_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_sva_if);
+  sva_if_exprt::check(expr);
+  return static_cast<const sva_if_exprt &>(expr);
+}
+
+static inline sva_if_exprt &to_sva_if_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_sva_if);
+  sva_if_exprt::check(expr);
+  return static_cast<sva_if_exprt &>(expr);
+}
+
 #endif

src/verilog/verilog_typecheck_expr.cpp

@@ -2516,6 +2516,22 @@ exprt verilog_typecheck_exprt::convert_trinary_expr(ternary_exprt expr)
 
     return std::move(expr);
   }
+  else if(expr.id() == ID_sva_if)
+  {
+    convert_expr(expr.op0());
+    make_boolean(expr.op0());
+
+    convert_expr(expr.op1());
+    make_boolean(expr.op1());
+
+    if(expr.op2().is_not_nil())
+    {
+      convert_expr(expr.op2());
+      make_boolean(expr.op2());
+    }
+
+    return std::move(expr);
+  }
   else
   {
     throw errort().with_location(expr.source_location())