Merge pull request #1095 from diffblue/s_always1

implement NNF for SVA `s_always`

Author: tautschnig

regression/verilog/SVA/s_always1.desc

@@ -0,0 +1,10 @@
+CORE
+s_always1.sv
+--bound 20
+^\[main\.p0\] s_always \[0:9\] main\.x < 10: PROVED up to bound 20$
+^\[main\.p1\] not \(s_always \[0:9\] main\.x < 10\): REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/SVA/s_always1.sv

@@ -0,0 +1,14 @@
+module main(input clk);
+
+  reg [31:0] x = 0;
+
+  always_ff @(posedge clk)
+    x<=x+1;
+
+  // should pass
+  initial p0: assert property (s_always [0:9] x<10);
+
+  // should fail
+  initial p1: assert property (not s_always [0:9] x<10);
+
+endmodule

src/temporal-logic/nnf.cpp

@@ -81,6 +81,13 @@ std::optional<exprt> negate_property_node(const exprt &expr)
     return sva_ranged_s_eventually_exprt{
       always.lower(), always.upper(), not_exprt{always.op()}};
   }
+  else if(expr.id() == ID_sva_s_always)
+  {
+    // not s_always [x:y] p --> eventually [x:y] not p
+    auto &s_always = to_sva_s_always_expr(expr);
+    return sva_eventually_exprt{
+      s_always.lower(), s_always.upper(), not_exprt{s_always.op()}};
+  }
   else if(expr.id() == ID_sva_s_eventually)
   {
     // not s_eventually p --> always not p