*** tpb <[email protected]> has joined #yosys | 00:00 | |
*** abradd <[email protected]> has joined #yosys | 00:30 | |
abradd | Using "prep; flatten; tribuf -formal" seems to resolve the error I was seeing | 01:20 |
---|---|---|
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 | 01:21 |
abradd | Is that expected or do I have some other issue? | 01:22 |
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 | 01:23 |
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 | 01:26 |
*** citypw <citypw!~citypw@gateway/tor-sasl/citypw> has joined #yosys | 01:32 | |
*** citypw <citypw!~citypw@gateway/tor-sasl/citypw> has quit IRC (Remote host closed the connection) | 01:44 | |
*** citypw <citypw!~citypw@gateway/tor-sasl/citypw> has joined #yosys | 01:44 | |
*** ec <ec!~ec@gateway/tor-sasl/ec> has joined #yosys | 02:29 | |
*** abradd <[email protected]> has quit IRC (Quit: Client closed) | 02:31 | |
*** abradd <[email protected]> has joined #yosys | 02:42 | |
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? | 03:16 |
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 | 03:17 |
abradd | It basically boils down to | 03:19 |
abradd | assign tri_inout = en ? in : 1'bz; | 03:19 |
abradd | assign out = tri_inout; | 03:19 |
abradd | with a formal verification section that runs a counter, counts to 3 and covers ( out == 1 && count == 3) | 03:19 |
abradd | I can also provide the testcase if that is preferred | 03:19 |
abradd | but it seems the "en" is removed in the design.il file: | 03:20 |
abradd | connect \out \tri_inout | 03:20 |
abradd | connect \tri_inout \in | 03:20 |
abradd | which is what I see if the traces, "out" goes high as soon as "in" does irrespective of "en" | 03:20 |
*** abradd <[email protected]> has quit IRC (Ping timeout: 250 seconds) | 05:46 | |
*** peeps <peeps!~peepsalot@openscad/peepsalot> has joined #yosys | 07:19 | |
*** peeps[zen] <peeps[zen]!~peepsalot@openscad/peepsalot> has quit IRC (Ping timeout: 268 seconds) | 07:19 | |
*** FabM <FabM!~FabM@2a03:d604:103:600:2e60:8c7c:e8fb:7990> has joined #yosys | 07:32 | |
*** ZipCPU_ <[email protected]> has joined #yosys | 07:56 | |
*** ZipCPU <[email protected]> has quit IRC (Ping timeout: 255 seconds) | 07:57 | |
*** ZipCPU_ is now known as ZipCPU | 07:57 | |
*** cr1901 <cr1901!~cr1901@2601:8d:8600:226:1915:bf93:3d7f:e1a9> has quit IRC (Read error: Connection reset by peer) | 08:27 | |
*** cr1901_ <cr1901_!~cr1901@2601:8d:8600:226:bda5:65fe:a24e:b190> has joined #yosys | 08:27 | |
*** ec <ec!~ec@gateway/tor-sasl/ec> has quit IRC (Remote host closed the connection) | 10:30 | |
*** ec <ec!~ec@gateway/tor-sasl/ec> has joined #yosys | 10:31 | |
*** notgull <notgull!~notgull@ec2-50-112-148-23.us-west-2.compute.amazonaws.com> has quit IRC (Ping timeout: 255 seconds) | 10:38 | |
*** notgull <notgull!~notgull@ec2-50-112-148-23.us-west-2.compute.amazonaws.com> has joined #yosys | 10:41 | |
*** FabM <FabM!~FabM@armadeus/team/FabM> has quit IRC (Ping timeout: 256 seconds) | 12:57 | |
*** FabM <FabM!~FabM@2a03:d604:103:600:2e60:8c7c:e8fb:7990> has joined #yosys | 13:09 | |
*** bjorkintosh <bjorkintosh!~bjork@user/bjorkintosh> has quit IRC (Ping timeout: 268 seconds) | 13:23 | |
*** tlwoerner <[email protected]> has quit IRC (Ping timeout: 256 seconds) | 13:34 | |
*** citypw <citypw!~citypw@gateway/tor-sasl/citypw> has quit IRC (Ping timeout: 240 seconds) | 13:35 | |
*** tlwoerner <[email protected]> has joined #yosys | 13:36 | |
*** strobo5 <[email protected]> has joined #yosys | 13:48 | |
*** bjorkintosh <bjorkintosh!~bjork@user/bjorkintosh> has joined #yosys | 13:54 | |
*** strobo5 <[email protected]> has quit IRC (Quit: leaving) | 14:03 | |
*** cr1901_ is now known as cr1901 | 14:42 | |
*** kristianpaul <kristianpaul!~paul@user/kristianpaul> has quit IRC (Read error: Connection reset by peer) | 16:42 | |
*** kristianpaul <kristianpaul!~paul@user/kristianpaul> has joined #yosys | 16:44 | |
*** FabM <FabM!~FabM@armadeus/team/FabM> has quit IRC (Ping timeout: 255 seconds) | 18:32 | |
*** bjorkintosh <bjorkintosh!~bjork@user/bjorkintosh> has quit IRC (Quit: Leaving) | 19:18 | |
*** bjorkintosh <bjorkintosh!~bjork@user/bjorkintosh> has joined #yosys | 20:11 | |
*** abradd <[email protected]> has joined #yosys | 22:26 | |
*** Lord_Nightmare <Lord_Nightmare!~Lord_Nigh@user/lord-nightmare/x-3657113> has quit IRC (Quit: ZNC - http://znc.in) | 22:31 | |
*** Lord_Nightmare <Lord_Nightmare!~Lord_Nigh@user/lord-nightmare/x-3657113> has joined #yosys | 22:34 | |
*** nonchip <[email protected]> has quit IRC (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.) | 23:21 | |
*** nonchip <[email protected]> has joined #yosys | 23:21 |
Generated by irclog2html.py 2.17.2 by Marius Gedminas - find it at https://mg.pov.lt/irclog2html/!