Monday, 2018-03-12

*** tpb has joined #yosys00:00
*** danieljabailey has quit IRC00:03
*** danieljabailey has joined #yosys00:03
*** AlexDaniel has quit IRC00:11
awygleZipCPU: just finished your recent blog post00:21
ZipCPUawygle: How'd I do?00:31
ZipCPUI 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.00:31
awygleZipCPU: i quite enjoyed it, and you showed me how to implement the idea that i'd had but hadn't had time to attempt00:32
ZipCPUWhich one was that?  Avoiding the f_past_valid?00:32
awyglethe way in which you're using assume() to require that i_ce toggle X amount of times in Y clock cycles00:33
awyglewhen you say "The induction step works by picking random initial values for every registered signal within the design", is that literally true?00:34
ZipCPUYeah, 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.00:34
ZipCPUWell, sort of ... it's certainly how it appears.00:35
ZipCPUI think in actuality it tries *every* possible set of initial values, rather than just a random one.00:35
awyglei suspect "random" can't actually be the case or it would have to run 2^N trials, where N is the number of registers00:35
awygleerr i suppose that wouldn't even be random00:35
ZipCPUThe benefit of formal is that it exhausts the space, and ... that's not random but rather methodical.00:36
awygleso "2^n initial conditions, minus any it's smart enough to be able to discard"00:36
awyglemy other comment is that you're teasing me at the end there! "these engines don't struggle with this problem" is quite the buried lede00:37
ZipCPUWell .... try them!00:37
awyglei will! ... when i can00:38
awyglei had actually played with abc pdr and seen that it was pickier about certain things than smtbmc, but didn't get beyond that00:38
ZipCPUIf you use SymbiYosys, then it's *very* easy to switch from among several formal engines.00:38
ZipCPUI'm not sure I've gone much farther than this test/post.00:38
awyglemy main concern is that all of clifford's slides discuss the k-induction proof method00:40
awyglebut the other engines seem to imply that they're using a different approach entirely00:40
awyglecertainly 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"00:40
ZipCPUAt one time I could use the yosys "opt -share_all" and yosys wouldn't struggle with the issue.00:41
ZipCPUI haven't gone back to see why that didn't work last night as I was putting the post together.00:42
awyglei suspect opt -share_all was merging your identical shift registers00:44
ZipCPUYeah, that's what I think it was doing.00:45
ZipCPUWhy that feature would be removed, I'm not certain.00:45
*** nonlinear has quit IRC00:55
*** m_t has quit IRC01:32
*** promach has joined #yosys01:57
*** promach has quit IRC02:34
*** promach has joined #yosys02:35
*** seldridge has joined #yosys02:59
*** nonlinear has joined #yosys03:40
*** vinnyp has joined #yosys03:42
vinnypHi all. Can you define a max number of fanout in the tool?03:42
*** cr1901_modern has quit IRC03:47
*** cr1901_modern has joined #yosys03:55
*** maartenBE has quit IRC04:22
*** maartenBE has joined #yosys04:23
*** seldridge has quit IRC04:27
vinnypHi all. If yosys can handle a max number of fanout, please let me know It would help me significantly :-)04:50
*** emeb_mac has joined #yosys05:02
*** promach has quit IRC05:05
*** promach has joined #yosys05:07
*** m_w has joined #yosys06:04
*** kc8apf_ has joined #yosys06:30
*** Max`P has joined #yosys06:37
*** kc8apf has quit IRC06:38
*** Kooda has quit IRC06:38
*** bluesceada has quit IRC06:38
*** Max-P has quit IRC06:38
*** kc8apf_ is now known as kc8apf06:38
*** Max`P is now known as Max-P06:38
*** bluesceada has joined #yosys06:38
*** sklv has quit IRC06:38
*** pie___ has joined #yosys06:39
*** pie__ has quit IRC06:41
*** pie___ has quit IRC06:44
*** Kooda has joined #yosys06:45
awygleZipCPU: this seems to be the Source for "abc pdr"
*** pie___ has joined #yosys07:00
*** dys has joined #yosys07:02
*** pie___ has quit IRC07:05
*** vinnyp has quit IRC07:06
*** dmin7 has joined #yosys07:21
*** dmin7 has left #yosys07:22
*** leviathan has joined #yosys07:25
*** leviathan has quit IRC07:27
*** leviathan has joined #yosys07:28
*** emeb_mac has quit IRC07:28
*** dys has quit IRC07:35
*** proteus-guy has quit IRC07:35
*** AlexDaniel has joined #yosys08:16
*** m_w has quit IRC08:29
*** m_w has joined #yosys08:29
*** proteus-guy has joined #yosys08:50
*** GuzTech has joined #yosys08:55
*** pie_ has joined #yosys08:59
*** zkrx has quit IRC09:03
*** zkrx has joined #yosys09:04
*** cemerick has joined #yosys09:11
*** AlexDaniel has quit IRC10:03
*** AlexDaniel has joined #yosys10:04
*** fsasm has joined #yosys10:45
*** pie_ has quit IRC10:56
*** fsasm has quit IRC10:59
*** cemerick has quit IRC11:24
*** proteus-guy has quit IRC11:32
*** leviathan has quit IRC11:36
*** proteus-guy has joined #yosys11:45
*** seldridge has joined #yosys12:16
*** promach has quit IRC12:40
*** pie_ has joined #yosys12:51
*** m_t has joined #yosys12:53
*** promach has joined #yosys12:55
*** pie_ has quit IRC12:56
*** seldridge has quit IRC13:52
*** leviathan has joined #yosys13:53
*** leviathan has quit IRC13:58
*** leviathan has joined #yosys13:59
*** pie_ has joined #yosys14:00
*** pie_ has quit IRC14:20
*** seldridge has joined #yosys14:21
*** sklv has joined #yosys14:22
*** AlexDaniel has quit IRC14:34
*** cemerick has joined #yosys14:47
*** pie_ has joined #yosys14:58
*** sklv has quit IRC15:26
*** sklv has joined #yosys15:26
*** AlexDaniel has joined #yosys15:57
*** leviathan has quit IRC16:21
*** GuzTech has quit IRC16:22
*** leviathan has joined #yosys16:24
*** m_w has quit IRC16:25
*** eduardo_ has quit IRC16:26
*** eduardo_ has joined #yosys16:26
*** leviathan has quit IRC17:00
*** sklv has quit IRC17:02
*** seldridge has quit IRC17:03
*** sklv has joined #yosys17:03
*** leviathan has joined #yosys17:04
awygleso it seems that PDR is a distinct algorithm, while AIGER is just a file format17:11
awygleavy implements both PDR and "interpolation" (not sure if this is another distinct algorithm, sounds like it)17:13
awyglesuprove is super_prove, which seems to be another implementation of one or more algorithms but is tremendously hard to google17:13
*** sunxi_fan has quit IRC17:14
*** m_t has quit IRC17:23
*** seldridge has joined #yosys17:23
*** sklv has quit IRC17:57
*** sklv has joined #yosys17:57
*** m_w has joined #yosys18:03
*** digshadow has quit IRC18:05
*** seldridge has quit IRC18:07
*** digshadow has joined #yosys18:28
*** vinnyp has joined #yosys18:34
*** _whitelogger has quit IRC18:36
vinnypHi all. I still am trying to constrain the fanout for a gate using Yosys. Please let me know if it is possible. Thanks :-)18:36
*** _whitelogger has joined #yosys18:38
ZipCPUYosys is only a synthesis engine.  It doesn't handle place and route.  Isn't fanout a place and route issue?18:38
ravenexpxilinx handles it inside XST - its synthesys engine18:50
ravenexpdunno about vivado18:50
ravenexpthough xilinx place and route tool doesn't actually place18:52
ravenexpit's probably not the best example to model things on18:52
soreartiming-aware synthesis is a thing18:54
awyglefanout is a net list issue, so a synthesis issue. Turning it into something useful like a delay is a P&R issue18:58
*** m_t has joined #yosys18:59
sorearsome tools don't have a strict phase separation between synthesis and p&r18:59
awyglevinnyp: 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 link19:00
tpbTitle: Yosys Open SYnthesis Suite :: Documentation (at
awyglesorear: fair enough19:00
awyglebut Yosys does, with the minor exception of abc retiming, unless I'm mistaken19:01
vinnypI know that some tools like XST enable fanout constraints19:01
vinnypI looked at the documentation, but I was unable to find a suitable command19:02
vinnypor even a combination of command to enable it.19:02
vinnypI looked into abc, but the documentation doesn't hint at anything.19:03
vinnypawygle: Thanks!19:03
vinnypUnless abc can do it, I may have to write a pass.19:03
awyglevinnyp: I think if I understand the requirement it should be a pretty simple pass, you can just duplicate any cell with fanout >cutoff19:04
awygleand divide the fanout between the two19:04
vinnypyup. I am writing a pass now. (external to yosys for the moment).19:06
sorearit'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 algorithm19:11
vinnypI would need to build a model for it. That is not my concern at the moment. I just need to restrict the fanout.19:17
*** dys has joined #yosys19:33
*** dys has quit IRC19:58
ZipCPUvinnyp: Just checked with clifford.  He thinks ABC might have a feature for it, but there's nothing in yosys that would handle fanout.20:16
vinnypThanks ZipCPU! I looked at the abc  doc, but have not found anything.20:19
*** jwhitmore has joined #yosys20:25
*** _whitelogger has quit IRC21:24
*** _whitelogger has joined #yosys21:26
*** jwhitmore has quit IRC21:31
*** cemerick has quit IRC22:07
*** indy has quit IRC22:17
*** indy has joined #yosys22:19
*** leviathan has quit IRC22:19

Generated by 2.13.1 by Marius Gedminas - find it at!