<jix>
that's expected, the verification infrastructure doesn't actually support 'z so "tribuf -formal" converts it into equivalent logic + assertions to detect drive conflicts
citypw has joined #yosys
citypw has quit [Remote host closed the connection]
citypw has joined #yosys
ec has joined #yosys
abradd has quit [Quit: Client closed]
abradd has joined #yosys
<abradd>
Ok that makes sense. If I set any signal to 'z or it would otherwise have evaluated to 'z, is it always converted to '0 in the equivalent logic?
<abradd>
I've been testing the code at https://gist.github.com/jix/6ccf5b58f10ce77cf40d9f13ed15db86 and it behaves as expected given your description above, but I have another simple module that seems to be ignoring my "en" signal and I cannot figure out why
<abradd>
It basically boils down to
<abradd>
assign tri_inout = en ? in : 1'bz;
<abradd>
assign out = tri_inout;
<abradd>
with a formal verification section that runs a counter, counts to 3 and covers ( out == 1 && count == 3)
<abradd>
I can also provide the testcase if that is preferred
<abradd>
but it seems the "en" is removed in the design.il file:
<abradd>
connect \out \tri_inout
<abradd>
connect \tri_inout \in
<abradd>
which is what I see if the traces, "out" goes high as soon as "in" does irrespective of "en"
abradd has quit [Ping timeout: 250 seconds]
peeps has joined #yosys
peeps[zen] has quit [Ping timeout: 268 seconds]
FabM has joined #yosys
FabM has joined #yosys
ZipCPU_ has joined #yosys
ZipCPU has quit [Ping timeout: 255 seconds]
ZipCPU_ is now known as ZipCPU
cr1901 has quit [Read error: Connection reset by peer]
cr1901_ has joined #yosys
ec has quit [Remote host closed the connection]
ec has joined #yosys
notgull has quit [Ping timeout: 255 seconds]
notgull has joined #yosys
FabM has quit [Ping timeout: 256 seconds]
FabM has joined #yosys
FabM has joined #yosys
bjorkintosh has quit [Ping timeout: 268 seconds]
tlwoerner has quit [Ping timeout: 256 seconds]
citypw has quit [Ping timeout: 240 seconds]
tlwoerner has joined #yosys
strobo5 has joined #yosys
bjorkintosh has joined #yosys
strobo5 has quit [Quit: leaving]
cr1901_ is now known as cr1901
kristianpaul has quit [Read error: Connection reset by peer]