whitequark changed the topic of #yosys to: Yosys Open SYnthesis Suite: https://github.com/YosysHQ/yosys/ | Channel logs: https://libera.irclog.whitequark.org/yosys/ | Bridged to #yosys:matrix.org
tpb has quit [Remote host closed the connection]
tpb has joined #yosys
skipwich has quit [Quit: DISCONNECT]
skipwich has joined #yosys
so-offish has quit [Ping timeout: 260 seconds]
peeps[zen] has quit [Ping timeout: 260 seconds]
FabM has joined #yosys
lexano has joined #yosys
Stary has quit [Quit: ZNC - http://znc.in]
Stary has joined #yosys
FabM has quit [Ping timeout: 256 seconds]
FabM has joined #yosys
FabM has joined #yosys
PeterMonsson has joined #yosys
<PeterMonsson> Hi all, I am trying to play with liveness proofs in sby. When a liveness proof fails, I get the following error:
<PeterMonsson> SBY 14:06:54 [fib_live] engine_0: finished (returncode=0)
<PeterMonsson> SBY 14:06:54 [fib_live] engine_0: Status returned by engine: FAIL
<PeterMonsson> SBY 14:06:54 [fib_live] engine_0: Engine did not produce a counter example.
<PeterMonsson> SBY 14:06:54 [fib_live] engine_0: starting process "cd fib_live; yosys-witness aiw2yw engine_0/trace.aiw model/design_aiger.ywa engine_0/trace.yw"
<PeterMonsson> SBY 14:06:54 [fib_live] engine_0: Converting AIGER witness trace 'engine_0/trace.aiw' to Yosys witness trace 'engine_0/trace.yw'...
<PeterMonsson> SBY 14:06:54 [fib_live] engine_0: Using Yosys witness AIGER map file 'model/design_aiger.ywa'
<PeterMonsson> SBY 14:06:54 [fib_live] engine_0: Error: engine_0/trace.aiw: unexpected data in AIGER witness file
<PeterMonsson> SBY 14:06:54 [fib_live] engine_0: finished (returncode=1)
<PeterMonsson> SBY 14:06:54 [fib_live] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
<PeterMonsson> SBY 14:06:54 [fib_live] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
<PeterMonsson> SBY 14:06:54 [fib_live] summary: engine_0 (aiger suprove) returned FAIL
<PeterMonsson> SBY 14:06:54 [fib_live] summary: engine_0 did not produce any traces
<PeterMonsson> SBY 14:06:54 [fib_live] DONE (FAIL, rc=2)
<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)
PeterMonsson has quit [Ping timeout: 250 seconds]
peeps[zen] has joined #yosys
so-offish has joined #yosys
so-offishul has joined #yosys
so-offish has quit [Ping timeout: 240 seconds]
so-offishul has quit [Quit: Leaving]
chaoticryptidz has quit [Quit: https://quassel-irc.org - Chat comfortably. Anywhere.]
chaoticryptidz has joined #yosys
chaoticryptidz has quit [Client Quit]
chaoticryptidz has joined #yosys
corecode has joined #yosys
FabM has quit [Ping timeout: 260 seconds]
ec_ has joined #yosys
ec_ is now known as ec
PeterMonsson has joined #yosys
PeterMonsson has quit [Ping timeout: 250 seconds]
mundanesemantics has joined #yosys
mundanesemantics has quit [Ping timeout: 256 seconds]
mundanesemantics has joined #yosys
Guest64 has joined #yosys
<Guest64> Hi, I wanted to ask if anyone could advise me how to set time constraints for Tang Nano 20k.
Guest64 has quit [Quit: Client closed]
nonchip has quit [Quit: https://quassel-irc.org - Chat comfortably. Anywhere.]
nonchip has joined #yosys