clifford changed the topic of #yosys to: Yosys Open SYnthesis Suite: http://www.clifford.at/yosys/ -- Channel Logs: https://irclog.whitequark.org/yosys
pie_ has quit [Ping timeout: 240 seconds]
pie_ has joined #yosys
hobbes- has quit [Quit: ZNC - http://znc.in]
philgekni has quit [Quit: ZNC - http://znc.in]
gnufan has quit [Quit: Leaving.]
<promach> ZipCPU: what do you think about 'flatten' command ?
<ZipCPU> As with everything, it has its purpose.
m_t has quit [Quit: Leaving]
<promach> so, 'flaten' is not to be used for referencing signals from other levels in the hierarchy ?
<promach> I mean during formal verification
<promach> it seems to me that 'flatten' is only for the purpose of synthesis
<promach> ZipCPU
<ZipCPU> What tool are you referencing? yosys?
<ZipCPU> Verilator has a flatten as well.
<ZipCPU> What are you trying to accomplish?
[X-Scale] has joined #yosys
X-Scale has quit [Ping timeout: 240 seconds]
[X-Scale] is now known as X-Scale
m_w has quit [Quit: Leaving]
<promach__> ZipCPU: yosys-smtbmc
<ZipCPU> Ok, so ... go on, what are you trying to accomplsih?
<promach__> ZipCPU: remember the verific that you mentioned
<promach__> ?
<ZipCPU> Ahm, okay ... go on
<promach__> calling variables from other hierarchy is not yet supported currently in yosys-smtbmc
<promach__> ZipCPU: do you remember ?
<ZipCPU> Ok, go on ...
<ZipCPU> Sure, go on ...
<promach__> I just found out about 'flatten' command this morning
<promach__> but I guess that 'flatten' is only for synthesis
<ZipCPU> "flatten" doesn't solve your problem, if that's what you are asking about.
<promach__> :|
<ZipCPU> Did you read the article about proving the ZipCPU prefetch?
<ZipCPU> ;D No, the one about formally proving the prefetch.
<ZipCPU> See ... one of the common problem's I've had is that modules that use the formal bus properties need values from that property list.
<ZipCPU> For example, the formal properties count the number of outstanding transactions.
<promach__> Could you share the direct link instead ?
<ZipCPU> The prefetch needs to *assert* that the number of outstanding transactions matches what the prefetch thinks it should be.
<promach__> is prefetch similar to speculative caching ?
<ZipCPU> In this case, the prefetch I posted about does nothing but read one instruction from the bus.
<ZipCPU> Once the CPU uses that instruction, it then reads the next.
<ZipCPU> The particular prefetch mentioned there is woefully slow.
* ZipCPU is still looking through wb-prefetch.html, and not finding what he was talking about.
<promach__> why slow ?
<ZipCPU> Two reasons: 1) it was the first one I built, and 2) it is the one with the lowest logic I've built
<ZipCPU> I have three other prefetch modules, all of which are significantly faster.
<promach__> hmm... I am not familiar with prefetching, have not done one before
<ZipCPU> Really? What did you find scary about it?
<promach__> because I do not understand how it works ;)
<ZipCPU> That's why I posted about it ... to explain how it works.
<promach__> cool, I need some time to read about it over the weekend
<promach__> it is really a long post
<promach__> For instance, if one iteration of the loop takes 7 cycles to execute, and the cache miss penalty is 49 cycles then we should have k=7 ???
<ZipCPU> promach__: How would you describe the taste of chocolate to someone who had never tasted it?
<promach__> I suppose you had done prefetching coding
<promach__> huh ?
<ZipCPU> I've never used the prefetch() operator discussed in the wikipedia article.
<ZipCPU> I had been discussing an _instruction_ prefetch. That looks like a reference to a _data_ cache read.
<ZipCPU> promach__: That wikipedia article is confusing you.
<ZipCPU> You'd do better to read the article I wrote.
<promach__> ok
<ZipCPU> At least ... it's more complete.
<promach__> ZipCPU: sure
<qu1j0t3> ZipCPU: "dirt with sugar"?
* qu1j0t3 runz
<ZipCPU> ;)
* qu1j0t3 is being silly. it's that kind of day
<ZipCPU> qu1j0t3: Yeah, I'm about done for the day too.
<sorear> for once, single-issue in-order is useful
<ZipCPU> Ready for something quieter and simpler ...
<ZipCPU> ... so I'm formally proving my MMU.
<qu1j0t3> :)
<qu1j0t3> shhhhh don't tell intel
<ZipCPU> Heheh ...
<ZipCPU> It's not as hard as it sounds.
<ZipCPU> I just added the "key" missing criteria to it as well, so ... I'm expecting it to pass formal induction in addition to the bounded model check.
<promach__> sorear: yeah
digshadow has quit [Ping timeout: 264 seconds]
digshadow has joined #yosys
promach__ is now known as promach_
AlexDaniel has quit [Ping timeout: 256 seconds]
dys has joined #yosys
eduardo_ has joined #yosys
eduardo__ has quit [Ping timeout: 240 seconds]
eduardo_ has quit [Ping timeout: 268 seconds]
eduardo_ has joined #yosys
m_t has joined #yosys
ar3itrary has quit [Remote host closed the connection]
LongHairedHacker has joined #yosys
LongHairedHacker is now known as ar3itrary
sklv has quit [Write error: Connection reset by peer]
sklv has joined #yosys
sklv has quit [Ping timeout: 272 seconds]
sklv has joined #yosys
promach__ has joined #yosys
promach__ has quit [Read error: Connection reset by peer]
promach__ has joined #yosys
promach__ has quit [Remote host closed the connection]
sklv has quit [Ping timeout: 272 seconds]
zino has quit [Quit: Leaving]
zino has joined #yosys
sklv has joined #yosys
jhol has quit [Quit: Coyote finally caught me]
jhol has joined #yosys
jhol has quit [Quit: Coyote finally caught me]
jhol has joined #yosys
AlexDaniel has joined #yosys
adj__3 has quit [Ping timeout: 260 seconds]
adj__ has joined #yosys
adj__ has quit [Ping timeout: 248 seconds]
digshadow has quit [Ping timeout: 248 seconds]
adj__ has joined #yosys
shapr has joined #yosys
digshadow has joined #yosys
pie_ has quit [Ping timeout: 256 seconds]
dys has quit [Ping timeout: 250 seconds]
peterbjornx has joined #yosys
dys has joined #yosys
gnufan has joined #yosys
dys has quit [Ping timeout: 248 seconds]
quigonjinn has joined #yosys
dys has joined #yosys
stefano_ has joined #yosys
stefano_ has left #yosys [#yosys]
gnufan has quit [Quit: Leaving.]