EBMC/ic3 fails to verify property of ring_buffer example

[mgudemann]

both --bdd and --k-induction verify the property. Maybe --ic3 does not handle the assumes?

  wire full=count==15;
  wire empty=count==0;

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

  assert property (((writeptr-readptr)&'b1111)==count);

[eigold]

We had a discussion about how to specify constraints a while ago. Rajdeep said that the verilog 'assume' was not implemented yet. (However, I did not hear that from Daniel.) So constraints for IC3 are currently specified as a list of literals in a separate file. Maybe something has changed since then or Rajdeep was wrong. Could you send me the entire verilog file? Eugene

…

On Sun, Jul 2, 2017 at 9:35 AM, Matthias Güdemann ***@***.***> wrote: both --bdd and --k-induction verify the property. Maybe --ic3 does not handle the assumes? wire full=count==15; wire empty=count==0; assume property (empty |-> !read); assume property (full |-> !write); assert property (((writeptr-readptr)&'b1111)==count); — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#20>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AS5pCtV79kJNoZ4tU6BzLDOeNJS7Jv3Rks5sJ5y8gaJpZM4OLldY> .

[mgudemann]

Hi Eugene, please find it attached. Best, Matthias

[mgudemann]

example4.sv.zip