Incorrect refutations with not, until_with, s_until and |-> in EBMC 5.0/5.1

[spdskatr]

Code:

module top(input x, input y, input clk);

  logic a, b;
  always_ff @(posedge clk) begin
    a <= x;
    b <= y;
  end

  // Not s_eventually 0 should always be true
  assert property (not s_eventually 0);
  
  // Using until_with
  assert property (a until_with b |-> not ((not b) s_until (not a)));
  assert property (not ((not b) s_until (not a)) |-> a until_with b);

  // Until_with equivalence with until
  assert property ((a until_with b) |-> (a until (a and b)));
  assert property ((a until (a and b)) |-> (a until_with b));

  // Property implies itself should always be true
  assert property ((b or (always b)) |-> (b or (always b)));
  assert property ((b or (always b)) implies (b or (always b)));

  // Definitions of strong eventually
  assert property ((s_eventually a) |-> (1 s_until a));
  assert property ((1 s_until a) |-> (s_eventually a));

  // Definitions of strong until
  assert property ((a s_until b) |-> ((s_eventually b) and (a until b)));
  assert property ((a s_until b) implies ((s_eventually b) and (a until b)));
  assert property (((s_eventually b) and (a until b)) |-> (a s_until b));
  assert property (((s_eventually b) and (a until b)) implies (a s_until b));

endmodule

Run with ebmc code.sv --systemverilog --bound 5 --top top. I think all of these assertions should be true by LTL laws. However, most of these properties get refuted with counterexample traces that seem to make no sense.

EBMC 5.0 output:

[top.assert.1] always !(s_eventually 0): REFUTED
[top.assert.2] always ((top.a until_with top.b) |-> !(!top.b s_until !top.a)): REFUTED
[top.assert.3] always (!(!top.b s_until !top.a) |-> (top.a until_with top.b)): REFUTED
[top.assert.4] always ((top.a until_with top.b) |-> (top.a until top.a && top.b)): REFUTED
[top.assert.5] always ((top.a until top.a && top.b) |-> (top.a until_with top.b)): REFUTED
[top.assert.6] always (top.b || (always top.b) |-> top.b || (always top.b)): PROVED up to bound 5
[top.assert.7] always (top.b || (always top.b) |-> top.b || (always top.b)): PROVED up to bound 5
[top.assert.8] always ((s_eventually top.a) |-> (1 s_until top.a)): PROVED up to bound 5
[top.assert.9] always ((1 s_until top.a) |-> (s_eventually top.a)): REFUTED
[top.assert.10] always ((top.a s_until top.b) |-> (s_eventually top.b) && (top.a until top.b)): REFUTED
[top.assert.11] always (top.a s_until top.b |-> (s_eventually top.b) && (top.a until top.b)): REFUTED
[top.assert.12] always ((s_eventually top.b) && (top.a until top.b) |-> (top.a s_until top.b)): PROVED up to bound 5
[top.assert.13] always ((s_eventually top.b) && (top.a until top.b) |-> top.a s_until top.b): PROVED up to bound 5

EBMC 5.1 output:

[top.assert.1] always not s_eventually 0: REFUTED
[top.assert.2] always ((top.a until_with top.b) |-> not (not top.b s_until not top.a)): REFUTED
[top.assert.3] always (not (not top.b s_until not top.a) |-> (top.a until_with top.b)): REFUTED
[top.assert.4] always ((top.a until_with top.b) |-> (top.a until top.a and top.b)): REFUTED
[top.assert.5] always ((top.a until top.a and top.b) |-> (top.a until_with top.b)): REFUTED
[top.assert.6] always (top.b or (always top.b) |-> top.b or (always top.b)): REFUTED
[top.assert.7] always (top.b or (always top.b) |-> top.b or (always top.b)): PROVED up to bound 5
[top.assert.8] always ((s_eventually top.a) |-> (1 s_until top.a)): PROVED up to bound 5
[top.assert.9] always ((1 s_until top.a) |-> (s_eventually top.a)): REFUTED
[top.assert.10] always ((top.a s_until top.b) |-> (s_eventually top.b) and (top.a until top.b)): REFUTED
[top.assert.11] always (top.a s_until top.b |-> (s_eventually top.b) and (top.a until top.b)): REFUTED
[top.assert.12] always ((s_eventually top.b) and (top.a until top.b) |-> (top.a s_until top.b)): REFUTED
[top.assert.13] always ((s_eventually top.b) and (top.a until top.b) |-> top.a s_until top.b): PROVED up to bound 5

In EBMC 5.1, |-> and implies also seem to produce different results.

[kroening]

Somewhat unrelated question: The SVA grammar requires a sequence on the LHS of |->:

sequence_expr |-> property_expr

Do you have another tool at hand that parses this?

[spdskatr]

The SVA grammar requires a sequence on the LHS of |->:

Ah, you are right - I completely missed that. I suppose the assertions should all be using implies instead. I tried this:

module top(input x, input y, input clk);

  logic a, b;
  always_ff @(posedge clk) begin
    a <= x;
    b <= y;
  end

  // Not s_eventually 0 should always be true
  assert property (not s_eventually 0);

  // Using until_with
  assert property ((a until_with b) implies not ((not b) s_until (not a)));
  assert property (not ((not b) s_until (not a)) implies (a until_with b));

  // Until_with equivalence with until
  assert property ((a until_with b) implies (a until (a and b)));
  assert property ((a until (a and b)) implies (a until_with b));

  // Definitions of strong eventually
  assert property ((s_eventually a) implies (1 s_until a));
  assert property ((1 s_until a) implies (s_eventually a));

  // Definitions of strong until
  assert property ((a s_until b) implies ((s_eventually b) and (a until b)));
  assert property (((s_eventually b) and (a until b)) implies (a s_until b));

endmodule

The output is still the same:

[top.assert.1] always !(s_eventually 0): REFUTED
[top.assert.2] always (top.a until_with top.b |-> !(!top.b s_until !top.a)): REFUTED
[top.assert.3] always (!(!top.b s_until !top.a) |-> top.a until_with top.b): REFUTED
[top.assert.4] always (top.a until_with top.b |-> top.a until top.a && top.b): REFUTED
[top.assert.5] always (top.a until top.a && top.b |-> top.a until_with top.b): REFUTED
[top.assert.6] always (s_eventually top.a |-> 1 s_until top.a): PROVED up to bound 5
[top.assert.7] always (1 s_until top.a |-> s_eventually top.a): REFUTED
[top.assert.8] always (top.a s_until top.b |-> (s_eventually top.b) && (top.a until top.b)): REFUTED
[top.assert.9] always ((s_eventually top.b) && (top.a until top.b) |-> top.a s_until top.b): PROVED up to bound 5

Do you have another tool at hand that parses this?

I don't have another tool that I can cross-check with.