| *** tpb has joined #yosys | 00:00 | |
| promach_ | ZipCPU: you are done with asynchronous FIFO and UART ? | 00:00 |
|---|---|---|
| promach_ | I mean formally verifiying | 00:00 |
| ZipCPU | Not 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 |
| ZipCPU | So, the issue is how do you prove that the FIFO actually acts like a, well, a FIFO. | 00:01 |
| ZipCPU | To 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 latency | 00:02 |
| ZipCPU | Yes ... 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 |
| ZipCPU | So why were you asking about satisfiability then? | 00:04 |
| awygle | ZipCPU: i am working on a similar task, although that FIFO is synchronous | 00:04 |
| awygle | i've just about decided the problem is actually in my verilog rather than the asserts though... | 00:05 |
| awygle | which i suppose is nice | 00:05 |
| promach_ | ZipCPU: I am trying to get into the theory of formal verification by looking at some online powerpoints | 00:05 |
| ZipCPU | awygle: "proving" a FIFO via the two-transaction abstraction? | 00:05 |
| awygle | ZipCPU: i'm not familiar with that phrase | 00:06 |
| ZipCPU | promach_: Why don't you introduce yourself with the theory via a counter example? :P | 00:06 |
| ZipCPU | awygle: 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 |
| awygle | but trying to prove a fifo "acts like a fifo" | 00:06 |
| ZipCPU | If the values are arbitrary, then you can prove the property for all. | 00:07 |
| ZipCPU | My former FIFO post handles proving the FIFO's control signals. | 00:07 |
| awygle | which, as i discovered this weekend, a) is nontrivial and b) doesn't actually mean your fifo works :P | 00:08 |
| ZipCPU | :D | 00:09 |
| *** AlexDaniel has quit IRC | 00:09 | |
| ZipCPU | Did you take a look at all at my post on the topic? | 00:09 |
| awygle | i did yes | 00:09 |
| ZipCPU | Did it help at all? | 00:10 |
| awygle | it 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 way | 00:12 |
| ZipCPU | awygle: So, there's a solution in SystemVerilog for that--the "bind" statement. | 00:13 |
| ZipCPU | Using the "bind" statement, you can get "visibility" into the internal variables of submodules. | 00:13 |
| ZipCPU | yosys just doesn't support it .... yet. | 00:13 |
| awygle | hm yes i can see how that would be useful | 00:14 |
| awygle | but i still feel it should be possible - if not convenient - to prove the module entirely from the outside | 00:14 |
| ZipCPU | ... *and* pass induction?? | 00:15 |
| ZipCPU | I can provide a fairly simple proof that it's not possible. | 00:15 |
| awygle | Hmmm, a *proof*, or a thought experiment? ;-) | 00:16 |
| ZipCPU | More along the lines of a very simple counter example. | 00:17 |
| awygle | I think we've been down this road before, but we both know more now than we did in November. Shoot! | 00:17 |
| ZipCPU | I think you'll like my example ... let me make some images of it. | 00:18 |
| awygle | The 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 #yosys | 00:21 | |
| ZipCPU | awygle: Take a look at this example, https://imgur.com/a/MMr3c | 00:21 |
| tpb | Title: Imgur: The magic of the Internet (at imgur.com) | 00:21 |
| ZipCPU | Although ... you might already know what's going on, still ... it makes a good example of the difficulty involved. | 00:22 |
| ZipCPU | At any rate, that's my "fairly simple proof that it's not possible." | 00:23 |
| awygle | yep, i get what's going on | 00:26 |
| awygle | you have a clock enable so there's nothing forcing induction to walk back to the beginning of the shift register and find an illegal state | 00:27 |
| awygle | but there's a couple things which make it a less than compelling argument, in my view | 00:29 |
| ZipCPU | How so? | 00:29 |
| awygle | let me try to phrase it in a way that isn't an obscure literary allusion... | 00:31 |
| awygle | basically, it's pretty easy in this contrived example to refuse to admit the validity of the property | 00:31 |
| ZipCPU | That was sort of the purpose. | 00:32 |
| awygle | in 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 time | 00:33 |
| awygle | in 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 module | 00:33 |
| awygle | what we care about is that if "count" says 14, there have been 14 more cycles with "wr" high than with "rd" high | 00:34 |
| awygle | (or whatever the rules of your fifo w.r.t count are) | 00:34 |
| ZipCPU | That alone should be simple to prove ... if you have insight into the FIFO ;) | 00:35 |
| ZipCPU | So, 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 |
| awygle | lol | 00:38 |
| promach_ | ZipCPU: why do you call it white-box testing ? awygle is able to test it entirely by treating his UART as a black box | 00:38 |
| awygle | ZipCPU: 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 approaches | 00:42 |
| ZipCPU | awygle: promach_: There is another way, which is very popular among the big-chip vendors | 00:57 |
| ZipCPU | Basically, it works by listing out a series of formal properties--asserts, assumes, etc., and then simulating the design with those properties. | 00:58 |
| ZipCPU | The 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 |
| ZipCPU | awygle: I don't get promach_'s statement. Are you able to *prove* your UART using black box testing? | 01:00 |
| promach_ | ZipCPU: https://github.com/awygle/spirit/blob/uart_lite_wip/uart_lite/verification/character_recovery_formal.v | 01:00 |
| tpb | Title: spirit/character_recovery_formal.v at uart_lite_wip · awygle/spirit · GitHub (at github.com) | 01:00 |
| awygle | ZipCPU: well, parts of it. not, as we've noted, the FIFO | 01:00 |
| ZipCPU | Through induction as well? | 01:01 |
| awygle | the receiver portion is different because it doesn't have a clock enable | 01:01 |
| awygle | (currently_ | 01:01 |
| awygle | and even if it did, that would be "triggered" by an external event, and take a defined amount of time to proceed to the terminal state | 01:02 |
| awygle | as it is, i have to run for 200 cycles (with my present configuration) to make it pass induction | 01:02 |
| promach_ | awygle: try induction depth of 10 | 01:02 |
| ZipCPU | promach_: 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 IRC | 01:04 | |
| promach_ | I am now working on passing induction at depth of 10 | 01:04 |
| awygle | well, 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 together | 01:04 |
| ZipCPU | If 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 |
| ZipCPU | If 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 depth | 01:08 |
| ZipCPU | "bugs"? In the code, or the properties? | 01:08 |
| promach_ | ZipCPU, awygle: I will come back in about half an hour as promach | 01:08 |
| promach_ | in the code, I mean the source code, not properties | 01: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 promach | 01:09 |
| * ZipCPU considers coming back as promach even ... | 01:09 | |
| * awygle is safe from name-squatting because no one can spell (or pronounce) his name | 01:10 | |
| *** promach_ has quit IRC | 01:13 | |
| *** ZipCPU|Alt has joined #yosys | 01:23 | |
| *** m_t_ has quit IRC | 01:32 | |
| promach | ZipCPU, ZipCPU|Alt, awygle: I am back :) | 01:48 |
| ZipCPU | Oh, okay, relax, there's nothing left to discuss--we got to the bottom of the life, universe, and indeed everything. :P | 01:49 |
| *** seldridge has joined #yosys | 01:50 | |
| promach | ZipCPU: but I do not really comprehend https://imgur.com/a/MMr3c | 01:51 |
| tpb | Title: Imgur: The magic of the Internet (at imgur.com) | 01:51 |
| ZipCPU | Ok, why not? | 01:51 |
| ZipCPU | Care to try it? It might help you understand your UART issue(s). | 01:52 |
| promach | ZipCPU: give me an hour to think. I am stupid ;) | 01:53 |
| ZipCPU | Not really, you just haven't tried building things often enough. | 01:53 |
| ZipCPU | Try building it and testing it. See what happens. | 01:54 |
| *** promach_ has joined #yosys | 01:57 | |
| *** cemerick has quit IRC | 02:13 | |
| promach | ZipCPU: would you mind if I share https://imgur.com/a/MMr3c and ask a questions about it on reddit ? | 02:18 |
| tpb | Title: Imgur: The magic of the Internet (at imgur.com) | 02:18 |
| ZipCPU | Yes, I would. | 02:18 |
| ZipCPU | I would mind, so please don't. | 02:18 |
| promach | ok | 02:18 |
| ZipCPU | Which reddit forum did you wish to ask a question on? | 02:18 |
| promach | /fpga | 02:19 |
| ZipCPU | .... and can that question be answered here? | 02:19 |
| promach | just want to see some interesting replies | 02:19 |
| ZipCPU | promach: 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 |
| promach | I have no solution/answer to the i_ce question | 02:21 |
| ZipCPU | Ok, did you look at the trace under induction? | 02:22 |
| ZipCPU | promach? | 02:26 |
| promach | ZipCPU: can I reply you when you wake up tomorrow morning. I am a bit stucked at my work currently. I mean RIFFA | 02:30 |
| ZipCPU | Ok. 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 |
| promach | ZipCPU: ok | 02:32 |
| ZipCPU | :) | 02:32 |
| *** emeb_mac has joined #yosys | 02:37 | |
| *** seldridge has quit IRC | 03:06 | |
| *** cemerick has joined #yosys | 03:21 | |
| *** cemerick has quit IRC | 03:30 | |
| *** puddingp1mp is now known as puddingpimp | 03:38 | |
| ZipCPU | Hey, blimey! My serial port logic passes! Wow, that's kind of exciting. | 03:44 |
| qu1j0t3 | ZipCPU: congrats | 03:44 |
| ZipCPU | Thanks! | 03:45 |
| *** cr1901_modern1 has joined #yosys | 04:54 | |
| *** cr1901_modern has quit IRC | 04:56 | |
| *** sklv has quit IRC | 05:46 | |
| *** sklv has joined #yosys | 05:46 | |
| *** cr1901_modern1 has quit IRC | 05:50 | |
| *** cr1901_modern has joined #yosys | 05:55 | |
| *** promach has quit IRC | 06:02 | |
| *** promach has joined #yosys | 06:04 | |
| *** sklv has quit IRC | 06:26 | |
| *** sklv has joined #yosys | 06:27 | |
| *** promach has quit IRC | 06:39 | |
| *** xrexeon has joined #yosys | 06:43 | |
| *** pie_ has quit IRC | 06:57 | |
| *** promach has joined #yosys | 07:12 | |
| *** promach has quit IRC | 07:14 | |
| *** promach has joined #yosys | 07:15 | |
| *** xrexeon has quit IRC | 07:18 | |
| *** emeb_mac has quit IRC | 07:20 | |
| *** maartenBE has quit IRC | 07:34 | |
| *** maartenBE has joined #yosys | 07:37 | |
| *** AlexDaniel has joined #yosys | 08:02 | |
| *** _whitelogger has quit IRC | 08:06 | |
| *** _whitelogger_ has joined #yosys | 08:08 | |
| *** AlexDaniel has quit IRC | 08:13 | |
| *** AlexDaniel has joined #yosys | 08:15 | |
| *** fsasm_ has quit IRC | 08:19 | |
| *** dys has joined #yosys | 08:48 | |
| mattvenn_ | could I get some feedback on my i2c master | 09:35 |
| mattvenn_ | https://github.com/mattvenn/fpga-virtual-graf/blob/master/src/i2c_master.v | 09:35 |
| tpb | Title: fpga-virtual-graf/i2c_master.v at master · mattvenn/fpga-virtual-graf · GitHub (at github.com) | 09:35 |
| mattvenn_ | it has a lot of shortcomings, including ignoring nacks | 09:36 |
| mattvenn_ | but I've used it with a few sensors in the past | 09:36 |
| mattvenn_ | I've just started using it with a new sensor and the device never acked | 09:36 |
| mattvenn_ | https://imagebin.ca/v/3u2Y99M4EwIh | 09:37 |
| mattvenn_ | after slowing the clock down my next guess was that SDA was changing too close to SCL | 09:38 |
| mattvenn_ | so I added a delay between when the i2c_master module changed the pin and when the pin actually got changed | 09: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 sense | 09: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 machine | 09:40 |
| mattvenn_ | which is one reason there are so many states | 09: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 transitions | 09:40 |
| mattvenn_ | but I'm not sure if I can do it | 09:41 |
| mattvenn_ | maybe the whole thing needs a rewrite | 09:41 |
| mattvenn_ | if anyone can spare some time to have a look and give me feedback I'd appreciate it5 | 09:41 |
| *** cemerick has joined #yosys | 09:58 | |
| *** danieljabailey has quit IRC | 10:07 | |
| *** danieljabailey has joined #yosys | 10:08 | |
| *** digshadow has quit IRC | 10:14 | |
| *** sklv has quit IRC | 10:32 | |
| *** sklv has joined #yosys | 10:37 | |
| ZipCPU | mattvenn_: I'm looking at how you control your data line and comparing it to how you are controlling the clock line. | 11:35 |
| ZipCPU | Both lines should have a : assign output_i2c_wire = (local_i2c_wire) ? 1'bz : 1'b0; | 11:36 |
| ZipCPU | You 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 |
| ZipCPU | You need to allow it to do this, and then slow down if it does. | 11:37 |
| *** promach has quit IRC | 12:18 | |
| *** promach has joined #yosys | 12:20 | |
| *** fsasm has joined #yosys | 12:30 | |
| *** cemerick_ has joined #yosys | 13:16 | |
| *** cemerick has quit IRC | 13:20 | |
| *** xrexeon has joined #yosys | 13:32 | |
| *** xrexeon has quit IRC | 13:37 | |
| *** xrexeon has joined #yosys | 13:38 | |
| *** xrexeon has quit IRC | 13:54 | |
| mattvenn_ | thanks ZipCPU | 14:07 |
| mattvenn_ | I agree that this is another thing the i2c_master module doesn't do | 14:07 |
| mattvenn_ | but in this case it's not the problem, I already tried a much slower clock rate | 14:08 |
| mattvenn_ | the problem here was timing between sda and scl. sda changing too close to the scl edges | 14:08 |
| mattvenn_ | and I'm not sure how to handle this nicely | 14:08 |
| ZipCPU | Ok | 14:09 |
| ZipCPU | When 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 IRC | 14:11 | |
| ZipCPU | I think so. I haven't looked at the code in a while, although it is published online. | 14:12 |
| ZipCPU | Check out: https://github.com/ZipCPU/wbi2c | 14:12 |
| tpb | Title: GitHub - ZipCPU/wbi2c: Wishbone controlled I2C controllers (at github.com) | 14:12 |
| *** quigonjinn has quit IRC | 14:13 | |
| mattvenn_ | thanks | 14:14 |
| ZipCPU | I 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 split | 14:16 |
| *** promach__ has joined #yosys | 14:19 | |
| *** AlexDaniel has quit IRC | 14:44 | |
| *** seldridge has joined #yosys | 14:44 | |
| *** seldridge has quit IRC | 15:10 | |
| *** seldridge has joined #yosys | 15:14 | |
| *** AlexDaniel has joined #yosys | 16:03 | |
| *** fsasm has quit IRC | 16:10 | |
| *** xrexeon has joined #yosys | 16:13 | |
| *** eduardo_ has joined #yosys | 16:21 | |
| *** proteus-guy has quit IRC | 16:24 | |
| *** proteus-guy has joined #yosys | 16:24 | |
| *** eduardo__ has quit IRC | 16:25 | |
| *** seldridge has quit IRC | 16:30 | |
| *** xrexeon has quit IRC | 16:33 | |
| *** quigonjinn has joined #yosys | 16:57 | |
| *** maartenBE has quit IRC | 17:00 | |
| *** maartenBE has joined #yosys | 17:01 | |
| *** seldridge has joined #yosys | 17:08 | |
| *** seldridge has quit IRC | 17:09 | |
| *** seldridge has joined #yosys | 17:09 | |
| *** Exaeta-mobile2 has joined #yosys | 17:23 | |
| Exaeta-mobile2 | How complicated would I2C be for the 1k for example? | 17:24 |
| Exaeta-mobile2 | I think I'm gonna try a smaller project first to familiarize myself with the I/O on a fpga | 17:25 |
| ZipCPU | Master or slave? | 17:25 |
| ZipCPU | The unoptimized I2C master I have requires 2271 LUT4's. | 17:26 |
| ZipCPU | The slave uses 153 LUT4's. | 17:26 |
| awygle | ZipCPU: wow, that many for the master? That's kind of surprising | 17:30 |
| ZipCPU | awygle: 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 |
| awygle | Could just be I2C being terrible | 17:32 |
| ZipCPU | Yeah, 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 |
| ravenexp | there's a gconf variable for that afair | 17:46 |
| *** Exaeta-mobile has joined #yosys | 17:46 | |
| ravenexp | or an ini file parameter | 17:47 |
| *** Exaeta-mobile has joined #yosys | 17:47 | |
| ravenexp | whichever it uses | 17:47 |
| Exaeta-mobile | ZipCPU: Master I think? I want to read data from two I2C modules and convert that to serial commands | 17:47 |
| ZipCPU | It 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 IRC | 17:50 | |
| mattvenn_ | though handling all the clock stretching, multiple starts and stops etc... adds up | 17:52 |
| ZipCPU | mattvenn_: +1 | 17:53 |
| mattvenn_ | my crappy one is using 260 LUTS, but it doesn't handle any of that stuff | 17:53 |
| mattvenn_ | ravenexp: if you know how to do it, or know the parameter please let me know | 17:54 |
| mattvenn_ | I've already read the manpage and searched the users guide | 17:54 |
| mattvenn_ | was thinking of recompiling it! | 17:54 |
| ravenexp | man gtkwaverc | 17:56 |
| ravenexp | use_big_fonts <value> | 17:59 |
| *** dys has quit IRC | 18:03 | |
| *** cemerick_ has joined #yosys | 18:15 | |
| mattvenn_ | thanks, much better | 18:18 |
| *** dys has joined #yosys | 18:26 | |
| *** digshadow has joined #yosys | 18:43 | |
| *** m_w has quit IRC | 18:45 | |
| *** promach__ has quit IRC | 19:44 | |
| *** cr1901_modern1 has joined #yosys | 19:55 | |
| *** cr1901_modern has quit IRC | 19:58 | |
| *** digshadow has quit IRC | 21:08 | |
| *** Exaeta-mobile2 has joined #yosys | 21:16 | |
| *** Exaeta-mobile has quit IRC | 21:17 | |
| *** xrexeon has joined #yosys | 21:20 | |
| *** Exaeta-mobile has joined #yosys | 21:36 | |
| *** Exaeta-mobile2 has quit IRC | 21:37 | |
| *** Exaeta-mobile has quit IRC | 21:53 | |
| *** Exaeta-mobile has joined #yosys | 22:02 | |
| *** cemerick_ is now known as cemerick | 22:07 | |
| *** Exaeta-mobile2 has joined #yosys | 22:16 | |
| *** Exaeta-mobile has quit IRC | 22:19 | |
| *** cemerick has quit IRC | 22:21 | |
| *** AlexDaniel has quit IRC | 22:30 | |
| *** digshadow has joined #yosys | 22:32 | |
| *** m_w has joined #yosys | 23:04 | |
| *** Exaeta-mobile has joined #yosys | 23:13 | |
| *** Exaeta-mobile2 has quit IRC | 23:14 | |
| *** GuzTech has quit IRC | 23:17 | |
| *** m_w has quit IRC | 23:22 | |
| *** Exaeta-mobile2 has joined #yosys | 23:25 | |
| *** Exaeta-mobile has quit IRC | 23:27 | |
| *** proteus-guy has quit IRC | 23:44 | |
| *** proteus-guy has joined #yosys | 23:44 | |
Generated by irclog2html.py 2.13.1 by Marius Gedminas - find it at mg.pov.lt!