citypw has quit [Remote host closed the connection]
<josuah>
I am having this surprising behavior with symbiyosys (sby): I am running it with mode prove and smtbmc engine
<josuah>
and have a block with if (condition) assert(property_under_test);
<josuah>
and sby shows me a counterexample where condition is false
<josuah>
is it allowed to sbi to ignore the `if (condition)` guarding the `assert()` after it?
MoeIcenowy has quit [Read error: Connection reset by peer]
MoeIcenowy has joined #yosys
Guest9654 has joined #yosys
Klotz has joined #yosys
<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)
Klotz has quit [Remote host closed the connection]
Klotz has joined #yosys
<josuah>
jix: thank you! I was myself AFK
<josuah>
I will try to get a shorter reproducer
<josuah>
haha! found it!
<josuah>
jix: thank you for your very efficient debugging: making me try a reproducer
<josuah>
the problem: I neglected the reset signal I made for myself
<josuah>
which in formal testing, may not be high right at the beginning and low forever after, unless I properly assume() it away
* josuah
takes a deep breath and goes back to be prooven wrong by sby once more
Klotz has quit [Remote host closed the connection]
Klotz has joined #yosys
<jix>
if only I could solve every case of "sby doesn't do what it should" like this :D