Wednesday, 2018-03-07

*** tpb has joined #yosys00:00
promach_ZipCPU: you are done with asynchronous FIFO and UART ?00:00
promach_I mean formally verifiying00:00
ZipCPUNot quite on either account.  I'm trying to figure out how to do the two-transaction abstraction on the asynchronous FIFO right now.  I'm done with the control signals, though.00:01
promach_abstraction ..???00:01
ZipCPUSo, the issue is how do you prove that the FIFO actually acts like a, well, a FIFO.00:01
ZipCPUTo prove that, you need to place two values into the FIFO, and make certain that you can get those same two values out in the proper order.00:02
promach_with some latency00:02
ZipCPUYes ... and it has to get past induction too ... ;)00:02
promach_I am currently stucked with UART and RIFFA. I will need to do the do the asynchronous FIFO testing and verification next week or two :|00:03
ZipCPUSo why were you asking about satisfiability then?00:04
awygleZipCPU: i am working on a similar task, although that FIFO is synchronous00:04
awyglei've just about decided the problem is actually in my verilog rather than the asserts though...00:05
awyglewhich i suppose is nice00:05
promach_ZipCPU: I am trying to get into the theory of formal verification by looking at some online powerpoints00:05
ZipCPUawygle: "proving" a FIFO via the two-transaction abstraction?00:05
awygleZipCPU: i'm not familiar with that phrase00:06
ZipCPUpromach_: Why don't you introduce yourself with the theory via a counter example?  :P00:06
ZipCPUawygle: So, the theory is that to prove a FIFO you need to be able to place two values into the FIFO, and then read those same two values back out in the same order.00:06
awyglebut trying to prove a fifo "acts like a fifo"00:06
ZipCPUIf the values are arbitrary, then you can prove the property for all.00:07
ZipCPUMy former FIFO post handles proving the FIFO's control signals.00:07
awyglewhich, as i discovered this weekend, a) is nontrivial and b) doesn't actually mean your fifo works :P00:08
*** AlexDaniel has quit IRC00:09
ZipCPUDid you take a look at all at my post on the topic?00:09
awyglei did yes00:09
ZipCPUDid it help at all?00:10
awygleit did! as we discussed last week, i'm still not happy about having to break out the read and write pointers. that suggests to me that i am proving the wrong properties in some way00:12
ZipCPUawygle: So, there's a solution in SystemVerilog for that--the "bind" statement.00:13
ZipCPUUsing the "bind" statement, you can get "visibility" into the internal variables of submodules.00:13
ZipCPUyosys just doesn't support it .... yet.00:13
awyglehm yes i can see how that would be useful00:14
awyglebut i still feel it should be possible - if not convenient - to prove the module entirely from the outside00:14
ZipCPU... *and* pass induction??00:15
ZipCPUI can provide a fairly simple proof that it's not possible.00:15
awygleHmmm, a *proof*, or a thought experiment? ;-)00:16
ZipCPUMore along the lines of a very simple counter example.00:17
awygleI think we've been down this road before, but we both know more now than we did in November. Shoot!00:17
ZipCPUI think you'll like my example ... let me make some images of it.00:18
awygleThe problem with the fifo is that it can stay in a bad state for arbitrarily long by just... Not writing or reading.00:18
* ZipCPU is saving his example to imgur ...00:20
*** dxld has joined #yosys00:21
ZipCPUawygle: Take a look at this example,
tpbTitle: Imgur: The magic of the Internet (at
ZipCPUAlthough ... you might already know what's going on, still ... it makes a good example of the difficulty involved.00:22
ZipCPUAt any rate, that's my "fairly simple proof that it's not possible."00:23
awygleyep, i get what's going on00:26
awygleyou have a clock enable so there's nothing forcing induction to walk back to the beginning of the shift register and find an illegal state00:27
awyglebut there's a couple things which make it a less than compelling argument, in my view00:29
ZipCPUHow so?00:29
awyglelet me try to phrase it in a way that isn't an obscure literary allusion...00:31
awyglebasically, it's pretty easy in this contrived example to refuse to admit the validity of the property00:31
ZipCPUThat was sort of the purpose.00:32
awyglein this case, you don't just care that the last value is the same all the time. you either care that the 16th values are the same after 16 cycles with i_ce high, or that all the values are the same all the time00:33
awyglein the case of the fifo, no one actually cares about the relationship between count and read_ptr and write_ptr. that's not interesting except to the internal logic of the module00:33
awyglewhat we care about is that if "count" says 14, there have been 14 more cycles with "wr" high than with "rd" high00:34
awygle(or whatever the rules of your fifo w.r.t count are)00:34
ZipCPUThat alone should be simple to prove ... if you have insight into the FIFO ;)00:35
ZipCPUSo, the basic problem is that formal isn't a black box testing technique.  It's very much a *white* box testing technique.00:35
ZipCPU(There is also a ticking box testing technique--commonly used by certain big-name vendors ...)00:36
promach_ZipCPU: why do you call it white-box testing ? awygle is able to test it entirely by treating his UART as a black box00:38
awygleZipCPU: i'm not really in a position to argue with you, but i also share some of promach_'s skepticism. formal verification doesn't seem to be _inherently_ tied to either white or black box approaches00:42
ZipCPUawygle: promach_: There is another way, which is very popular among the big-chip vendors00:57
ZipCPUBasically, it works by listing out a series of formal properties--asserts, assumes, etc., and then simulating the design with those properties.00:58
ZipCPUThe external observer can then verify that the properties are met via simulation--just not via formal and hence not via *every* path through the design.00:59
ZipCPUawygle: I don't get promach_'s statement.  Are you able to *prove* your UART using black box testing?01:00
tpbTitle: spirit/character_recovery_formal.v at uart_lite_wip · awygle/spirit · GitHub (at
awygleZipCPU: well, parts of it. not, as we've noted, the FIFO01:00
ZipCPUThrough induction as well?01:01
awyglethe receiver portion is different because it doesn't have a clock enable01:01
awygleand even if it did, that would be "triggered" by an external event, and take a defined amount of time to proceed to the terminal state01:02
awygleas it is, i have to run for 200 cycles (with my present configuration) to make it pass induction01:02
promach_awygle: try induction depth of 1001:02
ZipCPUpromach_: Why?01:02
promach_awygle Rx coding might not have enough assert(). from my own coding experience, when I lower the induction depth, I need much more assert()01:03
*** jkiv has quit IRC01:04
promach_I am now working on passing induction at depth of 1001:04
awyglewell, if i wanted to pass at a lower induction depth, i would need to do internal assertions (or reduce the oversampling)01:04
ZipCPU"not enough assert()", but yet it still passes?01:04
promach_I mean for both Tx and Rx together01:04
ZipCPUIf it passes, it passes ... what would be the advantage of proving at a 10 clock depth?01:05
promach_it is not about advantage, it is more about how confident the code author is about the proof/verification through assert()01:06
ZipCPUIf the assert()'s present prove that the code works, even if it takes 200 clocks, then why would more asserts give you more confidence?01:07
promach_hmm... I am not trying to argue, but from my little experience, I did found some more bugs in the my UART verilog source code when I lower the induction depth01:08
ZipCPU"bugs"?  In the code, or the properties?01:08
promach_ZipCPU, awygle: I will come back in about half an hour as promach01:08
promach_in the code, I mean the source code, not properties01:08
* ZipCPU contemplates coming back as Darth Vader.01:09
promach_maybe I am wrong, but I got to go now. I will come back later as promach01:09
* ZipCPU considers coming back as promach even ...01:09
* awygle is safe from name-squatting because no one can spell (or pronounce) his name01:10
*** promach_ has quit IRC01:13
*** ZipCPU|Alt has joined #yosys01:23
*** m_t_ has quit IRC01:32
promachZipCPU, ZipCPU|Alt, awygle: I am back :)01:48
ZipCPUOh, okay, relax, there's nothing left to discuss--we got to the bottom of the life, universe, and indeed everything.  :P01:49
*** seldridge has joined #yosys01:50
promachZipCPU: but I do not really comprehend
tpbTitle: Imgur: The magic of the Internet (at
ZipCPUOk, why not?01:51
ZipCPUCare to try it?  It might help you understand your UART issue(s).01:52
promachZipCPU: give me an hour to think. I am stupid ;)01:53
ZipCPUNot really, you just haven't tried building things often enough.01:53
ZipCPUTry building it and testing it.  See what happens.01:54
*** promach_ has joined #yosys01:57
*** cemerick has quit IRC02:13
promachZipCPU: would you mind if I share and ask a questions about it on reddit ?02:18
tpbTitle: Imgur: The magic of the Internet (at
ZipCPUYes, I would.02:18
ZipCPUI would mind, so please don't.02:18
ZipCPUWhich reddit forum did you wish to ask a question on?02:18
promach /fpga02:19
ZipCPU.... and can that question be answered here?02:19
promachjust want to see some interesting replies02:19
ZipCPUpromach: Let's look at this from another viewpoint.  Imagine yourself the expert with the knowledge you've just learned.  What answer would you provide to your own question?02:20
promachI have no solution/answer to the i_ce question02:21
ZipCPUOk, did you look at the trace under induction?02:22
promachZipCPU: can I reply you when you wake up tomorrow morning. I am a bit stucked at my work currently. I mean RIFFA02:30
ZipCPUOk.  But, for your own development, please don't abandon the problem for others to solve.  In other words, let's continue the discussion here in the morning and I'll ask that you not post it elsewhere.02:31
promachZipCPU: ok02:32
*** emeb_mac has joined #yosys02:37
*** seldridge has quit IRC03:06
*** cemerick has joined #yosys03:21
*** cemerick has quit IRC03:30
*** puddingp1mp is now known as puddingpimp03:38
ZipCPUHey, blimey!  My serial port logic passes!  Wow, that's kind of exciting.03:44
qu1j0t3ZipCPU: congrats03:44
*** cr1901_modern1 has joined #yosys04:54
*** cr1901_modern has quit IRC04:56
*** sklv has quit IRC05:46
*** sklv has joined #yosys05:46
*** cr1901_modern1 has quit IRC05:50
*** cr1901_modern has joined #yosys05:55
*** promach has quit IRC06:02
*** promach has joined #yosys06:04
*** sklv has quit IRC06:26
*** sklv has joined #yosys06:27
*** promach has quit IRC06:39
*** xrexeon has joined #yosys06:43
*** pie_ has quit IRC06:57
*** promach has joined #yosys07:12
*** promach has quit IRC07:14
*** promach has joined #yosys07:15
*** xrexeon has quit IRC07:18
*** emeb_mac has quit IRC07:20
*** maartenBE has quit IRC07:34
*** maartenBE has joined #yosys07:37
*** AlexDaniel has joined #yosys08:02
*** _whitelogger has quit IRC08:06
*** _whitelogger_ has joined #yosys08:08
*** AlexDaniel has quit IRC08:13
*** AlexDaniel has joined #yosys08:15
*** fsasm_ has quit IRC08:19
*** dys has joined #yosys08:48
mattvenn_could I get some feedback on my i2c master09:35
tpbTitle: fpga-virtual-graf/i2c_master.v at master · mattvenn/fpga-virtual-graf · GitHub (at
mattvenn_it has a lot of shortcomings, including ignoring nacks09:36
mattvenn_but I've used it with a few sensors in the past09:36
mattvenn_I've just started using it with a new sensor and the device never acked09:36
mattvenn_after slowing the clock down my next guess was that SDA was changing too close to SCL09:38
mattvenn_so I added a delay between when the i2c_master module changed the pin and when the pin actually got changed09:38
mattvenn_now the sensor acks, but this 'fix' isn't really any good because the state machine expects to be able to read sda but in reality the pin hasn't changed direction.09:39
mattvenn_hope that makes sense09:39
mattvenn_I started trying to make the i2c master with an actual clock for SCL but switched to generating it as part of the state machine09:40
mattvenn_which is one reason there are so many states09:40
mattvenn_I'd like to avoid adding a whole new set of states to handle changing/reading SDA in between SCL low to high transitions09:40
mattvenn_but I'm not sure if I can do it09:41
mattvenn_maybe the whole thing needs a rewrite09:41
mattvenn_if anyone can spare some time to have a look and give me feedback I'd appreciate it509:41
*** cemerick has joined #yosys09:58
*** danieljabailey has quit IRC10:07
*** danieljabailey has joined #yosys10:08
*** digshadow has quit IRC10:14
*** sklv has quit IRC10:32
*** sklv has joined #yosys10:37
ZipCPUmattvenn_: I'm looking at  how you control your data line and comparing it to how you are controlling the clock line.11:35
ZipCPUBoth lines should have a : assign output_i2c_wire = (local_i2c_wire)  ? 1'bz : 1'b0;11:36
ZipCPUYou may find that the device you are trying to communicate with is trying to slow down the communication by stretching the clock line, and holding it low for some time.11:37
ZipCPUYou need to allow it to do this, and then slow down if it does.11:37
*** promach has quit IRC12:18
*** promach has joined #yosys12:20
*** fsasm has joined #yosys12:30
*** cemerick_ has joined #yosys13:16
*** cemerick has quit IRC13:20
*** xrexeon has joined #yosys13:32
*** xrexeon has quit IRC13:37
*** xrexeon has joined #yosys13:38
*** xrexeon has quit IRC13:54
mattvenn_thanks ZipCPU14:07
mattvenn_I agree that this is another thing the i2c_master module doesn't do14:07
mattvenn_but in this case it's not the problem, I already tried a much slower clock rate14:08
mattvenn_the problem here was timing between sda and scl. sda changing too close to the scl edges14:08
mattvenn_and I'm not sure how to handle this nicely14:08
ZipCPUWhen I built my own I2C controller, I think I split the clock into 4 phases at one point.  1 for the new data, 2 with the clock high, and 1 with the clock low before the new data on the next clock.14:10
mattvenn_and were each of those phases a separate FSM state?14:10
*** cemerick_ has quit IRC14:11
ZipCPUI think so.  I haven't looked at the code in a while, although it is published online.14:12
ZipCPUCheck out:
tpbTitle: GitHub - ZipCPU/wbi2c: Wishbone controlled I2C controllers (at
*** quigonjinn has quit IRC14:13
ZipCPUI think I needed two state machines to build it.  In one case (master/slave can't remember which) both are in the same file, whereas for the other they are split between two files.14:15
mattvenn_looks like the master is split14:16
*** promach__ has joined #yosys14:19
*** AlexDaniel has quit IRC14:44
*** seldridge has joined #yosys14:44
*** seldridge has quit IRC15:10
*** seldridge has joined #yosys15:14
*** AlexDaniel has joined #yosys16:03
*** fsasm has quit IRC16:10
*** xrexeon has joined #yosys16:13
*** eduardo_ has joined #yosys16:21
*** proteus-guy has quit IRC16:24
*** proteus-guy has joined #yosys16:24
*** eduardo__ has quit IRC16:25
*** seldridge has quit IRC16:30
*** xrexeon has quit IRC16:33
*** quigonjinn has joined #yosys16:57
*** maartenBE has quit IRC17:00
*** maartenBE has joined #yosys17:01
*** seldridge has joined #yosys17:08
*** seldridge has quit IRC17:09
*** seldridge has joined #yosys17:09
*** Exaeta-mobile2 has joined #yosys17:23
Exaeta-mobile2How complicated would I2C be for the 1k for example?17:24
Exaeta-mobile2I think I'm gonna try a smaller project first to familiarize myself with the I/O on a fpga17:25
ZipCPUMaster or slave?17:25
ZipCPUThe unoptimized I2C master I have requires 2271 LUT4's.17:26
ZipCPUThe slave uses 153 LUT4's.17:26
awygleZipCPU: wow, that many for the master? That's kind of surprising17:30
ZipCPUawygle: Yeah, you and me both.  I'm wondering what I did that made it that big.  Still, it was built for a 200k device where LUT's didn't need to be optimized.17:30
awygleCould just be I2C being terrible17:32
ZipCPUYeah, well, it's my own code ... I feel a bit responsible for such a large implementation.17:32
mattvenn_anyone know how to make gtkwave give me taller traces?17:45
mattvenn_they are annoyingly small;17:45
ravenexpthere's a gconf variable for that afair17:46
*** Exaeta-mobile has joined #yosys17:46
ravenexpor an ini file parameter17:47
*** Exaeta-mobile has joined #yosys17:47
ravenexpwhichever it uses17:47
Exaeta-mobileZipCPU: Master I think? I want to read data from two I2C modules and convert that to serial commands17:47
ZipCPUIt should be small in logic, but as you can see ... I must have messed something up in my own master since it is anything but small.  So, you can be certain an I2C master will fit in less than 2k logic blocks.17:48
*** Exaeta-mobile2 has quit IRC17:50
mattvenn_though handling all the clock stretching, multiple starts and stops etc... adds up17:52
ZipCPUmattvenn_: +117:53
mattvenn_my crappy one is using 260 LUTS, but it doesn't handle any of that stuff17:53
mattvenn_ravenexp: if you know how to do it, or know the parameter please let me know17:54
mattvenn_I've already read the manpage and searched the users guide17:54
mattvenn_was thinking of recompiling it!17:54
ravenexpman gtkwaverc17:56
ravenexpuse_big_fonts <value>17:59
*** dys has quit IRC18:03
*** cemerick_ has joined #yosys18:15
mattvenn_thanks, much better18:18
*** dys has joined #yosys18:26
*** digshadow has joined #yosys18:43
*** m_w has quit IRC18:45
*** promach__ has quit IRC19:44
*** cr1901_modern1 has joined #yosys19:55
*** cr1901_modern has quit IRC19:58
*** digshadow has quit IRC21:08
*** Exaeta-mobile2 has joined #yosys21:16
*** Exaeta-mobile has quit IRC21:17
*** xrexeon has joined #yosys21:20
*** Exaeta-mobile has joined #yosys21:36
*** Exaeta-mobile2 has quit IRC21:37
*** Exaeta-mobile has quit IRC21:53
*** Exaeta-mobile has joined #yosys22:02
*** cemerick_ is now known as cemerick22:07
*** Exaeta-mobile2 has joined #yosys22:16
*** Exaeta-mobile has quit IRC22:19
*** cemerick has quit IRC22:21
*** AlexDaniel has quit IRC22:30
*** digshadow has joined #yosys22:32
*** m_w has joined #yosys23:04
*** Exaeta-mobile has joined #yosys23:13
*** Exaeta-mobile2 has quit IRC23:14
*** GuzTech has quit IRC23:17
*** m_w has quit IRC23:22
*** Exaeta-mobile2 has joined #yosys23:25
*** Exaeta-mobile has quit IRC23:27
*** proteus-guy has quit IRC23:44
*** proteus-guy has joined #yosys23:44

Generated by 2.13.1 by Marius Gedminas - find it at!