| *** tpb <[email protected]> has joined #yosys | 00:00 | |
| *** revcane <[email protected]> has quit IRC (Ping timeout: 272 seconds) | 02:22 | |
| *** revcane <[email protected]> has joined #yosys | 02:22 | |
| *** citypw <citypw!~citypw@gateway/tor-sasl/citypw> has joined #yosys | 02:58 | |
| *** chuangzhu <chuangzhu!~chuangmel@2001:470:69fc:105::1:d139> has quit IRC (Quit: Reconnecting) | 04:06 | |
| *** chuangzhu <chuangzhu!~chuangmel@2001:470:69fc:105::1:d139> has joined #yosys | 04:06 | |
| *** GenTooMan <GenTooMan!~cyberman@2601:547:437f:e5c6:21f:5bff:fefe:a883> has quit IRC (Ping timeout: 255 seconds) | 04:16 | |
| *** GenTooMan <GenTooMan!~cyberman@2601:547:437f:e5c6:21f:5bff:fefe:a883> has joined #yosys | 04:28 | |
| *** FabM <[email protected]> has joined #yosys | 06:59 | |
| *** kristianpaul <kristianpaul!~paul@user/kristianpaul> has quit IRC (Ping timeout: 240 seconds) | 07:03 | |
| *** kristianpaul <kristianpaul!~paul@user/kristianpaul> has joined #yosys | 07:05 | |
| *** nelgau <[email protected]> has joined #yosys | 09:00 | |
| *** nelgau_ <[email protected]> has quit IRC (Ping timeout: 272 seconds) | 09:02 | |
| *** citypw <citypw!~citypw@gateway/tor-sasl/citypw> has quit IRC (Ping timeout: 268 seconds) | 09:28 | |
| *** TFKyle <[email protected]> has joined #yosys | 09:33 | |
| *** citypw <citypw!~citypw@gateway/tor-sasl/citypw> has joined #yosys | 09:41 | |
| *** TFKyle <[email protected]> has quit IRC (Quit: :q!) | 09:48 | |
| *** GenTooMan <GenTooMan!~cyberman@2601:547:437f:e5c6:21f:5bff:fefe:a883> has quit IRC (Ping timeout: 268 seconds) | 10:29 | |
| *** GenTooMan <GenTooMan!~cyberman@2601:547:437f:e5c6:21f:5bff:fefe:a883> has joined #yosys | 10:42 | |
| *** DamienM <[email protected]> has joined #yosys | 12:01 | |
| *** DamienM <[email protected]> has quit IRC (Quit: Client closed) | 12:15 | |
| *** GenTooMan <GenTooMan!~cyberman@2601:547:437f:e5c6:21f:5bff:fefe:a883> has quit IRC (Ping timeout: 240 seconds) | 13:21 | |
| *** GenTooMan <GenTooMan!~cyberman@2601:547:437f:e5c6:21f:5bff:fefe:a883> has joined #yosys | 13:35 | |
| *** FabM <FabM!~FabM@armadeus/team/FabM> has quit IRC (Quit: Leaving) | 15:21 | |
| *** citypw <citypw!~citypw@gateway/tor-sasl/citypw> has quit IRC (Remote host closed the connection) | 16:23 | |
| josuah | I am having this surprising behavior with symbiyosys (sby): I am running it with mode prove and smtbmc engine | 18:27 |
|---|---|---|
| josuah | and have a block with if (condition) assert(property_under_test); | 18:27 |
| josuah | and sby shows me a counterexample where condition is false | 18:28 |
| josuah | is it allowed to sbi to ignore the `if (condition)` guarding the `assert()` after it? | 18:28 |
| *** MoeIcenowy <[email protected]> has quit IRC (Read error: Connection reset by peer) | 18:49 | |
| *** MoeIcenowy <[email protected]> has joined #yosys | 18:50 | |
| *** Guest9654 <[email protected]> has joined #yosys | 19:04 | |
| *** Klotz <Klotz!~Klotzoman@gateway/tor-sasl/klotz> has joined #yosys | 19:20 | |
| jix | josuah: using an if like that to guard an assertion should work, can you share your code and/or the counterexample you get? (I'm afk now for a bit, but I can have a look when I'm back) | 19:58 |
| *** Klotz <Klotz!~Klotzoman@gateway/tor-sasl/klotz> has quit IRC (Remote host closed the connection) | 20:43 | |
| *** Klotz <Klotz!~Klotzoman@gateway/tor-sasl/klotz> has joined #yosys | 20:44 | |
| josuah | jix: thank you! I was myself AFK | 20:50 |
| josuah | I will try to get a shorter reproducer | 20:50 |
| josuah | haha! found it! | 21:14 |
| josuah | jix: thank you for your very efficient debugging: making me try a reproducer | 21:14 |
| josuah | the problem: I neglected the reset signal I made for myself | 21:15 |
| josuah | which in formal testing, may not be high right at the beginning and low forever after, unless I properly assume() it away | 21:16 |
| * josuah takes a deep breath and goes back to be prooven wrong by sby once more | 21:18 | |
| *** Klotz <Klotz!~Klotzoman@gateway/tor-sasl/klotz> has quit IRC (Remote host closed the connection) | 21:20 | |
| *** Klotz <Klotz!~Klotzoman@gateway/tor-sasl/klotz> has joined #yosys | 21:20 | |
| jix | if only I could solve every case of "sby doesn't do what it should" like this :D | 21:20 |
| josuah | jix: ask to jix, that worked well for me | 21:27 |
| *** nonchip <[email protected]> has quit IRC (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.) | 22:03 | |
| *** nonchip <[email protected]> has joined #yosys | 22:03 | |
| *** Klotz <Klotz!~Klotzoman@gateway/tor-sasl/klotz> has quit IRC (Remote host closed the connection) | 22:38 | |
| *** Klotz <Klotz!~Klotzoman@gateway/tor-sasl/klotz> has joined #yosys | 22:39 | |
| *** Klotz <Klotz!~Klotzoman@gateway/tor-sasl/klotz> has quit IRC (Quit: Klotz) | 22:44 | |
Generated by irclog2html.py 2.17.2 by Marius Gedminas - find it at https://mg.pov.lt/irclog2html/!