| *** tpb has joined #yosys | 00:00 | |
| *** danieljabailey has quit IRC | 00:03 | |
| *** danieljabailey has joined #yosys | 00:03 | |
| *** AlexDaniel has quit IRC | 00:11 | |
| awygle | ZipCPU: just finished your recent blog post | 00:21 |
|---|---|---|
| ZipCPU | awygle: How'd I do? | 00:31 |
| 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. | 00:31 |
| 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 | 00:32 |
| ZipCPU | Which one was that? Avoiding the f_past_valid? | 00:32 |
| awygle | the way in which you're using assume() to require that i_ce toggle X amount of times in Y clock cycles | 00:33 |
| awygle | when you say "The induction step works by picking random initial values for every registered signal within the design", is that literally true? | 00:34 |
| 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. | 00:34 |
| ZipCPU | Well, sort of ... it's certainly how it appears. | 00:35 |
| ZipCPU | I think in actuality it tries *every* possible set of initial values, rather than just a random one. | 00:35 |
| 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 | 00:35 |
| awygle | err i suppose that wouldn't even be random | 00:35 |
| ZipCPU | The benefit of formal is that it exhausts the space, and ... that's not random but rather methodical. | 00:36 |
| awygle | right | 00:36 |
| awygle | so "2^n initial conditions, minus any it's smart enough to be able to discard" | 00:36 |
| 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 | 00:37 |
| ZipCPU | Well .... try them! | 00:37 |
| awygle | i will! ... when i can | 00:38 |
| 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 | 00:38 |
| ZipCPU | If you use SymbiYosys, then it's *very* easy to switch from among several formal engines. | 00:38 |
| ZipCPU | I'm not sure I've gone much farther than this test/post. | 00:38 |
| awygle | my main concern is that all of clifford's slides discuss the k-induction proof method | 00:40 |
| awygle | but the other engines seem to imply that they're using a different approach entirely | 00:40 |
| 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" | 00:40 |
| ZipCPU | At one time I could use the yosys "opt -share_all" and yosys wouldn't struggle with the issue. | 00:41 |
| ZipCPU | I haven't gone back to see why that didn't work last night as I was putting the post together. | 00:42 |
| awygle | i suspect opt -share_all was merging your identical shift registers | 00:44 |
| ZipCPU | Yeah, that's what I think it was doing. | 00:45 |
| ZipCPU | Why that feature would be removed, I'm not certain. | 00:45 |
| *** nonlinear has quit IRC | 00:55 | |
| *** m_t has quit IRC | 01:32 | |
| *** promach has joined #yosys | 01:57 | |
| *** promach has quit IRC | 02:34 | |
| *** promach has joined #yosys | 02:35 | |
| *** seldridge has joined #yosys | 02:59 | |
| *** nonlinear has joined #yosys | 03:40 | |
| *** vinnyp has joined #yosys | 03:42 | |
| vinnyp | Hi all. Can you define a max number of fanout in the tool? | 03:42 |
| *** cr1901_modern has quit IRC | 03:47 | |
| *** cr1901_modern has joined #yosys | 03:55 | |
| *** maartenBE has quit IRC | 04:22 | |
| *** maartenBE has joined #yosys | 04:23 | |
| *** seldridge has quit IRC | 04:27 | |
| vinnyp | Hi 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 #yosys | 05:02 | |
| *** promach has quit IRC | 05:05 | |
| *** promach has joined #yosys | 05:07 | |
| *** m_w has joined #yosys | 06:04 | |
| *** kc8apf_ has joined #yosys | 06:30 | |
| *** Max`P has joined #yosys | 06:37 | |
| *** kc8apf has quit IRC | 06:38 | |
| *** Kooda has quit IRC | 06:38 | |
| *** bluesceada has quit IRC | 06:38 | |
| *** Max-P has quit IRC | 06:38 | |
| *** kc8apf_ is now known as kc8apf | 06:38 | |
| *** Max`P is now known as Max-P | 06:38 | |
| *** bluesceada has joined #yosys | 06:38 | |
| *** sklv has quit IRC | 06:38 | |
| *** pie___ has joined #yosys | 06:39 | |
| *** pie__ has quit IRC | 06:41 | |
| *** pie___ has quit IRC | 06:44 | |
| *** Kooda has joined #yosys | 06:45 | |
| awygle | ZipCPU: this seems to be the Source for "abc pdr" https://www2.eecs.berkeley.edu/Pubs/TechRpts/2013/EECS-2013-225.pdf | 06:49 |
| *** pie___ has joined #yosys | 07:00 | |
| *** dys has joined #yosys | 07:02 | |
| *** pie___ has quit IRC | 07:05 | |
| *** vinnyp has quit IRC | 07:06 | |
| *** dmin7 has joined #yosys | 07:21 | |
| *** dmin7 has left #yosys | 07:22 | |
| *** leviathan has joined #yosys | 07:25 | |
| *** leviathan has quit IRC | 07:27 | |
| *** leviathan has joined #yosys | 07:28 | |
| *** emeb_mac has quit IRC | 07:28 | |
| *** dys has quit IRC | 07:35 | |
| *** proteus-guy has quit IRC | 07:35 | |
| *** AlexDaniel has joined #yosys | 08:16 | |
| *** m_w has quit IRC | 08:29 | |
| *** m_w has joined #yosys | 08:29 | |
| *** proteus-guy has joined #yosys | 08:50 | |
| *** GuzTech has joined #yosys | 08:55 | |
| *** pie_ has joined #yosys | 08:59 | |
| *** zkrx has quit IRC | 09:03 | |
| *** zkrx has joined #yosys | 09:04 | |
| *** cemerick has joined #yosys | 09:11 | |
| *** AlexDaniel has quit IRC | 10:03 | |
| *** AlexDaniel has joined #yosys | 10:04 | |
| *** fsasm has joined #yosys | 10:45 | |
| *** pie_ has quit IRC | 10:56 | |
| *** fsasm has quit IRC | 10:59 | |
| *** cemerick has quit IRC | 11:24 | |
| *** proteus-guy has quit IRC | 11:32 | |
| *** leviathan has quit IRC | 11:36 | |
| *** proteus-guy has joined #yosys | 11:45 | |
| *** seldridge has joined #yosys | 12:16 | |
| *** promach has quit IRC | 12:40 | |
| *** pie_ has joined #yosys | 12:51 | |
| *** m_t has joined #yosys | 12:53 | |
| *** promach has joined #yosys | 12:55 | |
| *** pie_ has quit IRC | 12:56 | |
| *** seldridge has quit IRC | 13:52 | |
| *** leviathan has joined #yosys | 13:53 | |
| *** leviathan has quit IRC | 13:58 | |
| *** leviathan has joined #yosys | 13:59 | |
| *** pie_ has joined #yosys | 14:00 | |
| *** pie_ has quit IRC | 14:20 | |
| *** seldridge has joined #yosys | 14:21 | |
| *** sklv has joined #yosys | 14:22 | |
| *** AlexDaniel has quit IRC | 14:34 | |
| *** cemerick has joined #yosys | 14:47 | |
| *** pie_ has joined #yosys | 14:58 | |
| *** sklv has quit IRC | 15:26 | |
| *** sklv has joined #yosys | 15:26 | |
| *** AlexDaniel has joined #yosys | 15:57 | |
| *** leviathan has quit IRC | 16:21 | |
| *** GuzTech has quit IRC | 16:22 | |
| *** leviathan has joined #yosys | 16:24 | |
| *** m_w has quit IRC | 16:25 | |
| *** eduardo_ has quit IRC | 16:26 | |
| *** eduardo_ has joined #yosys | 16:26 | |
| *** leviathan has quit IRC | 17:00 | |
| *** sklv has quit IRC | 17:02 | |
| *** seldridge has quit IRC | 17:03 | |
| *** sklv has joined #yosys | 17:03 | |
| *** leviathan has joined #yosys | 17:04 | |
| awygle | so it seems that PDR is a distinct algorithm, while AIGER is just a file format | 17:11 |
| awygle | avy implements both PDR and "interpolation" (not sure if this is another distinct algorithm, sounds like it) | 17:13 |
| awygle | suprove is super_prove, which seems to be another implementation of one or more algorithms but is tremendously hard to google | 17:13 |
| *** sunxi_fan has quit IRC | 17:14 | |
| *** m_t has quit IRC | 17:23 | |
| *** seldridge has joined #yosys | 17:23 | |
| *** sklv has quit IRC | 17:57 | |
| *** sklv has joined #yosys | 17:57 | |
| *** m_w has joined #yosys | 18:03 | |
| *** digshadow has quit IRC | 18:05 | |
| *** seldridge has quit IRC | 18:07 | |
| *** digshadow has joined #yosys | 18:28 | |
| *** vinnyp has joined #yosys | 18:34 | |
| *** _whitelogger has quit IRC | 18:36 | |
| vinnyp | Hi 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 #yosys | 18:38 | |
| ZipCPU | Yosys is only a synthesis engine. It doesn't handle place and route. Isn't fanout a place and route issue? | 18:38 |
| ravenexp | xilinx handles it inside XST - its synthesys engine | 18:50 |
| ravenexp | dunno about vivado | 18:50 |
| ravenexp | though xilinx place and route tool doesn't actually place | 18:52 |
| ravenexp | it's probably not the best example to model things on | 18:52 |
| sorear | timing-aware synthesis is a thing | 18:54 |
| awygle | fanout is a net list issue, so a synthesis issue. Turning it into something useful like a delay is a P&R issue | 18:58 |
| *** m_t has joined #yosys | 18:59 | |
| sorear | some tools don't have a strict phase separation between synthesis and p&r | 18:59 |
| 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 | 19:00 |
| awygle | http://www.clifford.at/yosys/documentation.html | 19:00 |
| tpb | Title: Yosys Open SYnthesis Suite :: Documentation (at www.clifford.at) | 19:00 |
| awygle | sorear: fair enough | 19:00 |
| awygle | but Yosys does, with the minor exception of abc retiming, unless I'm mistaken | 19:01 |
| vinnyp | I know that some tools like XST enable fanout constraints | 19:01 |
| vinnyp | I looked at the documentation, but I was unable to find a suitable command | 19:02 |
| vinnyp | or even a combination of command to enable it. | 19:02 |
| vinnyp | I looked into abc, but the documentation doesn't hint at anything. | 19:03 |
| vinnyp | awygle: Thanks! | 19:03 |
| vinnyp | Unless abc can do it, I may have to write a pass. | 19:03 |
| 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 | 19:04 |
| awygle | and divide the fanout between the two | 19:04 |
| vinnyp | yup. I am writing a pass now. (external to yosys for the moment). | 19:06 |
| 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 | 19:11 |
| 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. | 19:17 |
| *** dys has joined #yosys | 19:33 | |
| *** dys has quit IRC | 19:58 | |
| 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. | 20:16 |
| vinnyp | Thanks ZipCPU! I looked at the abc doc, but have not found anything. | 20:19 |
| *** jwhitmore has joined #yosys | 20:25 | |
| *** _whitelogger has quit IRC | 21:24 | |
| *** _whitelogger has joined #yosys | 21:26 | |
| *** jwhitmore has quit IRC | 21:31 | |
| *** cemerick has quit IRC | 22:07 | |
| *** indy has quit IRC | 22:17 | |
| *** indy has joined #yosys | 22:19 | |
| *** leviathan has quit IRC | 22:19 | |
Generated by irclog2html.py 2.13.1 by Marius Gedminas - find it at mg.pov.lt!