<PeterMonsson>
I am expecting that I should get a VCD file or similar that can help me debug the liveness failure. Is this a correct expectation?
<jix_>
PeterMonsson: AFAICT suprove simply isn't providing an actual counter example trace which SBY could turn into a vcd trace
<PeterMonsson>
jix_ Thank you. I don't see a different solver that does this. Is there a solver that you know of that provides traces on liveness failure?
<jix_>
Nope, and I would try to avoid using liveness overall
<jix_>
(usually by coming up with an actual upper bound that can be used instead of an eventually)
<PeterMonsson>
Thank you. Unfortunately, liveness is what I want in this case.Maybe I can do something with a bounded check to debug.
<jix_>
PeterMonsson: can you tell me what your use case is that requires livenss?
<PeterMonsson>
Proof that "the good thing happens", for example in the fib demo example from sby where liveness guarantees that the algorithm eventually completes
<jix_>
yeah but you still get that if you prove the stronger property "the good thing happens within N cycles" for a specific N
<jix_>
that's what I was suggesting, not using a BMC instead, I might not have been that clear
<PeterMonsson>
That is correct
<jix_>
and "the good thing happens within N cycles" is a safety property, which are much better supported
<jix_>
and that's still something you can't use for your usecase?
<PeterMonsson>
I can probably make it work. Thank you
<jix_>
(I'm mostly asking because if there is an actual use case for liveness in hardware verification where coming up with such a bound isn't pratical, and there might be, it would be great to know of it)