diff --git a/regression/verilog/SVA/cover1.desc b/regression/verilog/SVA/cover1.desc
new file mode 100644
index 000000000..93180a052
--- /dev/null
+++ b/regression/verilog/SVA/cover1.desc
@@ -0,0 +1,11 @@
+KNOWNBUG
+cover1.sv
+--bound 10
+^\[main\.property\.p0\] cover main\.counter == 1: REFUTED$
+^\[main\.property\.p1\] cover main\.counter == 100: REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Back-end support is missing.
diff --git a/regression/verilog/SVA/cover1.sv b/regression/verilog/SVA/cover1.sv
new file mode 100644
index 000000000..fbdece9d8
--- /dev/null
+++ b/regression/verilog/SVA/cover1.sv
@@ -0,0 +1,20 @@
+module main(input clk);
+
+  // count up from 0 to 10
+  reg [7:0] counter;
+
+  initial counter = 0;
+
+  always @(posedge clk)
+    if(counter == 10)
+      counter = 0;
+    else
+      counter = counter + 1;
+
+  // expected to pass
+  p0: cover property (counter == 1);
+
+  // expected to fail
+  p1: cover property (counter == 100);
+
+endmodule
diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h
index 2a650aa0d..17de86ce5 100644
--- a/src/hw_cbmc_irep_ids.h
+++ b/src/hw_cbmc_irep_ids.h
@@ -16,6 +16,7 @@ IREP_ID_ONE(sva_sequence_throughout)
 IREP_ID_ONE(sva_sequence_concatenation)
 IREP_ID_ONE(sva_sequence_first_match)
 IREP_ID_ONE(sva_always)
+IREP_ID_ONE(sva_cover)
 IREP_ID_ONE(sva_nexttime)
 IREP_ID_ONE(sva_s_nexttime)
 IREP_ID_ONE(sva_eventually)
diff --git a/src/verilog/expr2verilog.cpp b/src/verilog/expr2verilog.cpp
index 58620a909..bb967f162 100644
--- a/src/verilog/expr2verilog.cpp
+++ b/src/verilog/expr2verilog.cpp
@@ -1088,6 +1088,9 @@ std::string expr2verilogt::convert(
   else if(src.id()==ID_sva_always)
     return precedence = 0, convert_sva("always", to_sva_always_expr(src).op());
 
+  else if(src.id() == ID_sva_cover)
+    return precedence = 0, convert_sva("cover", to_sva_cover_expr(src).op());
+
   else if(src.id()==ID_sva_nexttime)
     return precedence = 0,
            convert_sva("nexttime", to_sva_nexttime_expr(src).op());
diff --git a/src/verilog/sva_expr.h b/src/verilog/sva_expr.h
index 1ed1bb685..7f7942219 100644
--- a/src/verilog/sva_expr.h
+++ b/src/verilog/sva_expr.h
@@ -170,6 +170,29 @@ static inline sva_always_exprt &to_sva_always_expr(exprt &expr)
   return static_cast<sva_always_exprt &>(expr);
 }
 
+class sva_cover_exprt : public unary_predicate_exprt
+{
+public:
+  explicit sva_cover_exprt(exprt op)
+    : unary_predicate_exprt(ID_sva_cover, std::move(op))
+  {
+  }
+};
+
+static inline const sva_cover_exprt &to_sva_cover_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_sva_cover);
+  sva_cover_exprt::check(expr, validation_modet::INVARIANT);
+  return static_cast<const sva_cover_exprt &>(expr);
+}
+
+static inline sva_cover_exprt &to_sva_cover_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_sva_cover);
+  sva_cover_exprt::check(expr, validation_modet::INVARIANT);
+  return static_cast<sva_cover_exprt &>(expr);
+}
+
 class sva_until_exprt : public binary_predicate_exprt
 {
 public:
diff --git a/src/verilog/verilog_expr.h b/src/verilog/verilog_expr.h
index af5a39c0f..bdabd2abe 100644
--- a/src/verilog/verilog_expr.h
+++ b/src/verilog/verilog_expr.h
@@ -1603,14 +1603,19 @@ inline verilog_non_blocking_assignt &to_verilog_non_blocking_assign(exprt &expr)
   return static_cast<verilog_non_blocking_assignt &>(expr);
 }
 
-/// Verilog concurrent assertion module item
-class verilog_assert_module_itemt : public verilog_module_itemt
+/// Verilog assert/assume/cover property module item
+class verilog_assert_assume_cover_module_itemt : public verilog_module_itemt
 {
 public:
-  verilog_assert_module_itemt()
-    : verilog_module_itemt(ID_verilog_assert_property)
+  verilog_assert_assume_cover_module_itemt(
+    irep_idt __id,
+    exprt __condition,
+    verilog_statementt __action)
+    : verilog_module_itemt(__id)
   {
     operands().resize(2);
+    condition() = std::move(__condition);
+    action() = std::move(__action);
   }
   
   inline exprt &condition()
@@ -1623,51 +1628,14 @@ class verilog_assert_module_itemt : public verilog_module_itemt
     return op0();
   }
 
-  const irep_idt &identifier() const
+  inline exprt &action()
   {
-    return get(ID_identifier);
-  }
-
-  void identifier(irep_idt __identifier)
-  {
-    set(ID_identifier, __identifier);
-  }
-};
-
-inline const verilog_assert_module_itemt &
-to_verilog_assert_module_item(const verilog_module_itemt &module_item)
-{
-  PRECONDITION(module_item.id() == ID_verilog_assert_property);
-  binary_exprt::check(module_item);
-  return static_cast<const verilog_assert_module_itemt &>(module_item);
-}
-
-inline verilog_assert_module_itemt &
-to_verilog_assert_module_item(verilog_module_itemt &module_item)
-{
-  PRECONDITION(module_item.id() == ID_verilog_assert_property);
-  binary_exprt::check(module_item);
-  return static_cast<verilog_assert_module_itemt &>(module_item);
-}
-
-/// Verilog concurrent assumption module item
-class verilog_assume_module_itemt : public verilog_module_itemt
-{
-public:
-  verilog_assume_module_itemt()
-    : verilog_module_itemt(ID_verilog_assume_property)
-  {
-    operands().resize(2);
-  }
-
-  inline exprt &condition()
-  {
-    return op0();
+    return op1();
   }
 
-  inline const exprt &condition() const
+  inline const exprt &action() const
   {
-    return op0();
+    return op1();
   }
 
   const irep_idt &identifier() const
@@ -1681,20 +1649,28 @@ class verilog_assume_module_itemt : public verilog_module_itemt
   }
 };
 
-inline const verilog_assume_module_itemt &
-to_verilog_assume_module_item(const verilog_module_itemt &module_item)
+inline const verilog_assert_assume_cover_module_itemt &
+to_verilog_assert_assume_cover_module_item(
+  const verilog_module_itemt &module_item)
 {
-  PRECONDITION(module_item.id() == ID_verilog_assume_property);
+  PRECONDITION(
+    module_item.id() == ID_verilog_assert_property ||
+    module_item.id() == ID_verilog_assume_property ||
+    module_item.id() == ID_verilog_cover_property);
   binary_exprt::check(module_item);
-  return static_cast<const verilog_assume_module_itemt &>(module_item);
+  return static_cast<const verilog_assert_assume_cover_module_itemt &>(
+    module_item);
 }
 
-inline verilog_assume_module_itemt &
-to_verilog_assume_module_item(verilog_module_itemt &module_item)
+inline verilog_assert_assume_cover_module_itemt &
+to_verilog_assert_assume_cover_module_item(verilog_module_itemt &module_item)
 {
-  PRECONDITION(module_item.id() == ID_verilog_assume_property);
+  PRECONDITION(
+    module_item.id() == ID_verilog_assert_property ||
+    module_item.id() == ID_verilog_assume_property ||
+    module_item.id() == ID_verilog_cover_property);
   binary_exprt::check(module_item);
-  return static_cast<verilog_assume_module_itemt &>(module_item);
+  return static_cast<verilog_assert_assume_cover_module_itemt &>(module_item);
 }
 
 // Can be one of three:
diff --git a/src/verilog/verilog_synthesis.cpp b/src/verilog/verilog_synthesis.cpp
index 98dd2da85..5f2a25942 100644
--- a/src/verilog/verilog_synthesis.cpp
+++ b/src/verilog/verilog_synthesis.cpp
@@ -1838,8 +1838,8 @@ Function: verilog_synthesist::synth_assert
 
 \*******************************************************************/
 
-void verilog_synthesist::synth_assert(
-  const verilog_assert_module_itemt &module_item)
+void verilog_synthesist::synth_assert_cover(
+  const verilog_assert_assume_cover_module_itemt &module_item)
 {
   const irep_idt &identifier = module_item.identifier();
   symbolt &symbol=symbol_table_lookup(identifier);
@@ -1848,9 +1848,19 @@ void verilog_synthesist::synth_assert(
 
   auto cond = synth_expr(module_item.condition(), symbol_statet::SYMBOL);
 
-  // concurrent assertions come with an implicit 'always'
-  if(cond.id() != ID_sva_always)
-    cond = sva_always_exprt(cond);
+  if(module_item.id() == ID_verilog_assert_property)
+  {
+    // Concurrent assertions come with an implicit 'always'.
+    if(cond.id() != ID_sva_always)
+      cond = sva_always_exprt(cond);
+  }
+  else if(module_item.id() == ID_verilog_cover_property)
+  {
+    // 'cover' requirements are existential.
+    cond = sva_cover_exprt(cond);
+  }
+  else
+    PRECONDITION(false);
 
   symbol.value = std::move(cond);
 }
@@ -1891,7 +1901,7 @@ Function: verilog_synthesist::synth_assume
 \*******************************************************************/
 
 void verilog_synthesist::synth_assume(
-  const verilog_assume_module_itemt &module_item)
+  const verilog_assert_assume_cover_module_itemt &module_item)
 {
   auto condition = synth_expr(to_binary_expr(module_item).op0(), symbol_statet::SYMBOL);
 
@@ -2688,10 +2698,16 @@ void verilog_synthesist::synth_module_item(
       synth_module_item(block_item, trans);
     }
   }
-  else if(module_item.id() == ID_verilog_assert_property)
-    synth_assert(to_verilog_assert_module_item(module_item));
+  else if(
+    module_item.id() == ID_verilog_assert_property ||
+    module_item.id() == ID_verilog_cover_property)
+  {
+    synth_assert_cover(to_verilog_assert_assume_cover_module_item(module_item));
+  }
   else if(module_item.id() == ID_verilog_assume_property)
-    synth_assume(to_verilog_assume_module_item(module_item));
+  {
+    synth_assume(to_verilog_assert_assume_cover_module_item(module_item));
+  }
   else if(module_item.id()==ID_task)
   {
     // ignore for now
diff --git a/src/verilog/verilog_synthesis_class.h b/src/verilog/verilog_synthesis_class.h
index 905a287a5..bc42d8556 100644
--- a/src/verilog/verilog_synthesis_class.h
+++ b/src/verilog/verilog_synthesis_class.h
@@ -220,8 +220,8 @@ class verilog_synthesist:
   void synth_module_item(const verilog_module_itemt &, transt &);
   void synth_always_base(const verilog_always_baset &);
   void synth_initial(const verilog_initialt &);
-  void synth_assert(const verilog_assert_module_itemt &);
-  void synth_assume(const verilog_assume_module_itemt &);
+  void synth_assert_cover(const verilog_assert_assume_cover_module_itemt &);
+  void synth_assume(const verilog_assert_assume_cover_module_itemt &);
   void synth_continuous_assign(const verilog_continuous_assignt &);
   void synth_force_rec(exprt &lhs, exprt &rhs, transt &);
   void synth_module_instance(const verilog_instt &, transt &);
diff --git a/src/verilog/verilog_typecheck.cpp b/src/verilog/verilog_typecheck.cpp
index 64ba592b5..ca1399973 100644
--- a/src/verilog/verilog_typecheck.cpp
+++ b/src/verilog/verilog_typecheck.cpp
@@ -993,7 +993,7 @@ void verilog_typecheckt::convert_assign(
 
 /*******************************************************************\
 
-Function: verilog_typecheckt::convert_assert
+Function: verilog_typecheckt::convert_assert_assume_cover
 
   Inputs:
 
@@ -1003,73 +1003,54 @@ Function: verilog_typecheckt::convert_assert
 
 \*******************************************************************/
 
-void verilog_typecheckt::convert_assert(
-  verilog_assert_module_itemt &module_item)
+void verilog_typecheckt::convert_assert_assume_cover(
+  verilog_assert_assume_cover_module_itemt &module_item)
 {
   exprt &cond = module_item.condition();
 
   convert_expr(cond);
   make_boolean(cond);
 
-  // We create a symbol for the property.
-  // The 'value' of the symbol is set by synthesis.
-  const irep_idt &identifier = module_item.identifier();
-
-  irep_idt base_name;
-
-  if(identifier == irep_idt())
-  {
-    assertion_counter++;
-    base_name=std::to_string(assertion_counter);
-  }
-  else
-    base_name=identifier;
-  
-  std::string full_identifier=
-    id2string(module_identifier)+
-    ".property."+id2string(base_name);
-
-  if(symbol_table.symbols.find(full_identifier)!=
-     symbol_table.symbols.end())
+  if(
+    module_item.id() == ID_verilog_assert_property ||
+    module_item.id() == ID_verilog_cover_property)
   {
-    throw errort().with_location(module_item.source_location())
-      << "property identifier `" << base_name << "' already used";
-  }
-
-  module_item.identifier(full_identifier);
-
-  symbolt symbol{base_name, bool_typet{}, mode};
-
-  symbol.module=module_identifier;
-  symbol.value = nil_exprt{}; // set by synthesis
-  symbol.name = full_identifier;
-  symbol.is_property=true;
-  symbol.location = module_item.find_source_location();
-  symbol.pretty_name=strip_verilog_prefix(full_identifier);
-
-  symbolt *new_symbol;
-  symbol_table.move(symbol, new_symbol);
-}
+    // We create a symbol for the property.
+    // The 'value' of the symbol is set by synthesis.
+    const irep_idt &identifier = module_item.identifier();
 
-/*******************************************************************\
+    irep_idt base_name;
 
-Function: verilog_typecheckt::convert_assume_property
+    if(identifier == irep_idt())
+    {
+      assertion_counter++;
+      base_name = std::to_string(assertion_counter);
+    }
+    else
+      base_name = identifier;
 
-  Inputs:
+    std::string full_identifier =
+      id2string(module_identifier) + ".property." + id2string(base_name);
 
- Outputs:
+    if(symbol_table.symbols.find(full_identifier) != symbol_table.symbols.end())
+    {
+      throw errort().with_location(module_item.source_location())
+        << "property identifier `" << base_name << "' already used";
+    }
 
- Purpose:
+    module_item.identifier(full_identifier);
 
-\*******************************************************************/
+    symbolt symbol{base_name, bool_typet{}, mode};
 
-void verilog_typecheckt::convert_assume(
-  verilog_assume_module_itemt &module_item)
-{
-  exprt &cond = module_item.condition();
+    symbol.module = module_identifier;
+    symbol.value = nil_exprt{}; // set by synthesis
+    symbol.name = full_identifier;
+    symbol.is_property = true;
+    symbol.location = module_item.find_source_location();
+    symbol.pretty_name = strip_verilog_prefix(full_identifier);
 
-  convert_expr(cond);
-  make_boolean(cond);
+    symbol_table.insert(std::move(symbol));
+  }
 }
 
 /*******************************************************************\
@@ -1538,12 +1519,12 @@ void verilog_typecheckt::convert_module_item(
   }
   else if(
     module_item.id() == ID_verilog_assert_property ||
-    module_item.id() == ID_verilog_smv_assert)
-    convert_assert(to_verilog_assert_module_item(module_item));
-  else if(
     module_item.id() == ID_verilog_assume_property ||
-    module_item.id() == ID_verilog_smv_assume)
-    convert_assume(to_verilog_assume_module_item(module_item));
+    module_item.id() == ID_verilog_cover_property)
+  {
+    convert_assert_assume_cover(
+      to_verilog_assert_assume_cover_module_item(module_item));
+  }
   else if(module_item.id()==ID_initial)
     convert_initial(to_verilog_initial(module_item));
   else if(module_item.id()==ID_continuous_assign)
diff --git a/src/verilog/verilog_typecheck.h b/src/verilog/verilog_typecheck.h
index ae8d48508..9bafda488 100644
--- a/src/verilog/verilog_typecheck.h
+++ b/src/verilog/verilog_typecheck.h
@@ -163,8 +163,7 @@ class verilog_typecheckt:
   void convert_always_base(class verilog_always_baset &);
   void convert_initial(class verilog_initialt &);
   void convert_continuous_assign(class verilog_continuous_assignt &);
-  void convert_assert(verilog_assert_module_itemt &);
-  void convert_assume(verilog_assume_module_itemt &);
+  void convert_assert_assume_cover(verilog_assert_assume_cover_module_itemt &);
   void check_lhs(const exprt &lhs, vassignt vassign);
   void convert_assignments(exprt &trans);
   void convert_module_item(class verilog_module_itemt &);