SystemVerilog: distinguish assertions

This changes the front-end to distinguish three kinds of assertions/assumptions:

1) concurrent assertions/assumptions ("assert property"), which can be
module items or statements,

2) immediate assertion/assumption statements, and

3) SMV-style assertions/assumptions.

Front-end and BMC back-end support for initial concurrent assertion
statements is added.

regression/ebmc/Output-Register-Passing/main.v

@@ -13,12 +13,12 @@ module main(in1, in2);
 
  and1 A1 (in1, in2, o1, o2);             
 
- assert property1: o1 == (in1 & in2);
+ always assert property1: o1 == (in1 & in2);
 /* A2 is another instance of      
 ports are referenced to the       
 declaration by name. */           
  and1 A2 (.c(o1),.d(o2),.a(o1),.b(in2)); 
- assert property2: o1 == (in1 & in2);
+ always assert property2: o1 == (in1 & in2);
 endmodule                       
 
 // MODULE DEFINITION              

regression/ebmc/smv/initial1.desc

@@ -0,0 +1,9 @@
+CORE
+initial1.smv
+--bound 0
+^\[main::spec1\] main::var::tmp1 = TRUE: PROVED up to bound 0$
+^\[main::spec2\] main::var::tmp2 = TRUE: REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/ebmc/smv/initial1.smv

@@ -0,0 +1,12 @@
+MODULE main
+
+VAR tmp1: boolean;
+VAR tmp2: boolean;
+
+ASSIGN init(tmp1):=1;
+
+-- should pass
+SPEC tmp1 = 1;
+
+-- should fail
+SPEC tmp2 = 1;

regression/verilog/SVA/initial1.desc

@@ -1,9 +1,13 @@
-KNOWNBUG
+CORE
 initial1.sv
 --module main --bound 1
-^EXIT=0$
+^\[main\.property\.1\] main\.counter == 0: PROVED up to bound 1$
+^\[main\.property\.2\] main\.counter == 100: REFUTED$
+^\[main\.property\.3\] ##1 main\.counter == 1: PROVED up to bound 1$
+^\[main\.property\.4\] ##1 main\.counter == 100: REFUTED$
+^\[main\.property\.5\] s_nexttime main\.counter == 1: PROVED up to bound 1$
+^EXIT=10$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-Syntax is missing for initial label: assert property (...);

regression/verilog/SVA/initial1.sv

@@ -14,7 +14,16 @@ module main(input clk);
   // expected to pass
   initial p0: assert property (counter == 0);
 
+  // expected to fail
+  initial p1: assert property (counter == 100);
+
+  // expected to pass
+  initial p2: assert property (##1 counter == 1);
+
+  // expected to fail
+  initial p2: assert property (##1 counter == 100);
+
   // expected to pass if there are timeframes 0 and 1
-  initial p1: assert property (s_nexttime counter == 1);
+  initial p3: assert property (s_nexttime counter == 1);
 
 endmodule

regression/verilog/modules/parameters2.v

@@ -10,7 +10,7 @@ module test(in1, in2);
 
   my_m #( .Ptop(P), .Qtop(Q) ) m_instance(in1, in2, o1, o2); 
 
-  assert property1: tmp == 4; // should pass
+  always assert property1: tmp == 4; // should pass
 
 endmodule                       
 
@@ -25,6 +25,6 @@ module my_m(a, b, c, d);
 
   wire [3:0] tmp_in_m = Ptop; // tmp1 should be 4 now  
 
-  assert property2: tmp_in_m == 4; // should pass
+  always assert property2: tmp_in_m == 4; // should pass
 
 endmodule

regression/verilog/tasks/tasks1.v

@@ -12,6 +12,6 @@ module main;
     some_task(x, y);
   end
 
-  assert p1: y==x+1;
+  always assert p1: y==x+1;
 
 endmodule

src/hw-cbmc/Makefile

@@ -35,6 +35,7 @@ OBJ+= $(CPROVER_DIR)/goto-checker/goto-checker$(LIBEXT) \
       $(CPROVER_DIR)/solvers/solvers$(LIBEXT) \
       $(CPROVER_DIR)/util/util$(LIBEXT) \
       $(CPROVER_DIR)/json/json$(LIBEXT) \
+      ../temporal-logic/temporal-logic$(LIBEXT) \
       ../trans-netlist/trans_trace$(OBJEXT) \
       ../trans-word-level/trans-word-level$(LIBEXT)
 

src/hw_cbmc_irep_ids.h

@@ -66,6 +66,11 @@ IREP_ID_ONE(force)
 IREP_ID_ONE(deassign)
 IREP_ID_ONE(continuous_assign)
 IREP_ID_ONE(wait)
+IREP_ID_ONE(verilog_assert_property)
+IREP_ID_ONE(verilog_assume_property)
+IREP_ID_ONE(verilog_cover_property)
+IREP_ID_ONE(verilog_smv_assert)
+IREP_ID_ONE(verilog_smv_assume)
 IREP_ID_ONE(verilog_always)
 IREP_ID_ONE(verilog_always_comb)
 IREP_ID_ONE(verilog_always_ff)
@@ -76,7 +81,6 @@ IREP_ID_ONE(initial)
 IREP_ID_ONE(verilog_label_statement)
 IREP_ID_ONE(disable)
 IREP_ID_ONE(fork)
-IREP_ID_ONE(cover)
 IREP_ID_ONE(instance)
 IREP_ID_ONE(named_parameter_assignment)
 IREP_ID_ONE(parameter_assignment)

src/temporal-logic/temporal_logic.cpp

@@ -10,31 +10,28 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/expr_iterator.h>
 
+bool is_temporal_operator(const exprt &expr)
+{
+  return expr.id() == ID_AG || expr.id() == ID_EG || expr.id() == ID_AF ||
+         expr.id() == ID_EF || expr.id() == ID_AX || expr.id() == ID_EX ||
+         expr.id() == ID_A || expr.id() == ID_E || expr.id() == ID_U ||
+         expr.id() == ID_R || expr.id() == ID_G || expr.id() == ID_F ||
+         expr.id() == ID_X || expr.id() == ID_sva_always ||
+         expr.id() == ID_sva_always || expr.id() == ID_sva_nexttime ||
+         expr.id() == ID_sva_s_nexttime || expr.id() == ID_sva_until ||
+         expr.id() == ID_sva_s_until || expr.id() == ID_sva_until_with ||
+         expr.id() == ID_sva_s_until_with || expr.id() == ID_sva_eventually ||
+         expr.id() == ID_sva_s_eventually || expr.id() == ID_sva_cycle_delay;
+}
+
 bool has_temporal_operator(const exprt &expr)
 {
   for(auto subexpr_it = expr.depth_cbegin(), subexpr_end = expr.depth_cend();
       subexpr_it != subexpr_end;
       subexpr_it++)
   {
-    // clang-format off
-    if(
-      subexpr_it->id() == ID_AG || subexpr_it->id() == ID_EG ||
-      subexpr_it->id() == ID_AF || subexpr_it->id() == ID_EF ||
-      subexpr_it->id() == ID_AX || subexpr_it->id() == ID_EX ||
-      subexpr_it->id() == ID_A || subexpr_it->id() == ID_E ||
-      subexpr_it->id() == ID_U || subexpr_it->id() == ID_R ||
-      subexpr_it->id() == ID_G || subexpr_it->id() == ID_F ||
-      subexpr_it->id() == ID_X ||
-      subexpr_it->id() == ID_sva_always || subexpr_it->id() == ID_sva_always ||
-      subexpr_it->id() == ID_sva_nexttime || subexpr_it->id() == ID_sva_s_nexttime ||
-      subexpr_it->id() == ID_sva_until || subexpr_it->id() == ID_sva_s_until ||
-      subexpr_it->id() == ID_sva_until_with || subexpr_it->id() == ID_sva_s_until_with ||
-      subexpr_it->id() == ID_sva_eventually ||
-      subexpr_it->id() == ID_sva_s_eventually)
-    {
+    if(is_temporal_operator(*subexpr_it))
       return true;
-    }
-    // clang-format on
   }
 
   return false;

src/temporal-logic/temporal_logic.h

@@ -14,4 +14,8 @@ Author: Daniel Kroening, [email protected]
 /// Returns true iff the given expression contains a temporal operator
 bool has_temporal_operator(const exprt &);
 
+/// Returns true iff the given expression has a temporal operator
+/// as its root
+bool is_temporal_operator(const exprt &);
+
 #endif

src/trans-word-level/instantiate_word_level.cpp

@@ -148,60 +148,55 @@ exprt wl_instantiatet::instantiate_rec(exprt expr, const mp_integer &t) const
   }
   else if(expr.id()==ID_sva_cycle_delay) // ##[1:2] something
   {
-    if(expr.operands().size()==3)
+    auto &sva_cycle_delay_expr = to_sva_cycle_delay_expr(expr);
+
+    if(sva_cycle_delay_expr.to().is_nil())
     {
-      auto &ternary_expr = to_ternary_expr(expr);
+      mp_integer offset;
+      if(to_integer_non_constant(sva_cycle_delay_expr.from(), offset))
+        throw "failed to convert sva_cycle_delay offset";
 
-      if(ternary_expr.op1().is_nil())
-      {
-        mp_integer offset;
-        if(to_integer_non_constant(ternary_expr.op0(), offset))
-          throw "failed to convert sva_cycle_delay offset";
+      const auto u = t + offset;
 
-        const auto u = t + offset;
+      // Do we exceed the bound? Make it 'true'
+      if(u >= no_timeframes)
+        return true_exprt();
+      else
+        return instantiate_rec(sva_cycle_delay_expr.op(), u);
+    }
+    else
+    {
+      mp_integer from, to;
+      if(to_integer_non_constant(sva_cycle_delay_expr.from(), from))
+        throw "failed to convert sva_cycle_delay offsets";
 
-        // Do we exceed the bound? Make it 'true'
-        if(u >= no_timeframes)
-          return true_exprt();
-        else
-          return instantiate_rec(ternary_expr.op2(), u);
+      if(sva_cycle_delay_expr.to().id() == ID_infinity)
+      {
+        assert(no_timeframes != 0);
+        to = no_timeframes - 1;
       }
-      else
+      else if(to_integer_non_constant(sva_cycle_delay_expr.to(), to))
+        throw "failed to convert sva_cycle_delay offsets";
+
+      // This is an 'or', and we let it fail if the bound is too small.
+
+      exprt::operandst disjuncts;
+
+      for(mp_integer offset = from; offset < to; ++offset)
       {
-        mp_integer from, to;
-        if(to_integer_non_constant(ternary_expr.op0(), from))
-          throw "failed to convert sva_cycle_delay offsets";
+        auto u = t + offset;
 
-        if(ternary_expr.op1().id() == ID_infinity)
+        if(u >= no_timeframes)
         {
-          assert(no_timeframes!=0);
-          to=no_timeframes-1;
         }
-        else if(to_integer_non_constant(ternary_expr.op1(), to))
-          throw "failed to convert sva_cycle_delay offsets";
-
-        // This is an 'or', and we let it fail if the bound is too small.
-
-        exprt::operandst disjuncts;
-
-        for(mp_integer offset=from; offset<to; ++offset)
+        else
         {
-          auto u = t + offset;
-
-          if(u >= no_timeframes)
-          {
-          }
-          else
-          {
-            disjuncts.push_back(instantiate_rec(ternary_expr.op2(), u));
-          }
+          disjuncts.push_back(instantiate_rec(sva_cycle_delay_expr.op(), u));
         }
-
-        return disjunction(disjuncts);
       }
+
+      return disjunction(disjuncts);
     }
-    else
-      return expr;
   }
   else if(expr.id()==ID_sva_sequence_concatenation)
   {

src/trans-word-level/property.cpp

@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/symbol_table.h>
 
 #include <temporal-logic/temporal_expr.h>
+#include <temporal-logic/temporal_logic.h>
 #include <verilog/sva_expr.h>
 
 #include "instantiate_word_level.h"
@@ -34,8 +35,19 @@ Function: bmc_supports_property
 
 bool bmc_supports_property(const exprt &expr)
 {
-  if(expr.is_constant())
-    return true;
+  if(!is_temporal_operator(expr))
+  {
+    if(!has_temporal_operator(expr))
+      return true; // initial state only
+    else
+      return false;
+  }
+  else if(expr.id() == ID_sva_cycle_delay)
+    return !has_temporal_operator(to_sva_cycle_delay_expr(expr).op());
+  else if(expr.id() == ID_sva_nexttime)
+    return !has_temporal_operator(to_sva_nexttime_expr(expr).op());
+  else if(expr.id() == ID_sva_s_nexttime)
+    return !has_temporal_operator(to_sva_s_nexttime_expr(expr).op());
   else if(expr.id() == ID_AG)
     return true;
   else if(expr.id() == ID_G)
@@ -68,9 +80,20 @@ void property(
 {
   messaget message(message_handler);
 
-  if(property_expr.is_true())
+  // Initial state only property?
+  if(
+    !is_temporal_operator(property_expr) ||
+    property_expr.id() == ID_sva_cycle_delay ||
+    property_expr.id() == ID_sva_nexttime ||
+    property_expr.id() == ID_sva_s_nexttime)
   {
     prop_handles.resize(no_timeframes, true_exprt());
+    if(no_timeframes > 0)
+    {
+      exprt tmp = instantiate(property_expr, 0, no_timeframes, ns);
+      prop_handles.push_back(solver.handle(tmp));
+    }
+
     return;
   }