Verilog: add all remaining property_expr rules from 1800-2017

This adds all remaining property_expr productions given in IEEE 1800-2017:
* strong
* weak
* case

Author: kroening

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, dkr@amazon.com
 /// ¬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));