clifford changed the topic of #yosys to: Yosys Open SYnthesis Suite: http://www.clifford.at/yosys/ -- Channel Logs: https://irclog.whitequark.org/yosys
tpb has quit [Remote host closed the connection]
tpb has joined #yosys
rjo has quit [Ping timeout: 246 seconds]
rjo has joined #yosys
simeonm has quit [Ping timeout: 246 seconds]
futarisIRCcloud has quit [Quit: Connection closed for inactivity]
N2TOH has joined #yosys
lambda has quit [Ping timeout: 260 seconds]
lambda has joined #yosys
simeonm has joined #yosys
citypw has joined #yosys
lambda has quit [Ping timeout: 246 seconds]
Degi has quit [Ping timeout: 256 seconds]
Degi has joined #yosys
lambda has joined #yosys
Cerpin has quit [Read error: Connection reset by peer]
Cerpin has joined #yosys
BinaryLust has quit [Ping timeout: 258 seconds]
BinaryLust has joined #yosys
emeb_mac has quit [Quit: Leaving.]
futarisIRCcloud has joined #yosys
dys has joined #yosys
jakobwenzel has joined #yosys
Asu has joined #yosys
BinaryLust has quit [Ping timeout: 246 seconds]
rswarbrick has joined #yosys
jfcaron has joined #yosys
<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?
<rswarbrick> If so, I need to track "I inserted a top-level bind here"
<ZirconiumX> Yes, hierarchy should do nothing if there's nothing to do
vidbina has joined #yosys
<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)
<daveshah> Yes, ideally the bind would be removed by hierarchy
<daveshah> But that depends on how the bind is represented
<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).
<rswarbrick> (module-like for technical reasons to do with where we instantiate cells in genrtlil)
<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?
<rswarbrick> (because a top-level bind might have an effect on modules in x.sv and also on modules in a.sv)
<daveshah> Oh, I don't really know the bind semantics well enough here
<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.
<daveshah> Yeah, it might get complicated if you derive a new parameterisation of foo, too
<daveshah> then I think the attribute approach is indeed best
<rswarbrick> Cool, makes sense.
<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"?
<whitequark> concrete seems reasonable
<rswarbrick> Thanks!
<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?
<rswarbrick> (I'm asking because I can't guarantee that I see a bind directive before I specialise the module)
<rswarbrick> Ohh. I've just seen the hdlname attribute. I guess I can work from there.
<Sarayan> isn't it hdlname that's going to slightly change for the better?
<whitequark> hm?
<whitequark> hdlname on modules won't change
<Sarayan> dots to spaces
<whitequark> nope, currently there is no hdlname with dots
<whitequark> it's just the wire name
<Sarayan> ok cool then :-)
vidbina has quit [Ping timeout: 260 seconds]
vidbina has joined #yosys
vidbina has quit [Ping timeout: 246 seconds]
X-Scale` has joined #yosys
X-Scale has quit [Ping timeout: 256 seconds]
X-Scale` is now known as X-Scale
X-Scale has quit [Client Quit]
dys has quit [Ping timeout: 260 seconds]
emeb has joined #yosys
Cerpin has quit [Ping timeout: 246 seconds]
<ZirconiumX> daveshah, mwk: https://github.com/YosysHQ/yosys/pull/2096 <-- thoughts?
<tpb> Title: [RFC] Add conditional-insert operator to pool/dict by ZirconiumX · Pull Request #2096 · YosysHQ/yosys · GitHub (at github.com)
jfcaron has quit [Ping timeout: 265 seconds]
<mwk> I'm not convinced it improves readability
<whitequark> neither am I
<whitequark> I'm not strongly opposed but I don't see the benefit
<ZirconiumX> Mmm
<rswarbrick> ZirconiumX: Could you use something like std::copy_if for this?
<ZirconiumX> I don't think so
<ZirconiumX> You'd have to make two passes over the data
<rswarbrick> You'd need something like std::back_inserter too.
<rswarbrick> So std::copy_if(pool.begin(), pool.end(), dest_pool.inserter(), my_predicate);
<ZirconiumX> I feel like ranges are really important for readability
<ZirconiumX> pool.begin()/pool.end() is a bit messy
<rswarbrick> In which case, I don't understand your PR: isn't it basically the same syntax?
<ZirconiumX> I feel like range-style insert_if *is* an improvement though
citypw has quit [Ping timeout: 240 seconds]
vidbina has joined #yosys
Cerpin has joined #yosys
jakobwenzel has quit [Quit: jakobwenzel]
rlee287 has joined #yosys
jakobwenzel has joined #yosys
BinaryLust has joined #yosys
dys has joined #yosys
vidbina has quit [Ping timeout: 265 seconds]
jfcaron_ has joined #yosys
emeb_mac has joined #yosys
jakobwenzel has quit [Quit: jakobwenzel]
<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
<rlee287> Is this understanding correct?
rswarbrick has quit [Ping timeout: 272 seconds]
rlee287 has quit [Quit: Konversation terminated!]
jfcaron_ has quit [Ping timeout: 246 seconds]
Asu has quit [Ping timeout: 260 seconds]
captain_morgan has quit [Read error: Connection reset by peer]
captain_morgan has joined #yosys
emeb has quit [Quit: Leaving.]
alcorn has joined #yosys
<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?
<tpb> Title: [SystemVerilog] Cover passes but assume fails - Pastebin.com (at pastebin.com)
<ZirconiumX> ZipCPU: ^
<ZipCPU> alcorn: You can't assume it because it's false on the first clock tick
<ZipCPU> ZirconiumX: Thanks for the flag
<ZirconiumX> np
<ZipCPU> Assuming something for which there's no way to make it true leads to what's known as a "WARMUP FAILURE"
<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.
<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
<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?
<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.
<ZipCPU> assume limits the size of the search space the solver works with.
<ZipCPU> See ... https://zipcpu.com/quiz/2019/08/03/quiz01.html for more information
<tpb> Title: Quiz #1: Will the assertion below ever fail? (at zipcpu.com)
<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
<ZipCPU> The logic of the counter, however, will have it just counting up to 65535 and then rolling over
<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.
* ZipCPU needs to run for supper
<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.
<tpb> Title: My first experience with Formal Methods (at zipcpu.com)
<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
<ZipCPU> alcorn, that's not quite true. You can do an: always @(*) if (f_past_valid) assume(something_true_only_after_the_first_clock);
<alcorn> I have actually read a few of your blog posts before and they have been very illuminating, so thank you!
<ZipCPU> Np
<alcorn> ok so you just have to guard your assumes with some other logic
<alcorn> a naked assume has to be satisfiable on the first cycle
<alcorn> ?
<ZipCPU> You may. It depends on what you want to do.
<ZipCPU> A naked assume needs to be satisfied on *EVERY* cycle
<alcorn> Ok I see
<ZipCPU> always @(*) assume(!S_AXI_ARVALID); // will keep a slave component from ever receiving an AXI read request
<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
<ZipCPU> Absolutely!
<ZipCPU> The solver has to be ... very exacting. It must follow very strict rules, set forth by you. That's sort of the point.
<alcorn> Right
<ZipCPU> It's quite the stickler for details.
<alcorn> Really I was just confusing the semantics of cover and assume
<ZipCPU> cover(X) -> find one way, any way, to make X true
<ZipCPU> assume(X) -> don't consider any circumstances where !X
<ZipCPU> assert(X) -> a challenge to the solver. I don't think X will ever happen. Go ahead, prove me wrong, I dare you.
<alcorn> How would you go about assuming that f_past_valid has been true for several cycles?
<alcorn> I've been using this construction `assume(f_past_valid && $past(f_past_valid, 1) && $past(f_past_valid, 2) && ...)`
<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;
<alcorn> but this discussion has me questioning if it is right
<ZipCPU> if (f_past_valid_counter > 10) assume(XYZ);
<ZipCPU> No, that's not how you'd do it. Use f_past_valid in a condition, sort of like:
<ZipCPU> if (f_past_valid && $past(f_past_valid) && $past(f_past_valid, 2)) assert(XYZ);
<ZipCPU> Remember: Don't *assume* anything but inputs.
<alcorn> Ok this is sinking in
<ZipCPU> You shouldn't be making assumptions about f_past_valid at all
<alcorn> Righto
<alcorn> Ok I need to go back and rewrite a bunch of specs now that I understand assume a little better!
<alcorn> Thanks again
<ZipCPU> Glad I could help!
* ZipCPU steps away for supper