Problem with engine heuristic

[felixridoux]

The new basic engine heuristic seems to introduce a bug when it is applied to designs containing assumptions not supported by the k-induction engine (temporal property in my case). The assumption seems to be transformed into an assertion.

As an example, if you take regression/ebmc/k-induction/ring_buffer.sv, and you slightly modify the first assumption in order to add a temporal operator as follows, the engine will output REFUTED instead of ASSUMED or FAILURE: property unsupported by k-induction for the first assumption:

module ring_buffer(input clk, input read, input write);

  reg [4:0] count=0;
  reg [3:0] readptr=0, writeptr=0;

  always @(posedge clk) begin
    if(read) begin
      readptr++;
      count--;
    end

    if(write) begin
      writeptr++;
      count++;
    end

  end

  wire full=count==16;
  wire empty=count==0;

  assume property (empty |=> !read);
  assume property (full |-> !write);

  p0: assert property (((writeptr-readptr)&'b1111)==count[3:0]);
  p1: assert property (count <= 16);
  p2: assert property (count != 17);

endmodule

[kroening]

May I ask you to try #923 ?

[felixridoux]

Yep! It's working on my side. Thanks a lot. To be sure, I just want to point out that before this modification, in case of an unsupported assumption, the k-induction engine would attempt to prove the property without the assumption. However, now it seems the engine always returns "UNKNOWN" in such cases. This convention can make sense. Is it the intended behavior?

[kroening]

I am a bit torn on this; but yes, k-induction should still work even if an unsupported assumption is present. Will fix.

[kroening]

Just pushed, please try!

[felixridoux]

Thanks!

I see two remaining potential problems: (that can be reproduced on regression/ebmc/k-induction/k-induction6.sv)

• In the presence of an assume unsupported by the k-induction engine, if the property is proved by k-induction through the heuristic engine, the assume is marked as ASSUMED. (Whereas it could be marked as FAILURE, as if you were using the plain k-induction engine)

• When using the heuristic engine, if 1-induction returns INCONCLUSIVE, heuristic engine also returns INCONCLUSIVE. (Whereas it could attempt a bounded proof using BMC).

[kroening]

Agreed on both items, revision just pushed.

[felixridoux]

I tried your changes on my side. It seems that the first point still holds when a design contains several assumptions, some supported by k-induction, some not. As an example, if you run ebmc k-induction7.sv and ebmc --k-induction k-induction7.sv you get different outputs.

[kroening]

Indeed, agreed, you want to see which assumption was actually used. Change pushed.

[felixridoux]

I tried, but I think there is still an issue. It seems that now, if an assumption is not supported by k-induction, false assertions can be proven. This happens with both the k-induction engine and the heuristic engine. Here is a minimal example:

module main(input clk, input x);

  a0: assume property (not s_eventually !x);

  p0: assert property (0==1);

endmodule

On this example, both engines prove p0.

[kroening]

Just pushed the next attempt -- this will need a refactoring to prevent interaction between the engines.

[felixridoux]

Thanks ! Working better on my side. I am just a bit unsure of what should be output in the presence of a temporal assumption and several assertions. When some assertions are proved without the assumption by k-induction and others are proved by BMC using the assumption.

[kroening]

Agreed; I think this will hit the limit of what can be communicated in a simple list of properties.