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
abradd has joined #yosys
<abradd> Using "prep; flatten; tribuf -formal" seems to resolve the error I was seeing
<abradd> I noticed that when traces are generated they don't display the tristate port as 'z even when the input conditions mean they should
<abradd> Is that expected or do I have some other issue?
<abradd> I saw this in my own code, but started using https://gist.github.com/jix/6ccf5b58f10ce77cf40d9f13ed15db86 as a reference for testing. In it I also see that the tristate port goes to '0 instead of 'z when "en" is low
<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]
kristianpaul has joined #yosys
FabM has quit [Ping timeout: 255 seconds]
bjorkintosh has quit [Quit: Leaving]
bjorkintosh has joined #yosys
abradd has joined #yosys
Lord_Nightmare has quit [Quit: ZNC - http://znc.in]
Lord_Nightmare has joined #yosys
nonchip has quit [Quit: https://quassel-irc.org - Chat comfortably. Anywhere.]
nonchip has joined #yosys