danieljabailey has quit [Quit: ZNC 1.6.5+deb2build2 - http://znc.in]
danieljabailey has joined #yosys
AlexDaniel has quit [Ping timeout: 260 seconds]
<awygle>
ZipCPU: just finished your recent blog post
<ZipCPU>
awygle: How'd I do?
<ZipCPU>
I was trying to capture the conversation(s) I've been having with promach, figuring they'd be relevant to a much broader audience than just he and I.
<awygle>
ZipCPU: i quite enjoyed it, and you showed me how to implement the idea that i'd had but hadn't had time to attempt
<ZipCPU>
Which one was that? Avoiding the f_past_valid?
<awygle>
the way in which you're using assume() to require that i_ce toggle X amount of times in Y clock cycles
<awygle>
when you say "The induction step works by picking random initial values for every registered signal within the design", is that literally true?
<ZipCPU>
Yeah, okay ... that works good for the cases I gave it, but I'm not so sure that would be how I'd do it for i_ce being true one of every 20.
<ZipCPU>
Well, sort of ... it's certainly how it appears.
<ZipCPU>
I think in actuality it tries *every* possible set of initial values, rather than just a random one.
<awygle>
i suspect "random" can't actually be the case or it would have to run 2^N trials, where N is the number of registers
<awygle>
err i suppose that wouldn't even be random
<ZipCPU>
The benefit of formal is that it exhausts the space, and ... that's not random but rather methodical.
<awygle>
right
<awygle>
so "2^n initial conditions, minus any it's smart enough to be able to discard"
<awygle>
my other comment is that you're teasing me at the end there! "these engines don't struggle with this problem" is quite the buried lede
<ZipCPU>
Well .... try them!
<awygle>
i will! ... when i can
<awygle>
i had actually played with abc pdr and seen that it was pickier about certain things than smtbmc, but didn't get beyond that
<ZipCPU>
If you use SymbiYosys, then it's *very* easy to switch from among several formal engines.
<ZipCPU>
I'm not sure I've gone much farther than this test/post.
<awygle>
my main concern is that all of clifford's slides discuss the k-induction proof method
<awygle>
but the other engines seem to imply that they're using a different approach entirely
<awygle>
certainly if they don't suffer from this "induction issue" (not really a fair description but you know) then they must be doing something fundamentally "other"
<ZipCPU>
At one time I could use the yosys "opt -share_all" and yosys wouldn't struggle with the issue.
<ZipCPU>
I haven't gone back to see why that didn't work last night as I was putting the post together.
<awygle>
i suspect opt -share_all was merging your identical shift registers
<ZipCPU>
Yeah, that's what I think it was doing.
<ZipCPU>
Why that feature would be removed, I'm not certain.
nonlinear has quit [Ping timeout: 256 seconds]
m_t has quit [Quit: Leaving]
promach has joined #yosys
promach has quit [Quit: WeeChat 2.1-dev]
promach has joined #yosys
seldridge has joined #yosys
nonlinear has joined #yosys
vinnyp has joined #yosys
<vinnyp>
Hi all. Can you define a max number of fanout in the tool?
cr1901_modern has quit [Ping timeout: 268 seconds]
cr1901_modern has joined #yosys
maartenBE has quit [Ping timeout: 240 seconds]
maartenBE has joined #yosys
seldridge has quit [Ping timeout: 248 seconds]
<vinnyp>
Hi all. If yosys can handle a max number of fanout, please let me know It would help me significantly :-)
leviathan has quit [Read error: Connection reset by peer]
leviathan has joined #yosys
emeb_mac has quit [Quit: emeb_mac]
dys has quit [Ping timeout: 240 seconds]
proteus-guy has quit [Ping timeout: 256 seconds]
AlexDaniel has joined #yosys
m_w has quit [Ping timeout: 264 seconds]
m_w has joined #yosys
proteus-guy has joined #yosys
GuzTech has joined #yosys
pie_ has joined #yosys
zkrx has quit [Quit: I'm done]
zkrx has joined #yosys
cemerick has joined #yosys
AlexDaniel has quit [Ping timeout: 265 seconds]
AlexDaniel has joined #yosys
fsasm has joined #yosys
pie_ has quit [Ping timeout: 264 seconds]
fsasm has quit [Quit: Leaving]
cemerick has quit [Ping timeout: 248 seconds]
proteus-guy has quit [Ping timeout: 252 seconds]
leviathan has quit [Remote host closed the connection]
proteus-guy has joined #yosys
seldridge has joined #yosys
promach has quit [Quit: WeeChat 2.1-dev]
pie_ has joined #yosys
m_t has joined #yosys
promach has joined #yosys
pie_ has quit [Ping timeout: 260 seconds]
seldridge has quit [Ping timeout: 240 seconds]
leviathan has joined #yosys
leviathan has quit [Remote host closed the connection]
leviathan has joined #yosys
pie_ has joined #yosys
pie_ has quit [Ping timeout: 264 seconds]
seldridge has joined #yosys
sklv has joined #yosys
AlexDaniel has quit [Ping timeout: 260 seconds]
cemerick has joined #yosys
pie_ has joined #yosys
sklv has quit [Remote host closed the connection]
sklv has joined #yosys
AlexDaniel has joined #yosys
leviathan has quit [Ping timeout: 240 seconds]
GuzTech has quit [Quit: Leaving]
leviathan has joined #yosys
m_w has quit [Ping timeout: 240 seconds]
eduardo_ has quit [Ping timeout: 276 seconds]
eduardo_ has joined #yosys
leviathan has quit [Ping timeout: 264 seconds]
sklv has quit [Read error: Connection reset by peer]
seldridge has quit [Ping timeout: 256 seconds]
sklv has joined #yosys
leviathan has joined #yosys
<awygle>
so it seems that PDR is a distinct algorithm, while AIGER is just a file format
<awygle>
avy implements both PDR and "interpolation" (not sure if this is another distinct algorithm, sounds like it)
<awygle>
suprove is super_prove, which seems to be another implementation of one or more algorithms but is tremendously hard to google
sunxi_fan has quit [Ping timeout: 240 seconds]
m_t has quit [Quit: Leaving]
seldridge has joined #yosys
sklv has quit [Remote host closed the connection]
sklv has joined #yosys
m_w has joined #yosys
digshadow has quit [Ping timeout: 268 seconds]
seldridge has quit [Ping timeout: 264 seconds]
digshadow has joined #yosys
_whitelogger has joined #yosys
<ZipCPU>
Yosys is only a synthesis engine. It doesn't handle place and route. Isn't fanout a place and route issue?
<ravenexp>
xilinx handles it inside XST - its synthesys engine
<ravenexp>
dunno about vivado
<ravenexp>
though xilinx place and route tool doesn't actually place
<ravenexp>
it's probably not the best example to model things on
<sorear>
timing-aware synthesis is a thing
<awygle>
fanout is a net list issue, so a synthesis issue. Turning it into something useful like a delay is a P&R issue
m_t has joined #yosys
<sorear>
some tools don't have a strict phase separation between synthesis and p&r
<awygle>
vinnyp: yes, it's possible. You may have to write a custom pass. You might be able to do it with the built-in commands but if so I don't know how. Check the command documentation at the following link
<tpb>
Title: Yosys Open SYnthesis Suite :: Documentation (at www.clifford.at)
<awygle>
sorear: fair enough
<awygle>
but Yosys does, with the minor exception of abc retiming, unless I'm mistaken
<vinnyp>
I know that some tools like XST enable fanout constraints
<vinnyp>
I looked at the documentation, but I was unable to find a suitable command
<vinnyp>
or even a combination of command to enable it.
<vinnyp>
I looked into abc, but the documentation doesn't hint at anything.
<vinnyp>
awygle: Thanks!
<vinnyp>
Unless abc can do it, I may have to write a pass.
<awygle>
vinnyp: I think if I understand the requirement it should be a pretty simple pass, you can just duplicate any cell with fanout >cutoff
<awygle>
and divide the fanout between the two
<vinnyp>
yup. I am writing a pass now. (external to yosys for the moment).
<sorear>
it's trickier if you want to do this based on timing feedback from p&r, I understand it's been done but haven't been able to guess an algorithm
<vinnyp>
I would need to build a model for it. That is not my concern at the moment. I just need to restrict the fanout.
dys has joined #yosys
dys has quit [Ping timeout: 256 seconds]
<ZipCPU>
vinnyp: Just checked with clifford. He thinks ABC might have a feature for it, but there's nothing in yosys that would handle fanout.
<vinnyp>
Thanks ZipCPU! I looked at the abc doc, but have not found anything.