diff --git a/regression/verilog/SVA/case1.desc b/regression/verilog/SVA/case1.desc
new file mode 100644
index 000000000..aaea35756
--- /dev/null
+++ b/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
+--
diff --git a/regression/verilog/SVA/case1.sv b/regression/verilog/SVA/case1.sv
new file mode 100644
index 000000000..4cae30e5b
--- /dev/null
+++ b/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
diff --git a/regression/verilog/SVA/strong1.desc b/regression/verilog/SVA/strong1.desc
new file mode 100644
index 000000000..835a83573
--- /dev/null
+++ b/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
+--
diff --git a/regression/verilog/SVA/strong1.sv b/regression/verilog/SVA/strong1.sv
new file mode 100644
index 000000000..20231c2be
--- /dev/null
+++ b/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
diff --git a/regression/verilog/SVA/weak1.desc b/regression/verilog/SVA/weak1.desc
new file mode 100644
index 000000000..57705fb38
--- /dev/null
+++ b/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
+--
diff --git a/regression/verilog/SVA/weak1.sv b/regression/verilog/SVA/weak1.sv
new file mode 100644
index 000000000..25da5ba93
--- /dev/null
+++ b/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
diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h
index 221503787..bc38a0839 100644
--- a/src/hw_cbmc_irep_ids.h
+++ b/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)
diff --git a/src/temporal-logic/normalize_property.cpp b/src/temporal-logic/normalize_property.cpp
index 52589e00f..bb600b77b 100644
--- a/src/temporal-logic/normalize_property.cpp
+++ b/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())
diff --git a/src/temporal-logic/normalize_property.h b/src/temporal-logic/normalize_property.h
index 01a4cd322..1aeacf072 100644
--- a/src/temporal-logic/normalize_property.h
+++ b/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
diff --git a/src/verilog/expr2verilog.cpp b/src/verilog/expr2verilog.cpp
index aab077656..97dd5cf46 100644
--- a/src/verilog/expr2verilog.cpp
+++ b/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));
 
diff --git a/src/verilog/expr2verilog_class.h b/src/verilog/expr2verilog_class.h
index 470bcdf4e..648ff10c2 100644
--- a/src/verilog/expr2verilog_class.h
+++ b/src/verilog/expr2verilog_class.h
@@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #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 &);
diff --git a/src/verilog/parser.y b/src/verilog/parser.y
index f403c12d9..1804fc2a6 100644
--- a/src/verilog/parser.y
+++ b/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
diff --git a/src/verilog/sva_expr.cpp b/src/verilog/sva_expr.cpp
index 56b603dd8..50f82b650 100644
--- a/src/verilog/sva_expr.cpp
+++ b/src/verilog/sva_expr.cpp
@@ -7,3 +7,31 @@ Author: Daniel Kroening, kroening@kroening.com
 \*******************************************************************/
 
 #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};
+}
diff --git a/src/verilog/sva_expr.h b/src/verilog/sva_expr.h
index a8a9e1e6a..f14fdb988 100644
--- a/src/verilog/sva_expr.h
+++ b/src/verilog/sva_expr.h
@@ -695,4 +695,126 @@ static inline sva_if_exprt &to_sva_if_expr(exprt &expr)
   return static_cast<sva_if_exprt &>(expr);
 }
 
+class sva_strong_exprt : public unary_exprt
+{
+public:
+  sva_strong_exprt(exprt __op, typet __type)
+    : unary_exprt(ID_sva_strong, std::move(__op), std::move(__type))
+  {
+  }
+};
+
+inline const sva_strong_exprt &to_sva_strong_expr(const exprt &expr)
+{
+  sva_strong_exprt::check(expr);
+  return static_cast<const sva_strong_exprt &>(expr);
+}
+
+inline sva_strong_exprt &to_sva_strong_expr(exprt &expr)
+{
+  sva_strong_exprt::check(expr);
+  return static_cast<sva_strong_exprt &>(expr);
+}
+
+class sva_weak_exprt : public unary_exprt
+{
+public:
+  sva_weak_exprt(exprt __op, typet __type)
+    : unary_exprt(ID_sva_weak, std::move(__op), std::move(__type))
+  {
+  }
+};
+
+inline const sva_weak_exprt &to_sva_weak_expr(const exprt &expr)
+{
+  sva_weak_exprt::check(expr);
+  return static_cast<const sva_weak_exprt &>(expr);
+}
+
+inline sva_weak_exprt &to_sva_weak_expr(exprt &expr)
+{
+  sva_weak_exprt::check(expr);
+  return static_cast<sva_weak_exprt &>(expr);
+}
+
+class sva_case_exprt : public binary_predicate_exprt
+{
+public:
+  explicit sva_case_exprt(exprt __case_op, exprt __cases)
+    : binary_predicate_exprt(
+        std::move(__case_op),
+        ID_sva_case,
+        std::move(__cases))
+  {
+  }
+
+  const exprt &case_op() const
+  {
+    return op0();
+  }
+
+  exprt &case_op()
+  {
+    return op0();
+  }
+
+  class case_itemt : public binary_exprt
+  {
+  public:
+    const exprt::operandst &patterns() const
+    {
+      return op0().operands();
+    }
+
+    exprt::operandst &patterns()
+    {
+      return op0().operands();
+    }
+
+    const exprt &result() const
+    {
+      return op1();
+    }
+
+    exprt &result()
+    {
+      return op1();
+    }
+
+  protected:
+    using binary_exprt::op0;
+    using binary_exprt::op1;
+  };
+
+  using case_itemst = std::vector<case_itemt>;
+
+  const case_itemst &case_items() const
+  {
+    return (const case_itemst &)(op1().operands());
+  }
+
+  case_itemst &case_items()
+  {
+    return (case_itemst &)(op1().operands());
+  }
+
+  exprt lowering() const;
+
+protected:
+  using binary_predicate_exprt::op0;
+  using binary_predicate_exprt::op1;
+};
+
+inline const sva_case_exprt &to_sva_case_expr(const exprt &expr)
+{
+  sva_case_exprt::check(expr);
+  return static_cast<const sva_case_exprt &>(expr);
+}
+
+inline sva_case_exprt &to_sva_case_expr(exprt &expr)
+{
+  sva_case_exprt::check(expr);
+  return static_cast<sva_case_exprt &>(expr);
+}
+
 #endif
diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp
index 72c5c3853..62aa6cff9 100644
--- a/src/verilog/verilog_typecheck_expr.cpp
+++ b/src/verilog/verilog_typecheck_expr.cpp
@@ -1907,7 +1907,8 @@ exprt verilog_typecheck_exprt::convert_unary_expr(unary_exprt expr)
   else if(
     expr.id() == ID_sva_always || expr.id() == ID_sva_s_eventually ||
     expr.id() == ID_sva_cycle_delay_plus ||
-    expr.id() == ID_sva_cycle_delay_star)
+    expr.id() == ID_sva_cycle_delay_star || expr.id() == ID_sva_weak ||
+    expr.id() == ID_sva_strong)
   {
     assert(expr.operands().size()==1);
     convert_expr(expr.op());
@@ -2321,6 +2322,28 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr)
         << "cannot perform size cast on " << to_string(op_type);
     }
   }
+  else if(expr.id() == ID_sva_case)
+  {
+    auto &case_expr = to_sva_case_expr(expr);
+    convert_expr(case_expr.case_op());
+
+    for(auto &case_item : case_expr.case_items())
+    {
+      // same rules as case statement
+      for(auto &pattern : case_item.patterns())
+      {
+        convert_expr(pattern);
+        typet t = max_type(pattern.type(), case_expr.case_op().type());
+        propagate_type(pattern, t);
+      }
+
+      convert_expr(case_item.result());
+      make_boolean(case_item.result());
+    }
+
+    expr.type() = bool_typet();
+    return std::move(expr);
+  }
   else
   {
     // type is guessed for now