Verilog: add all remaining property_expr rules from 1800-2017

regression/verilog/SVA/case1.desc

@@ -0,0 +1,10 @@
+CORE
+case1.sv
+--bound 20 --numbered-trace
+^\[main\.property\.p0\] always \(case\(main\.x\) 10: 0; endcase\): REFUTED$
+^Counterexample with 11 states:$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/SVA/case1.sv

@@ -0,0 +1,14 @@
+module main;
+
+  reg [31:0] x;
+  wire clk;
+
+  initial x=0;
+
+  always @(posedge clk)
+    x<=x+1;
+
+  // fails when x reaches 10
+  p0: assert property (case(x) 10: 0; endcase);
+
+endmodule

regression/verilog/SVA/strong1.desc

@@ -0,0 +1,9 @@
+CORE
+strong1.sv
+--bound 20
+^\[main\.property\.p0\] strong\(##\[0:9\] main\.x == 100\): REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/SVA/strong1.sv

@@ -0,0 +1,14 @@
+module main;
+
+  reg [31:0] x;
+  wire clk;
+
+  initial x=0;
+
+  always @(posedge clk)
+    x<=x+1;
+
+  // fails
+  initial p0: assert property (strong(##[0:9] x==100));
+
+endmodule

regression/verilog/SVA/weak1.desc

@@ -0,0 +1,9 @@
+CORE
+weak1.sv
+--bound 20
+^\[main\.property\.p0\] weak\(##\[0:9\] main\.x == 100\): REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/SVA/weak1.sv

@@ -0,0 +1,14 @@
+module main;
+
+  reg [31:0] x;
+  wire clk;
+
+  initial x=0;
+
+  always @(posedge clk)
+    x<=x+1;
+
+  // fails
+  initial p0: assert property (weak(##[0:9] x==100));
+
+endmodule

src/hw_cbmc_irep_ids.h

@@ -15,7 +15,10 @@ IREP_ID_ONE(F)
 IREP_ID_ONE(E)
 IREP_ID_ONE(G)
 IREP_ID_ONE(X)
+IREP_ID_ONE(sva_strong)
+IREP_ID_ONE(sva_weak)
 IREP_ID_ONE(sva_if)
+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)

src/temporal-logic/normalize_property.cpp

@@ -135,6 +135,18 @@ 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_strong)
+  {
+    expr = to_sva_strong_expr(expr).op();
+  }
+  else if(expr.id() == ID_sva_weak)
+  {
+    expr = to_sva_weak_expr(expr).op();
+  }
+  else if(expr.id() == ID_sva_case)
+  {
+    expr = to_sva_case_expr(expr).lowering();
+  }
 
   // normalize the operands
   for(auto &op : expr.operands())

src/temporal-logic/normalize_property.h

@@ -27,6 +27,9 @@ Author: Daniel Kroening, [email protected]
 /// ¬Fφ --> G¬φ
 /// [*] φ --> F φ
 /// [+] φ --> X F φ
+/// strong(φ) --> φ
+/// weak(φ) --> φ
+/// sva_case --> ? :
 exprt normalize_property(exprt);
 
 #endif

src/verilog/expr2verilog.cpp

@@ -407,6 +407,42 @@ std::string expr2verilogt::convert_sva_ranged_predicate(
 
 /*******************************************************************\
 
+Function: expr2verilogt::convert_sva_case
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+std::string expr2verilogt::convert_sva_case(const sva_case_exprt &src)
+{
+  std::string cases;
+
+  for(auto &case_item : src.case_items())
+  {
+    bool first = true;
+    for(auto &pattern : case_item.patterns())
+    {
+      if(first)
+        first = false;
+      else
+        cases += ", ";
+      cases += convert(pattern);
+    }
+
+    cases += ": ";
+    cases += convert(case_item.result());
+    cases += "; ";
+  }
+
+  return "case(" + convert(src.case_op()) + ") " + cases + "endcase";
+}
+
+/*******************************************************************\
+
 Function: expr2verilogt::convert_sva_unary
 
   Inputs:
@@ -1171,7 +1207,13 @@ std::string expr2verilogt::convert(
   else if(src.id()==ID_sva_cycle_delay)
     return convert_sva_cycle_delay(to_ternary_expr(src), precedence = 0);
     // not sure about precedence
-
+
+  else if(src.id() == ID_sva_strong)
+    return convert_function("strong", src);
+
+  else if(src.id() == ID_sva_weak)
+    return convert_function("weak", src);
+
   else if(src.id()==ID_sva_sequence_concatenation)
     return convert_sva_sequence_concatenation(
       to_binary_expr(src), precedence = 0);
@@ -1251,6 +1293,9 @@ std::string expr2verilogt::convert(
   else if(src.id() == ID_sva_if)
     return precedence = 0, convert_sva_if(to_sva_if_expr(src));
 
+  else if(src.id() == ID_sva_case)
+    return precedence = 0, convert_sva_case(to_sva_case_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_case_exprt;
 class sva_if_exprt;
 class sva_ranged_predicate_exprt;
 
@@ -85,6 +86,8 @@ class expr2verilogt
     const std::string &name,
     const exprt &src);
 
+  std::string convert_sva_case(const sva_case_exprt &);
+
   std::string convert_sva_ranged_predicate(
     const std::string &name,
     const sva_ranged_predicate_exprt &);

src/verilog/parser.y

@@ -2055,50 +2055,95 @@ property_expr:
 	;
 
 property_expr_proper:
-          '(' property_expr_proper ')'      { $$ = $2; }
-        | "not" property_expr               { init($$, ID_not); mto($$, $2); }
-        | property_expr "or" property_expr  { init($$, ID_or); mto($$, $1); mto($$, $3); }
-        | 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
+	  "strong" '(' sequence_expr ')'
+		{ init($$, ID_sva_strong); mto ($$, $3); }
+	| "weak" '(' sequence_expr ')'
+		{ init($$, ID_sva_weak); mto ($$, $3); }
+	| '(' property_expr_proper ')'
+		{ $$ = $2; }
+	| "not" property_expr
+		{ init($$, ID_not); mto($$, $2); }
+	| property_expr "or" property_expr
+		{ init($$, ID_or); mto($$, $1); mto($$, $3); }
+	| 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
+	| "if" '(' expression_or_dist ')' property_expr "else" property_expr
 		{ init($$, ID_sva_if); mto($$, $3); mto($$, $5); mto($$, $7); }
-        | sequence_expr "#-#" property_expr { init($$, ID_sva_overlapped_followed_by); mto($$, $1); mto($$, $3); }
-        | sequence_expr "#=#" property_expr { init($$, ID_sva_nonoverlapped_followed_by); mto($$, $1); mto($$, $3); }
-        | "nexttime" property_expr
+	| "case" '(' expression_or_dist ')' property_case_item_brace "endcase"
+		{ init($$, ID_sva_case); mto($$, $3); mto($$, $5); }
+	| sequence_expr "#-#" property_expr
+		{ init($$, ID_sva_overlapped_followed_by); mto($$, $1); mto($$, $3); }
+	| sequence_expr "#=#" property_expr
+		{ init($$, ID_sva_nonoverlapped_followed_by); mto($$, $1); mto($$, $3); }
+	| "nexttime" property_expr
 		{ init($$, "sva_nexttime"); stack_expr($$).add_to_operands(nil_exprt()); mto($$, $2); }
-        | "nexttime" '[' constant_expression ']' property_expr %prec "nexttime"
+	| "nexttime" '[' constant_expression ']' property_expr %prec "nexttime"
 		{ init($$, "sva_nexttime"); mto($$, $3); mto($$, $5); }
-        | "s_nexttime" property_expr
+	| "s_nexttime" property_expr
 		{ init($$, "sva_s_nexttime"); stack_expr($$).add_to_operands(nil_exprt()); mto($$, $2); }
-        | "s_nexttime" '[' constant_expression ']' property_expr %prec "s_nexttime"
+	| "s_nexttime" '[' constant_expression ']' property_expr %prec "s_nexttime"
 		{ init($$, "sva_s_nexttime"); mto($$, $3); mto($$, $5); }
-        | "always" '[' cycle_delay_const_range_expression ']' property_expr %prec "always"
+	| "always" '[' cycle_delay_const_range_expression ']' property_expr %prec "always"
 		{ init($$, ID_sva_ranged_always); swapop($$, $3); mto($$, $5); }
-        | "always" property_expr
+	| "always" property_expr
 		{ init($$, "sva_always"); mto($$, $2); }
-        | "s_always" '[' constant_range ']' property_expr %prec "s_always"
+	| "s_always" '[' constant_range ']' property_expr %prec "s_always"
 		{ init($$, ID_sva_s_always); swapop($$, $3); mto($$, $5); }
-        | "s_eventually" property_expr
+	| "s_eventually" property_expr
 		{ init($$, ID_sva_s_eventually); mto($$, $2); }
-        | "eventually" '[' constant_range ']' property_expr %prec "eventually"
+	| "eventually" '[' constant_range ']' property_expr %prec "eventually"
 		{ init($$, ID_sva_eventually); swapop($$, $3); mto($$, $5); }
-        | "s_eventually" '[' cycle_delay_const_range_expression ']' property_expr %prec "s_eventually"
+	| "s_eventually" '[' cycle_delay_const_range_expression ']' property_expr %prec "s_eventually"
 		{ init($$, ID_sva_s_eventually); swapop($$, $3); mto($$, $5); }
-        | property_expr "until" property_expr        { init($$, "sva_until"); mto($$, $1); mto($$, $3); }
-        | property_expr "until_with" property_expr   { init($$, "sva_until_with"); mto($$, $1); mto($$, $3); }
-        | property_expr "s_until" property_expr      { init($$, "sva_s_until"); mto($$, $1); mto($$, $3); }
-        | property_expr "s_until_with" property_expr { init($$, "sva_s_until_with"); mto($$, $1); mto($$, $3); }
-        | property_expr "implies" property_expr       { 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); }
-        | event_control property_expr { $$=$2; } %prec "property_expr_event_control"
-        ;
+	| property_expr "until" property_expr
+		{ init($$, "sva_until"); mto($$, $1); mto($$, $3); }
+	| property_expr "s_until" property_expr
+		{ init($$, "sva_s_until"); mto($$, $1); mto($$, $3); }
+	| property_expr "until_with" property_expr
+		{ init($$, "sva_until_with"); mto($$, $1); mto($$, $3); }
+	| property_expr "s_until_with" property_expr
+		{ init($$, "sva_s_until_with"); mto($$, $1); mto($$, $3); }
+	| property_expr "implies" property_expr
+		{ 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); }
+	| event_control property_expr { $$=$2; } %prec "property_expr_event_control"
+	;
+
+property_case_item_brace:
+	  property_case_item
+		{ init($$); mto($$, $1); }
+	| property_case_item_brace property_case_item
+		{ $$ = $1; mto($$, $2); }
+	;
+
+property_case_item:
+	  expression_or_dist_brace TOK_COLON property_expr ';'
+		{ init($$, ID_case_item); mto($$, $1); mto($$, $3); }
+	| "default" TOK_COLON property_expr ';'
+		{ init($$, ID_case_item); mto($$, $3); }
+	;
+
+expression_or_dist_brace:
+	  expression_or_dist
+		{ init($$, "patterns"); mto($$, $1); }
+	| expression_or_dist_brace ',' expression_or_dist
+		{ $$ = $1; mto($1, $3); }
+	;
 
 sequence_expr:
           expression

src/verilog/sva_expr.cpp

@@ -7,3 +7,31 @@ Author: Daniel Kroening, [email protected]
 \*******************************************************************/
 
 #include "sva_expr.h"
+
+exprt sva_case_exprt::lowering() const
+{
+  auto &case_items = this->case_items();
+
+  // base case
+  if(case_items.empty())
+    return true_exprt();
+
+  // remove one case item, then do recursive call
+  exprt::operandst disjuncts;
+  disjuncts.reserve(case_items.front().patterns().size());
+
+  for(auto &pattern : case_items.front().patterns())
+  {
+    disjuncts.push_back(equal_exprt{
+      typecast_exprt::conditional_cast(case_op(), pattern.type()), pattern});
+  }
+
+  sva_case_exprt reduced = *this;
+  reduced.case_items().erase(reduced.case_items().begin());
+
+  // rec. call
+  auto reduced_rec = reduced.lowering();
+
+  return if_exprt{
+    disjunction(disjuncts), case_items.front().result(), reduced_rec};
+}