You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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>
.
both
--bdd
and--k-induction
verify the property. Maybe--ic3
does not handle theassume
s?The text was updated successfully, but these errors were encountered: