| *** tpb has joined #yosys | 00:00 | |
| *** rjo has quit IRC | 00:28 | |
| *** rjo has joined #yosys | 00:36 | |
| *** simeonm has quit IRC | 00:56 | |
| *** futarisIRCcloud has quit IRC | 01:31 | |
| *** N2TOH has joined #yosys | 01:35 | |
| *** lambda has quit IRC | 01:46 | |
| *** lambda has joined #yosys | 02:04 | |
| *** simeonm has joined #yosys | 02:05 | |
| *** citypw has joined #yosys | 02:18 | |
| *** lambda has quit IRC | 02:21 | |
| *** Degi has quit IRC | 02:59 | |
| *** Degi has joined #yosys | 03:00 | |
| *** lambda has joined #yosys | 03:03 | |
| *** Cerpin has quit IRC | 03:14 | |
| *** Cerpin has joined #yosys | 03:16 | |
| *** BinaryLust has quit IRC | 05:07 | |
| *** BinaryLust has joined #yosys | 06:18 | |
| *** emeb_mac has quit IRC | 06:31 | |
| *** futarisIRCcloud has joined #yosys | 07:06 | |
| *** dys has joined #yosys | 07:15 | |
| *** jakobwenzel has joined #yosys | 07:29 | |
| *** Asu has joined #yosys | 08:46 | |
| *** BinaryLust has quit IRC | 09:59 | |
| *** rswarbrick has joined #yosys | 10:08 | |
| *** jfcaron has joined #yosys | 10:30 | |
| rswarbrick | I'm still hacking away at adding bind support, and have got to the stage where I'm trying to insert cells in the hierarchy pass. Is the hierarchy command supposed to be idempotent? | 10:37 |
|---|---|---|
| rswarbrick | If so, I need to track "I inserted a top-level bind here" | 10:38 |
| ZirconiumX | Yes, hierarchy should do nothing if there's nothing to do | 10:39 |
| *** vidbina has joined #yosys | 10:39 | |
| rswarbrick | The point is that I might have a top-level bind statement that applies to all modules of type FOO. If I run hierarchy, then load foo.sv, then run hierarchy again, I'd like to get the cell bound in properly. But if I load foo.sv then run hierarchy twice, do I need to make sure I don't get 2 cells? (I think yes, but wanted to check) | 10:40 |
| daveshah | Yes, ideally the bind would be removed by hierarchy | 10:42 |
| daveshah | But that depends on how the bind is represented | 10:43 |
| rswarbrick | Well, it's a new module-like thing. A module can contain one, and so can the design (to allow bind directives at top-level). | 10:43 |
| rswarbrick | (module-like for technical reasons to do with where we instantiate cells in genrtlil) | 10:44 |
| rswarbrick | Do we support things like "load x.sv; hierarchy; load a.sv; hierarchy" ? If so, I think I have to ensure idempotence by setting a flag where the bind occurs, rather than on the bind object itself, no? | 10:45 |
| rswarbrick | (because a top-level bind might have an effect on modules in x.sv and also on modules in a.sv) | 10:46 |
| daveshah | Oh, I don't really know the bind semantics well enough here | 10:50 |
| rswarbrick | Well, one thing you can do is "bind foo bar bar_i(.*)", which means "put a bar called bar_i into every module of type foo". I guess we could delete a bind directive like this after applying it (since we now have the definition of foo), but I'm not sure that's right if you can do stuff like deleting modules and reloading them. | 10:52 |
| daveshah | Yeah, it might get complicated if you derive a new parameterisation of foo, too | 10:53 |
| daveshah | then I think the attribute approach is indeed best | 10:53 |
| rswarbrick | Cool, makes sense. | 10:53 |
| rswarbrick | Because "naming things is hard", do we have a name for a non-abstract module? That is, one that's either derived already or one that had no parameters? "concrete"? | 11:02 |
| whitequark | concrete seems reasonable | 11:10 |
| rswarbrick | Thanks! | 11:10 |
| rswarbrick | Also, is there a neat way to find all modules with a given original name? Looking at derive_common in ast.cc, it looks like a module called FOO might come out as $paramodFOOx=1 or $paramod$1234abcdFOO. Searching the strings seems a bit icky. Is there a better way? | 11:10 |
| rswarbrick | (I'm asking because I can't guarantee that I see a bind directive before I specialise the module) | 11:10 |
| rswarbrick | Ohh. I've just seen the hdlname attribute. I guess I can work from there. | 11:12 |
| Sarayan | isn't it hdlname that's going to slightly change for the better? | 11:13 |
| whitequark | hm? | 11:17 |
| whitequark | hdlname on modules won't change | 11:17 |
| Sarayan | dots to spaces | 11:17 |
| whitequark | nope, currently there is no hdlname with dots | 11:17 |
| whitequark | it's just the wire name | 11:17 |
| Sarayan | ok cool then :-) | 11:17 |
| *** vidbina has quit IRC | 11:43 | |
| *** vidbina has joined #yosys | 12:08 | |
| *** vidbina has quit IRC | 14:12 | |
| *** X-Scale` has joined #yosys | 14:53 | |
| *** X-Scale has quit IRC | 14:54 | |
| *** X-Scale` is now known as X-Scale | 14:54 | |
| *** X-Scale has quit IRC | 14:56 | |
| *** dys has quit IRC | 15:02 | |
| *** emeb has joined #yosys | 15:35 | |
| *** Cerpin has quit IRC | 15:35 | |
| ZirconiumX | daveshah, mwk: https://github.com/YosysHQ/yosys/pull/2096 <-- thoughts? | 15:57 |
| tpb | Title: [RFC] Add conditional-insert operator to pool/dict by ZirconiumX · Pull Request #2096 · YosysHQ/yosys · GitHub (at github.com) | 15:57 |
| *** jfcaron has quit IRC | 16:03 | |
| mwk | I'm not convinced it improves readability | 16:08 |
| whitequark | neither am I | 16:13 |
| whitequark | I'm not strongly opposed but I don't see the benefit | 16:13 |
| ZirconiumX | Mmm | 16:23 |
| rswarbrick | ZirconiumX: Could you use something like std::copy_if for this? | 16:34 |
| ZirconiumX | I don't think so | 16:37 |
| ZirconiumX | You'd have to make two passes over the data | 16:37 |
| rswarbrick | You'd need something like std::back_inserter too. | 16:37 |
| rswarbrick | So std::copy_if(pool.begin(), pool.end(), dest_pool.inserter(), my_predicate); | 16:38 |
| ZirconiumX | I feel like ranges are really important for readability | 16:39 |
| ZirconiumX | pool.begin()/pool.end() is a bit messy | 16:40 |
| rswarbrick | In which case, I don't understand your PR: isn't it basically the same syntax? | 16:40 |
| ZirconiumX | I feel like range-style insert_if *is* an improvement though | 16:40 |
| *** citypw has quit IRC | 17:17 | |
| *** vidbina has joined #yosys | 17:37 | |
| *** Cerpin has joined #yosys | 18:08 | |
| *** jakobwenzel has quit IRC | 18:10 | |
| *** rlee287 has joined #yosys | 18:47 | |
| *** jakobwenzel has joined #yosys | 19:41 | |
| *** BinaryLust has joined #yosys | 19:49 | |
| *** dys has joined #yosys | 19:51 | |
| *** vidbina has quit IRC | 20:03 | |
| *** jfcaron_ has joined #yosys | 20:17 | |
| *** emeb_mac has joined #yosys | 20:30 | |
| *** jakobwenzel has quit IRC | 20:33 | |
| rlee287 | In the Verilog backend, the code generation for the $_DFF_ cells determines a boolean "out_is_reg_wire" that seems to check if reg_name already exists and declares a new reg if it does not | 20:37 |
| rlee287 | Is this understanding correct? | 20:37 |
| *** rswarbrick has quit IRC | 20:57 | |
| *** rlee287 has quit IRC | 21:14 | |
| *** jfcaron_ has quit IRC | 21:43 | |
| *** Asu has quit IRC | 21:49 | |
| *** captain_morgan has quit IRC | 21:56 | |
| *** captain_morgan has joined #yosys | 21:57 | |
| *** emeb has quit IRC | 22:59 | |
| *** alcorn has joined #yosys | 23:19 | |
| alcorn | I'm seeing something weird with a Symbiyosys spec. I have a property that I can `cover` but can't `assume` https://pastebin.com/kX36Nbvi .Can someone help me understand if I'm missing some crucial concept? Or perhaps this is a bug? | 23:27 |
| tpb | Title: [SystemVerilog] Cover passes but assume fails - Pastebin.com (at pastebin.com) | 23:27 |
| ZirconiumX | ZipCPU: ^ | 23:34 |
| ZipCPU | alcorn: You can't assume it because it's false on the first clock tick | 23:35 |
| ZipCPU | ZirconiumX: Thanks for the flag | 23:35 |
| ZirconiumX | np | 23:35 |
| ZipCPU | Assuming something for which there's no way to make it true leads to what's known as a "WARMUP FAILURE" | 23:35 |
| ZipCPU | This is one of the reasons why I have a rule regarding assumptions: Only assume design *inputs*. Everything else, internal state and design outputs, should be constrained via assertions and your design logic. | 23:36 |
| ZipCPU | Cover succeeds because there's a way to make the statement true ... eventually, even though it's not true on the first clock tick | 23:38 |
| alcorn | ok thanks, I haven't quite yet wrapped my head around what assume/assert really do. What's the best way to tell the solver "I only care about situations where f_past_valid is true"? If I just assert(f_past_valid), can't the solver just issue a reset to find a counter example? | 23:38 |
| ZipCPU | I'm not normally asserting f_past_valid. That's constrained enough by logic, and I can verify it by cover(f_past_valid) if I want. | 23:39 |
| ZipCPU | assume limits the size of the search space the solver works with. | 23:39 |
| ZipCPU | See ... https://zipcpu.com/quiz/2019/08/03/quiz01.html for more information | 23:40 |
| tpb | Title: Quiz #1: Will the assertion below ever fail? (at zipcpu.com) | 23:40 |
| ZipCPU | In that design, you have a counter that is assumed to be less than 90, and an assertion that it will remain less than 100 | 23:40 |
| ZipCPU | The logic of the counter, however, will have it just counting up to 65535 and then rolling over | 23:40 |
| ZipCPU | So, will it ever reach 100? The answer is, No, because the assumption tells the solver not to ever consider cases where the assumption might be false. | 23:41 |
| * ZipCPU needs to run for supper | 23:41 | |
| ZipCPU | Consider checking out my first experiences here: https://zipcpu.com/blog/2017/10/19/formal-intro.html The descriptions of what assumptions and assertions are should be about right. | 23:42 |
| tpb | Title: My first experience with Formal Methods (at zipcpu.com) | 23:42 |
| alcorn | thanks for the tips! I think I now understand that you can only assume things that can be true on the first cycle. I had thought that it was possible to assume anything as long as it's reachable at some point... and that the solver would just figure out how to set up a sequence of input cycles that validate the assumption | 23:42 |
| ZipCPU | alcorn, that's not quite true. You can do an: always @(*) if (f_past_valid) assume(something_true_only_after_the_first_clock); | 23:43 |
| alcorn | I have actually read a few of your blog posts before and they have been very illuminating, so thank you! | 23:43 |
| ZipCPU | Np | 23:44 |
| alcorn | ok so you just have to guard your assumes with some other logic | 23:44 |
| alcorn | a naked assume has to be satisfiable on the first cycle | 23:44 |
| alcorn | ? | 23:44 |
| ZipCPU | You may. It depends on what you want to do. | 23:44 |
| ZipCPU | A naked assume needs to be satisfied on *EVERY* cycle | 23:44 |
| alcorn | Ok I see | 23:45 |
| ZipCPU | always @(*) assume(!S_AXI_ARVALID); // will keep a slave component from ever receiving an AXI read request | 23:45 |
| alcorn | This has helped. The solver is a bit less magical than I thought but perhaps less magic is good when you're trying to prove things correct | 23:46 |
| ZipCPU | Absolutely! | 23:46 |
| ZipCPU | The solver has to be ... very exacting. It must follow very strict rules, set forth by you. That's sort of the point. | 23:47 |
| alcorn | Right | 23:47 |
| ZipCPU | It's quite the stickler for details. | 23:47 |
| alcorn | Really I was just confusing the semantics of cover and assume | 23:47 |
| ZipCPU | cover(X) -> find one way, any way, to make X true | 23:47 |
| ZipCPU | assume(X) -> don't consider any circumstances where !X | 23:48 |
| ZipCPU | assert(X) -> a challenge to the solver. I don't think X will ever happen. Go ahead, prove me wrong, I dare you. | 23:48 |
| alcorn | How would you go about assuming that f_past_valid has been true for several cycles? | 23:49 |
| alcorn | I've been using this construction `assume(f_past_valid && $past(f_past_valid, 1) && $past(f_past_valid, 2) && ...)` | 23:49 |
| ZipCPU | initial f_past_valid_counter = 0; always @(*) if (f_past_valid && f_past_valid_counter < 200) f_past_valid_counter <= f_past_valid_counter + 1; | 23:50 |
| alcorn | but this discussion has me questioning if it is right | 23:50 |
| ZipCPU | if (f_past_valid_counter > 10) assume(XYZ); | 23:50 |
| ZipCPU | No, that's not how you'd do it. Use f_past_valid in a condition, sort of like: | 23:50 |
| ZipCPU | if (f_past_valid && $past(f_past_valid) && $past(f_past_valid, 2)) assert(XYZ); | 23:51 |
| ZipCPU | Remember: Don't *assume* anything but inputs. | 23:51 |
| alcorn | Ok this is sinking in | 23:51 |
| ZipCPU | You shouldn't be making assumptions about f_past_valid at all | 23:51 |
| alcorn | Righto | 23:51 |
| alcorn | Ok I need to go back and rewrite a bunch of specs now that I understand assume a little better! | 23:52 |
| alcorn | Thanks again | 23:52 |
| ZipCPU | Glad I could help! | 23:52 |
| * ZipCPU steps away for supper | 23:53 | |
Generated by irclog2html.py 2.17.2 by Marius Gedminas - find it at https://mg.pov.lt/irclog2html/!