SystemVerilog: cover property

kroening · kroening · commit 6de62b6d8d3b · 2024-03-24T16:58:07.000-07:00
This adds front-end support for cover property module items.
diff --git a/regression/verilog/SVA/cover1.desc 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
diff --git a/src/verilog/verilog_typecheck.h b/src/verilog/verilog_typecheck.h
