clifford changed the topic of #yosys to: Yosys Open SYnthesis Suite: http://www.clifford.at/yosys/ -- Channel Logs: https://irclog.whitequark.org/yosys
<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 :|
<ZipCPU> So why were you asking about satisfiability then?
<awygle> ZipCPU: i am working on a similar task, although that FIFO is synchronous
<awygle> i've just about decided the problem is actually in my verilog rather than the asserts though...
<awygle> which i suppose is nice
<promach_> ZipCPU: I am trying to get into the theory of formal verification by looking at some online powerpoints
<ZipCPU> awygle: "proving" a FIFO via the two-transaction abstraction?
<awygle> ZipCPU: i'm not familiar with that phrase
<ZipCPU> promach_: Why don't you introduce yourself with the theory via a counter example? :P
<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.
<awygle> but trying to prove a fifo "acts like a fifo"
<ZipCPU> If the values are arbitrary, then you can prove the property for all.
<ZipCPU> My former FIFO post handles proving the FIFO's control signals.
<awygle> which, as i discovered this weekend, a) is nontrivial and b) doesn't actually mean your fifo works :P
<ZipCPU> :D
AlexDaniel has quit [Ping timeout: 276 seconds]
<ZipCPU> Did you take a look at all at my post on the topic?
<awygle> i did yes
<ZipCPU> Did it help at all?
<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
<ZipCPU> awygle: So, there's a solution in SystemVerilog for that--the "bind" statement.
<ZipCPU> Using the "bind" statement, you can get "visibility" into the internal variables of submodules.
<ZipCPU> yosys just doesn't support it .... yet.
<awygle> hm yes i can see how that would be useful
<awygle> but i still feel it should be possible - if not convenient - to prove the module entirely from the outside
<ZipCPU> ... *and* pass induction??
<ZipCPU> I can provide a fairly simple proof that it's not possible.
<awygle> Hmmm, a *proof*, or a thought experiment? ;-)
<ZipCPU> More along the lines of a very simple counter example.
<awygle> I think we've been down this road before, but we both know more now than we did in November. Shoot!
<ZipCPU> I think you'll like my example ... let me make some images of it.
<awygle> The problem with the fifo is that it can stay in a bad state for arbitrarily long by just... Not writing or reading.
* ZipCPU is saving his example to imgur ...
dxld has joined #yosys
<ZipCPU> awygle: Take a look at this example, https://imgur.com/a/MMr3c
<tpb> Title: Imgur: The magic of the Internet (at imgur.com)
<ZipCPU> Although ... you might already know what's going on, still ... it makes a good example of the difficulty involved.
<ZipCPU> At any rate, that's my "fairly simple proof that it's not possible."
<awygle> yep, i get what's going on
<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
<awygle> but there's a couple things which make it a less than compelling argument, in my view
<ZipCPU> How so?
<awygle> let me try to phrase it in a way that isn't an obscure literary allusion...
<awygle> basically, it's pretty easy in this contrived example to refuse to admit the validity of the property
<ZipCPU> That was sort of the purpose.
<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
<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
<awygle> what we care about is that if "count" says 14, there have been 14 more cycles with "wr" high than with "rd" high
<awygle> (or whatever the rules of your fifo w.r.t count are)
<ZipCPU> That alone should be simple to prove ... if you have insight into the FIFO ;)
<ZipCPU> So, the basic problem is that formal isn't a black box testing technique. It's very much a *white* box testing technique.
<ZipCPU> (There is also a ticking box testing technique--commonly used by certain big-name vendors ...)
<awygle> lol
<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
<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
<ZipCPU> awygle: promach_: There is another way, which is very popular among the big-chip vendors
<ZipCPU> Basically, it works by listing out a series of formal properties--asserts, assumes, etc., and then simulating the design with those properties.
<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.
<ZipCPU> awygle: I don't get promach_'s statement. Are you able to *prove* your UART using black box testing?
<tpb> Title: spirit/character_recovery_formal.v at uart_lite_wip · awygle/spirit · GitHub (at github.com)
<awygle> ZipCPU: well, parts of it. not, as we've noted, the FIFO
<ZipCPU> Through induction as well?
<awygle> the receiver portion is different because it doesn't have a clock enable
<awygle> (currently_
<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
<awygle> as it is, i have to run for 200 cycles (with my present configuration) to make it pass induction
<promach_> awygle: try induction depth of 10
<ZipCPU> promach_: Why?
<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()
jkiv has quit [Quit: Leaving]
<promach_> I am now working on passing induction at depth of 10
<awygle> well, if i wanted to pass at a lower induction depth, i would need to do internal assertions (or reduce the oversampling)
<ZipCPU> "not enough assert()", but yet it still passes?
<promach_> I mean for both Tx and Rx together
<ZipCPU> If it passes, it passes ... what would be the advantage of proving at a 10 clock depth?
<promach_> it is not about advantage, it is more about how confident the code author is about the proof/verification through assert()
<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?
<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
<ZipCPU> "bugs"? In the code, or the properties?
<promach_> ZipCPU, awygle: I will come back in about half an hour as promach
<promach_> in the code, I mean the source code, not properties
* ZipCPU contemplates coming back as Darth Vader.
<promach_> maybe I am wrong, but I got to go now. I will come back later as promach
* ZipCPU considers coming back as promach even ...
* awygle is safe from name-squatting because no one can spell (or pronounce) his name
promach_ has quit [Ping timeout: 252 seconds]
ZipCPU|Alt has joined #yosys
ZipCPU|Alt has quit [Remote host closed the connection]
m_t_ has quit [Quit: Leaving]
<promach> ZipCPU, ZipCPU|Alt, awygle: I am back :)
<ZipCPU> Oh, okay, relax, there's nothing left to discuss--we got to the bottom of the life, universe, and indeed everything. :P
seldridge has joined #yosys
<promach> ZipCPU: but I do not really comprehend https://imgur.com/a/MMr3c
<tpb> Title: Imgur: The magic of the Internet (at imgur.com)
<ZipCPU> Ok, why not?
<ZipCPU> Care to try it? It might help you understand your UART issue(s).
<promach> ZipCPU: give me an hour to think. I am stupid ;)
<ZipCPU> Not really, you just haven't tried building things often enough.
<ZipCPU> Try building it and testing it. See what happens.
promach_ has joined #yosys
cemerick has quit [Ping timeout: 240 seconds]
<promach> ZipCPU: would you mind if I share https://imgur.com/a/MMr3c and ask a questions about it on reddit ?
<tpb> Title: Imgur: The magic of the Internet (at imgur.com)
<ZipCPU> Yes, I would.
<ZipCPU> I would mind, so please don't.
<promach> ok
<ZipCPU> Which reddit forum did you wish to ask a question on?
<promach> /fpga
<ZipCPU> .... and can that question be answered here?
<promach> just want to see some interesting replies
<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?
<promach> I have no solution/answer to the i_ce question
<ZipCPU> Ok, did you look at the trace under induction?
<ZipCPU> promach?
<promach> ZipCPU: can I reply you when you wake up tomorrow morning. I am a bit stucked at my work currently. I mean RIFFA
<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.
<promach> ZipCPU: ok
<ZipCPU> :)
emeb_mac has joined #yosys
seldridge has quit [Ping timeout: 256 seconds]
cemerick has joined #yosys
cemerick has quit [Ping timeout: 264 seconds]
puddingp1mp is now known as puddingpimp
<ZipCPU> Hey, blimey! My serial port logic passes! Wow, that's kind of exciting.
<qu1j0t3> ZipCPU: congrats
<ZipCPU> Thanks!
cr1901_modern1 has joined #yosys
cr1901_modern has quit [Ping timeout: 264 seconds]
sklv has quit [Remote host closed the connection]
sklv has joined #yosys
cr1901_modern1 has quit [Ping timeout: 264 seconds]
cr1901_modern has joined #yosys
promach has quit [Quit: WeeChat 2.1-dev]
promach has joined #yosys
sklv has quit [Remote host closed the connection]
sklv has joined #yosys
promach has quit [Quit: WeeChat 2.1-dev]
xrexeon has joined #yosys
pie_ has quit [Ping timeout: 248 seconds]
promach has joined #yosys
promach has quit [Quit: WeeChat 2.1-dev]
promach has joined #yosys
xrexeon has quit [Remote host closed the connection]
emeb_mac has quit [Quit: emeb_mac]
maartenBE has quit [Ping timeout: 248 seconds]
maartenBE has joined #yosys
AlexDaniel has joined #yosys
_whitelogger_ has joined #yosys
AlexDaniel has quit [Ping timeout: 260 seconds]
AlexDaniel has joined #yosys
fsasm_ has quit [Ping timeout: 240 seconds]
dys has joined #yosys
<mattvenn_> could I get some feedback on my i2c master
<tpb> Title: fpga-virtual-graf/i2c_master.v at master · mattvenn/fpga-virtual-graf · GitHub (at github.com)
<mattvenn_> it has a lot of shortcomings, including ignoring nacks
<mattvenn_> but I've used it with a few sensors in the past
<mattvenn_> I've just started using it with a new sensor and the device never acked
<mattvenn_> after slowing the clock down my next guess was that SDA was changing too close to SCL
<mattvenn_> so I added a delay between when the i2c_master module changed the pin and when the pin actually got changed
<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.
<mattvenn_> hope that makes sense
<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
<mattvenn_> which is one reason there are so many states
<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
<mattvenn_> but I'm not sure if I can do it
<mattvenn_> maybe the whole thing needs a rewrite
<mattvenn_> if anyone can spare some time to have a look and give me feedback I'd appreciate it5
cemerick has joined #yosys
danieljabailey has quit [Ping timeout: 248 seconds]
danieljabailey has joined #yosys
digshadow has quit [Ping timeout: 252 seconds]
sklv has quit [Remote host closed the connection]
sklv has joined #yosys
<ZipCPU> mattvenn_: I'm looking at how you control your data line and comparing it to how you are controlling the clock line.
<ZipCPU> Both lines should have a : assign output_i2c_wire = (local_i2c_wire) ? 1'bz : 1'b0;
<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.
<ZipCPU> You need to allow it to do this, and then slow down if it does.
promach has quit [Quit: WeeChat 2.1-dev]
promach has joined #yosys
fsasm has joined #yosys
cemerick_ has joined #yosys
cemerick has quit [Ping timeout: 256 seconds]
xrexeon has joined #yosys
xrexeon has quit [Remote host closed the connection]
xrexeon has joined #yosys
xrexeon has quit [Remote host closed the connection]
<mattvenn_> thanks ZipCPU
<mattvenn_> I agree that this is another thing the i2c_master module doesn't do
<mattvenn_> but in this case it's not the problem, I already tried a much slower clock rate
<mattvenn_> the problem here was timing between sda and scl. sda changing too close to the scl edges
<mattvenn_> and I'm not sure how to handle this nicely
<ZipCPU> Ok
<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.
<mattvenn_> and were each of those phases a separate FSM state?
cemerick_ has quit [Ping timeout: 260 seconds]
<ZipCPU> I think so. I haven't looked at the code in a while, although it is published online.
<tpb> Title: GitHub - ZipCPU/wbi2c: Wishbone controlled I2C controllers (at github.com)
quigonjinn has quit [Ping timeout: 256 seconds]
<mattvenn_> thanks
<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.
<mattvenn_> looks like the master is split
promach__ has joined #yosys
AlexDaniel has quit [Ping timeout: 255 seconds]
seldridge has joined #yosys
seldridge has quit [Ping timeout: 252 seconds]
seldridge has joined #yosys
AlexDaniel has joined #yosys
fsasm has quit [Ping timeout: 264 seconds]
xrexeon has joined #yosys
eduardo_ has joined #yosys
proteus-guy has quit [Quit: Leaving]
proteus-guy has joined #yosys
eduardo__ has quit [Ping timeout: 260 seconds]
seldridge has quit [Ping timeout: 245 seconds]
xrexeon has quit [Ping timeout: 264 seconds]
quigonjinn has joined #yosys
maartenBE has quit [Ping timeout: 256 seconds]
maartenBE has joined #yosys
seldridge has joined #yosys
seldridge has quit [Client Quit]
seldridge has joined #yosys
Exaeta-mobile2 has joined #yosys
<Exaeta-mobile2> How complicated would I2C be for the 1k for example?
<Exaeta-mobile2> I think I'm gonna try a smaller project first to familiarize myself with the I/O on a fpga
<ZipCPU> Master or slave?
<ZipCPU> The unoptimized I2C master I have requires 2271 LUT4's.
<ZipCPU> The slave uses 153 LUT4's.
<awygle> ZipCPU: wow, that many for the master? That's kind of surprising
<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.
<awygle> Could just be I2C being terrible
<ZipCPU> Yeah, well, it's my own code ... I feel a bit responsible for such a large implementation.
<mattvenn_> anyone know how to make gtkwave give me taller traces?
<mattvenn_> they are annoyingly small;
<ravenexp> there's a gconf variable for that afair
Exaeta-mobile has joined #yosys
Exaeta-mobile has quit [Client Quit]
<ravenexp> or an ini file parameter
Exaeta-mobile has joined #yosys
<ravenexp> whichever it uses
<Exaeta-mobile> ZipCPU: Master I think? I want to read data from two I2C modules and convert that to serial commands
<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.
Exaeta-mobile2 has quit [Ping timeout: 245 seconds]
<mattvenn_> though handling all the clock stretching, multiple starts and stops etc... adds up
<ZipCPU> mattvenn_: +1
<mattvenn_> my crappy one is using 260 LUTS, but it doesn't handle any of that stuff
<mattvenn_> ravenexp: if you know how to do it, or know the parameter please let me know
<mattvenn_> I've already read the manpage and searched the users guide
<mattvenn_> was thinking of recompiling it!
<ravenexp> man gtkwaverc
<ravenexp> use_big_fonts <value>
dys has quit [Ping timeout: 240 seconds]
cemerick_ has joined #yosys
<mattvenn_> thanks, much better
dys has joined #yosys
digshadow has joined #yosys
m_w has quit [Quit: leaving]
promach__ has quit [Ping timeout: 240 seconds]
cr1901_modern1 has joined #yosys
cr1901_modern has quit [Ping timeout: 264 seconds]
digshadow has quit [Ping timeout: 256 seconds]
Exaeta-mobile2 has joined #yosys
Exaeta-mobile has quit [Ping timeout: 260 seconds]
xrexeon has joined #yosys
Exaeta-mobile has joined #yosys
Exaeta-mobile2 has quit [Ping timeout: 245 seconds]
Exaeta-mobile has quit [Ping timeout: 265 seconds]
Exaeta-mobile has joined #yosys
cemerick_ is now known as cemerick
Exaeta-mobile2 has joined #yosys
Exaeta-mobile has quit [Ping timeout: 276 seconds]
cemerick has quit [Ping timeout: 260 seconds]
AlexDaniel has quit [Ping timeout: 252 seconds]
digshadow has joined #yosys
m_w has joined #yosys
Exaeta-mobile has joined #yosys
Exaeta-mobile2 has quit [Ping timeout: 245 seconds]
GuzTech has quit [Ping timeout: 268 seconds]
m_w has quit [Quit: leaving]
Exaeta-mobile2 has joined #yosys
Exaeta-mobile has quit [Ping timeout: 245 seconds]
proteus-guy has quit [Ping timeout: 245 seconds]
proteus-guy has joined #yosys
tpb has quit [Remote host closed the connection]
tpb has joined #yosys