Verilog: normalize ##[i:$]

This rewrites ##[i:$] to LTL, enabling the back-end to generate
counterexamples of the correct length.

Author: kroening

regression/verilog/SVA/sequence2.desc

@@ -0,0 +1,17 @@
+CORE
+sequence2.sv
+--bound 10 --numbered-trace
+^\[main\.property\.1] ##\[0:\$\] main\.x == 10: REFUTED$
+^Counterexample with 7 states:$
+^main\.x@0 = 0$
+^main\.x@1 = 1$
+^main\.x@2 = 2$
+^main\.x@3 = 3$
+^main\.x@4 = 4$
+^main\.x@5 = 5$
+^main\.x@6 = 5$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/SVA/sequence2.sv

@@ -0,0 +1,15 @@
+module main;
+
+  reg [31:0] x;
+  wire clk;
+
+  initial x=0;
+
+  always @(posedge clk)
+    if(x != 5)
+      x<=x+1;
+
+  // fails once we see the lasso 0, 1, 2, 3, 4, 5, 5
+  initial p0: assert property (##[0:$] x==10);
+
+endmodule

src/temporal-logic/normalize_property.cpp

@@ -8,6 +8,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "normalize_property.h"
 
+#include <util/arith_tools.h>
 #include <util/std_expr.h>
 
 #include <verilog/sva_expr.h>
@@ -74,6 +75,27 @@ exprt normalize_pre_sva_non_overlapped_implication(
   return or_exprt{not_exprt{expr.lhs()}, X_exprt{expr.rhs()}};
 }
 
+exprt normalize_pre_sva_cycle_delay(sva_cycle_delay_exprt expr)
+{
+  if(expr.is_unbounded())
+  {
+    if(
+      expr.from().is_constant() &&
+      numeric_cast_v<mp_integer>(to_constant_expr(expr.from())) == 0)
+    {
+      // ##[0:$] φ --> F φ
+      return F_exprt{expr.op()};
+    }
+    else
+    {
+      // ##[i:$] φ --> ##i F φ
+      return sva_cycle_delay_exprt{expr.from(), F_exprt{expr.op()}};
+    }
+  }
+  else
+    return std::move(expr);
+}
+
 exprt normalize_property(exprt expr)
 {
   // pre-traversal
@@ -93,6 +115,8 @@ exprt normalize_property(exprt expr)
     expr = X_exprt{to_sva_nexttime_expr(expr).op()};
   else if(expr.id() == ID_sva_s_nexttime)
     expr = X_exprt{to_sva_s_nexttime_expr(expr).op()};
+  else if(expr.id() == ID_sva_cycle_delay)
+    expr = normalize_pre_sva_cycle_delay(to_sva_cycle_delay_expr(expr));
 
   // normalize the operands
   for(auto &op : expr.operands())

src/verilog/sva_expr.h

@@ -443,7 +443,7 @@ to_sva_non_overlapped_implication_expr(exprt &expr)
 class sva_cycle_delay_exprt : public ternary_exprt
 {
 public:
-  explicit sva_cycle_delay_exprt(exprt from, exprt to, exprt op)
+  sva_cycle_delay_exprt(exprt from, exprt to, exprt op)
     : ternary_exprt(
         ID_sva_cycle_delay,
         std::move(from),
@@ -453,6 +453,16 @@ class sva_cycle_delay_exprt : public ternary_exprt
   {
   }
 
+  sva_cycle_delay_exprt(exprt cycles, exprt op)
+    : ternary_exprt(
+        ID_sva_cycle_delay,
+        std::move(cycles),
+        nil_exprt{},
+        std::move(op),
+        bool_typet())
+  {
+  }
+
   const exprt &from() const
   {
     return op0();
@@ -475,6 +485,11 @@ class sva_cycle_delay_exprt : public ternary_exprt
     return op1();
   }
 
+  bool is_unbounded() const
+  {
+    return to().id() == ID_infinity;
+  }
+
   const exprt &op() const
   {
     return op2();