| *** tpb <[email protected]> has joined #yosys | 00:00 | |
| *** skipwich <skipwich!~skipwich@user/skipwich> has quit IRC (Quit: DISCONNECT) | 01:50 | |
| *** skipwich <skipwich!~skipwich@user/skipwich> has joined #yosys | 01:52 | |
| *** so-offish <so-offish!~so-offish@2610:148:610:2b11::17> has quit IRC (Ping timeout: 260 seconds) | 05:33 | |
| *** peeps[zen] <peeps[zen]!~peepsalot@openscad/peepsalot> has quit IRC (Ping timeout: 260 seconds) | 07:06 | |
| *** FabM <FabM!~FabM@armadeus/team/FabM> has joined #yosys | 07:26 | |
| *** lexano <[email protected]> has joined #yosys | 11:53 | |
| *** Stary <Stary!Stary@hacksoc/infrastructure> has quit IRC (Quit: ZNC - http://znc.in) | 12:03 | |
| *** Stary <Stary!Stary@hacksoc/infrastructure> has joined #yosys | 12:09 | |
| *** FabM <FabM!~FabM@armadeus/team/FabM> has quit IRC (Ping timeout: 256 seconds) | 13:49 | |
| *** FabM <FabM!~FabM@2a03:d604:10a:9a00:f4be:37d9:b762:70ba> has joined #yosys | 14:01 | |
| *** PeterMonsson <[email protected]> has joined #yosys | 14:16 | |
| PeterMonsson | Hi all, I am trying to play with liveness proofs in sby. When a liveness proof fails, I get the following error: | 14:18 |
|---|---|---|
| PeterMonsson | SBY 14:06:54 [fib_live] engine_0: finished (returncode=0) | 14:18 |
| PeterMonsson | SBY 14:06:54 [fib_live] engine_0: Status returned by engine: FAIL | 14:18 |
| PeterMonsson | SBY 14:06:54 [fib_live] engine_0: Engine did not produce a counter example. | 14:18 |
| 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" | 14:18 |
| 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'... | 14:18 |
| PeterMonsson | SBY 14:06:54 [fib_live] engine_0: Using Yosys witness AIGER map file 'model/design_aiger.ywa' | 14:18 |
| PeterMonsson | SBY 14:06:54 [fib_live] engine_0: Error: engine_0/trace.aiw: unexpected data in AIGER witness file | 14:18 |
| PeterMonsson | SBY 14:06:54 [fib_live] engine_0: finished (returncode=1) | 14:18 |
| PeterMonsson | SBY 14:06:54 [fib_live] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0) | 14:18 |
| PeterMonsson | SBY 14:06:54 [fib_live] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0) | 14:18 |
| PeterMonsson | SBY 14:06:54 [fib_live] summary: engine_0 (aiger suprove) returned FAIL | 14:18 |
| PeterMonsson | SBY 14:06:54 [fib_live] summary: engine_0 did not produce any traces | 14:18 |
| PeterMonsson | SBY 14:06:54 [fib_live] DONE (FAIL, rc=2) | 14:18 |
| 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? | 14:18 |
| jix_ | PeterMonsson: AFAICT suprove simply isn't providing an actual counter example trace which SBY could turn into a vcd trace | 14:29 |
| 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? | 14:35 |
| jix_ | Nope, and I would try to avoid using liveness overall | 14:37 |
| jix_ | (usually by coming up with an actual upper bound that can be used instead of an eventually) | 14:38 |
| PeterMonsson | Thank you. Unfortunately, liveness is what I want in this case.Maybe I can do something with a bounded check to debug. | 14:41 |
| jix_ | PeterMonsson: can you tell me what your use case is that requires livenss? | 14:42 |
| PeterMonsson | Proof that "the good thing happens", for example in the fib demo example from sby where liveness guarantees that the algorithm eventually completes | 14:44 |
| jix_ | yeah but you still get that if you prove the stronger property "the good thing happens within N cycles" for a specific N | 14:45 |
| jix_ | that's what I was suggesting, not using a BMC instead, I might not have been that clear | 14:45 |
| PeterMonsson | That is correct | 14:46 |
| jix_ | and "the good thing happens within N cycles" is a safety property, which are much better supported | 14:47 |
| jix_ | and that's still something you can't use for your usecase? | 14:50 |
| PeterMonsson | I can probably make it work. Thank you | 14:53 |
| 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) | 14:54 |
| *** PeterMonsson <[email protected]> has quit IRC (Ping timeout: 250 seconds) | 14:57 | |
| *** peeps[zen] <peeps[zen]!~peepsalot@openscad/peepsalot> has joined #yosys | 15:39 | |
| *** so-offish <[email protected]> has joined #yosys | 16:13 | |
| *** so-offishul <so-offishul!~so-offish@2610:148:610:2b11::3> has joined #yosys | 16:14 | |
| *** so-offish <[email protected]> has quit IRC (Ping timeout: 240 seconds) | 16:17 | |
| *** so-offishul <so-offishul!~so-offish@2610:148:610:2b11::3> has quit IRC (Quit: Leaving) | 16:25 | |
| *** chaoticryptidz <chaoticryptidz!~quassel@static.62.145.21.65.clients.your-server.de> has quit IRC (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.) | 16:37 | |
| *** chaoticryptidz <chaoticryptidz!~quassel@static.62.145.21.65.clients.your-server.de> has joined #yosys | 16:38 | |
| *** chaoticryptidz <chaoticryptidz!~quassel@static.62.145.21.65.clients.your-server.de> has quit IRC (Client Quit) | 16:38 | |
| *** chaoticryptidz <chaoticryptidz!~quassel@static.62.145.21.65.clients.your-server.de> has joined #yosys | 16:39 | |
| *** corecode <[email protected]> has joined #yosys | 17:13 | |
| *** FabM <FabM!~FabM@armadeus/team/FabM> has quit IRC (Ping timeout: 260 seconds) | 17:14 | |
| *** ec_ <ec_!~ec@gateway/tor-sasl/ec> has joined #yosys | 18:12 | |
| *** ec_ is now known as ec | 18:12 | |
| *** PeterMonsson <[email protected]> has joined #yosys | 20:25 | |
| *** PeterMonsson <[email protected]> has quit IRC (Ping timeout: 250 seconds) | 20:36 | |
| *** mundanesemantics <[email protected]> has joined #yosys | 21:19 | |
| *** mundanesemantics <[email protected]> has quit IRC (Ping timeout: 256 seconds) | 21:27 | |
| *** mundanesemantics <[email protected]> has joined #yosys | 21:35 | |
| *** Guest64 <[email protected]> has joined #yosys | 21:44 | |
| Guest64 | Hi, I wanted to ask if anyone could advise me how to set time constraints for Tang Nano 20k. | 21:45 |
| *** Guest64 <[email protected]> has quit IRC (Quit: Client closed) | 22:08 | |
| *** nonchip <[email protected]> has quit IRC (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.) | 23:27 | |
| *** nonchip <[email protected]> has joined #yosys | 23:27 | |
Generated by irclog2html.py 2.17.2 by Marius Gedminas - find it at https://mg.pov.lt/irclog2html/!