s_frit has quit [Remote host closed the connection]
s_frit has joined #yosys
citypw has joined #yosys
Degi has quit [Ping timeout: 246 seconds]
Degi has joined #yosys
_whitelogger has joined #yosys
<thardin>
some of the set comprehension loops could be ||ized with a little work. they seem to account for a lot of the time
Jybz has joined #yosys
Cerpin has quit [Read error: Connection reset by peer]
Cerpin has joined #yosys
dys has joined #yosys
emeb_mac has quit [Quit: Leaving.]
s_frit has quit [Ping timeout: 246 seconds]
<thardin>
part of my efforts here are finding out where the actual meat of the computations are
jakobwenzel1 has joined #yosys
jakobwenzel1 has quit [Ping timeout: 250 seconds]
<thardin>
inline const std::vector<RTLIL::SigChunk> &chunks() const { pack(); return chunks_; } <-- I presume pack() is idempotent? it's got an ugly hack in it to pretend it's const
<thardin>
the more proper way would be to mark bits_ and chunks_ mutable and maybe have a bool that keeps track of whether they're dirty
Jybz has quit [Quit: Konversation terminated!]
Jybz has joined #yosys
Jybz has quit [Client Quit]
Jybz has joined #yosys
Jybz has quit [Remote host closed the connection]
Jybz has joined #yosys
Jybz has quit [Client Quit]
Jybz has joined #yosys
<thardin>
changing AST_INTERNAL::current_scope to std::unordered_map -> 5% speedup
<daveshah>
FYI, usually Yosys uses dict not std::unordered_map
<thardin>
does it have the same methods as std::map so that it's just a matter of search and replace?
<daveshah>
Yes, I think so
<daveshah>
It should be faster than unordered_map and with a few benefits (deterministic iterator order across runtimes for a start)
mbock has joined #yosys
mbock has quit [Client Quit]
dys has quit [Ping timeout: 246 seconds]
Cerpin has quit [Ping timeout: 265 seconds]
dys has joined #yosys
<thardin>
one telling thing is that for dpram.ys yosys spends 20% of its time in libc
<thardin>
almost 30% with libstdc++
Jybz has quit [Quit: Konversation terminated!]
Jybz has joined #yosys
emeb has joined #yosys
<ZirconiumX>
daveshah: Suppose I wanted to make the ECP5 global promotion more eager. How would I go about that?
<daveshah>
There are some nasty bugs that mean it's non trivial
<daveshah>
I didn't manage to get it to work when I tried
<ZirconiumX>
Hmm.
<ZirconiumX>
Would you mind giving more detail?
<daveshah>
I tried looking for resets in the promotion but for some reason they didn't actually always work
<daveshah>
The entire way globals are represented is a horrible hack
<daveshah>
I'm busy with something else right now but I can try and explain later
<ZirconiumX>
Sure, that's fine
develonepi3 has joined #yosys
<thardin>
roughly half the time of replace_const_cells() is spent in the setup before the loop
Cerpin has joined #yosys
<thardin>
making the stack variables into globals -> 4% speedup
<ZirconiumX>
I don't think they'd accept that kind of change
<thardin>
there's already global state, and those functions are not class methods
<thardin>
but there's likely a better algorithmic way
<thardin>
the triple loop in there would be an excellent candidate for openmp:ing
elGamal has quit [Ping timeout: 250 seconds]
elGamal has joined #yosys
<ZirconiumX>
So I got the design down to 11% and it's still unroutable
<thardin>
is it possible to route via LUTs?
<ZirconiumX>
Depends on the architecture
<ZirconiumX>
But I'm inclined to say no here
<thardin>
surely LUTs can do identity functions?
<thardin>
assuming of course that there's something useful for routing on the other side of it :)
<mwk>
in general routing through a LUT is a valid move
<mwk>
though usually not very optimal (LUTs are slow)
<ZirconiumX>
<thardin> assuming of course that there's something useful for routing on the other side of it :) <-- this definitely doesn't hold for Cyclone V/10GX
<thardin>
interesting
<ZirconiumX>
Each LAB has a block of local interconnect, and while there *is* a fast path to the next row along, the output of the LUT has to go back to the local interconnect block
<ZirconiumX>
Which makes it pointless to route through LUTs
citypw has quit [Ping timeout: 250 seconds]
rswarbrick has joined #yosys
<rswarbrick>
Hi all! Has anyone had any experience using yosys/symbiyosys and black-boxing some components? I've got a design with some SRAMs and would like to prove some assertions without modelling the memories.
<rswarbrick>
Sorry, that wasn't clear: I mean has anyone any experience using yosys/symbiyosys to do formal verification [the rest...]
<ZirconiumX>
That would be ZipCPU
<ZirconiumX>
Who might be asleep at present
<ZipCPU>
No, I'm up
<ZipCPU>
I've been up for ... about four hours or so
<ZipCPU>
What's up?
<rswarbrick>
ZipCPU: Oh, hi! I've been reading some of your blog. Thanks for writing it: it's excellent!
<ZipCPU>
Sure!
<rswarbrick>
Anyway, my question is about black-boxing stuff for formal verification.
<ZipCPU>
<shameless plug> If you like it, please consider sponsoring it! </shameless plug> :D
<rswarbrick>
Do you have any examples where you've black-boxed a memory (since I don't currently care about how that behaves) in order to verify control lines?
<rswarbrick>
:-D Understood!
<ZipCPU>
Hmm ... I have an SRAM example, and several flash examples that might help
<ZipCPU>
I'm not sure I "blackboxed" the components though. That term typically gets used for other things
<ZirconiumX>
I feel like how the memory works is sufficiently relevant for this kind of thing
<rswarbrick>
To be clear: This design doesn't pull SRAM signals out to top-level, and instead instantiates a ram primitive inside it. If I run it through sby, I see a few thousand wire bits for state that I don't care about.
<rswarbrick>
prim_generic_ram_1p is a ram primitive
<rswarbrick>
(SRAM, not SDRAM)
<ZipCPU>
So ... the SRAM is a subcomponent then?
<ZipCPU>
What's the name of the SRAM within that design?
<ZipCPU>
prim_secded_28_22_dec ?
<ZipCPU>
No, that wouldn't be it ...
<rswarbrick>
tag_bank and data_bank
<rswarbrick>
(there are a few of them in a generate loop, so I guess it'll be something a bit more hairy than that)
<ZipCPU>
Ahh ... I see it now
<rswarbrick>
So I imagined that I could hide the actual RAM implementation from Yosys: just like pulling out to top-level would. Then I'd be able to prove things about the control logic which don't care about whether the cache stores the right data or not.
<rswarbrick>
My (somewhat naive) bashing around with blackbox commands didn't seem to help, and I was hoping there was someone I could copy! :-)
<ZipCPU>
Formal can't handle multiplies very well, so I kind of had to "black box" them as you are calling it (it's not a bad term for what you are doing either)
<ZipCPU>
I also recently blogged about that core as well, so you might enjoy reading about what it's supposed to do and how it works (and why I treated the multiplies that way). That's all posted here: http://zipcpu.com/dsp/2020/03/17/cheap-spectra.html
<rswarbrick>
Ah, ok. So the equivalent for me would presumably be hiding the RAMs behind `ifdefs and telling the SMT solver to waggle them as desired?
<rswarbrick>
*to waggle the output lines
<ZipCPU>
That's how I've done it so far
<rswarbrick>
Ok, that makes sense. Just so I get my terminology straight, what does "blackbox" normally mean in yosys-land? (I clearly had it wrong!)
<ZipCPU>
Not necessarily
<ZipCPU>
It normally refers to a stub that's used to describe a primitive with support provided by the hardware
<ZipCPU>
Like you have it here
<ZipCPU>
I ... just wasn't expecting an SRAM interface *within* the design ;)
<rswarbrick>
Yes, it's a new coding style for me too (I came from Broadcom and have only just joined lowRISC).
<rswarbrick>
I guess it doesn't really matter once you get to synthesis, and it means fewer ports to route all the way to the top.
<rswarbrick>
Just so I understand correctly: It wouldn't necessarily be unreasonable to use the blackbox command in this situation; it's just that Yosys's SMT output doesn't seem to support it at the moment. Is that correct?
<ZipCPU>
That is as I understand things
<ZipCPU>
I'm not the one normally working with the internals of Yosys, though, so I'd have to ask others about that to be certain
<rswarbrick>
Great, that makes sense to me. I've not had much experience with Yosys development (currently, I have a grand total of 1 stalled PR). Would the core dev team consider patches to add support for this sort of thing? If so, is it better to do the work and open a PR, or create a tracking issue or... something else?
<ZipCPU>
Yes, the core team accepts patches and PR's although they do struggle to stay on top of them
<rswarbrick>
Well, that's understandable! (And probably a nice problem to have)
<ZipCPU>
Sometimes you can ping them about a particular patch if you need to
<ZipCPU>
Which patch are you referencing that's been stalled?
<rswarbrick>
Specifically, we care about it because our "prim_assert.svh" file (which defines various `ASSERT macros) uses optional arguments in its defines. I can add a SIMPLE_ASSERT flavour to the file, which makes assertions that Yosys supports, but I don't want to change the argument lists.
<ZipCPU>
Let me ask Claire about it tomorrow and see what's up with it. It looks like it's waiting on his review anyway, so let's see where that goes.
<corecode>
i think i have a faint idea how i could come up with formal verification assertions: basically everything you assume as a given, i.e. input signal contract, and everything you assume as given from your own other processes (internal contract)
<rswarbrick>
That's really helpful (as were the hints above). Thank you very much!
<corecode>
does that make sense? am i thinking in the right direction?
<ZipCPU>
corecode: Yeah, pretty much. Remember the master rule, though: assume inputs, assert local state and outputs
<corecode>
right
<corecode>
of course this is much easier when you do it while designing
<corecode>
and not after the fact
<rswarbrick>
corecode: Indeed. I'm currently after the fact on someone else's design and it's not always easy to figure out whether an induction counterexample is showing a bug or whether it's just started somewhere completely silly.
<ZipCPU>
rswarbrick: I feel your pain
<corecode>
i haven't used any formal stuff yet
<corecode>
so, just trying to sort my brain
<ZipCPU>
corecode: You ought to try it. Pick something simple, maybe a FIFO or some such, to try it on and see what you learn from it
<ZipCPU>
At least ... that's where I started. (and got spanked ...)
<rswarbrick>
ZipCPU: Well, to be fair, I now have a *much* better understanding of how the icache works, so I can't really complain. I also have pages and pages of scribbled-out notes...
<rswarbrick>
(with "erk!" or "is this possible???!!" in the margins)
<ZipCPU>
Remember: Use assert()'ions on your local state to pass induction, not assumptions
<ZipCPU>
(assumptions should be applied to "inputs", or in this case to responses from the black box)
<corecode>
rswarbrick: do you print the HDL and mark it up?
adjtm has quit [Remote host closed the connection]
<rswarbrick>
corecode: No! I mean I've got a notebook full of notes to myself while I trace through the logic to figure out what's going on.
dh73 has joined #yosys
adjtm has joined #yosys
<corecode>
ah
<rswarbrick>
corecode: If you start with an existing design, my advice is to write a high-level assertion about ports ("don't drop valid until you see a ready" or similar). Run the induction. It will fail! Look at the trace and try to write an assertion to disallow whatever silliness is going on. Run the induction again with the high level assertion commented out and try to get it to go through. Now uncomment the original assert
<rswarbrick>
ion, lather, rinse, repeat...
<corecode>
yea i need to figure out how to think of assertions
<corecode>
not a natural thing to me
N2TOH_ has joined #yosys
N2TOH has quit [Ping timeout: 250 seconds]
dys has quit [Ping timeout: 250 seconds]
<thardin>
aha there's an #undef YOSYS_NO_IDS_REFCNT preventing my -DYOSYS_NO_IDS_REFCNT from working
dys has joined #yosys
dh73 has quit [Read error: Connection reset by peer]
rswarbrick has left #yosys ["rcirc on GNU Emacs 26.3"]
Vinalon has joined #yosys
<Vinalon>
Hi everyone, I have a question about 'global buffers' and how they relate to package pins, if anyone has a minute
<Vinalon>
I'm configuring a clock input on an iCE40LP384 chip, and copying some 'icestick' configurations to get things set up. The LP384 board's clock is connected to 'IOT_45', which doesn't have an associated 'GBIN' signal
<Vinalon>
on the 'icestick', it looks like the 12MHz clock is connected to 'IOL_7A' / 'GBIN6', and the clock is marked as a global attribute
<Vinalon>
When I try to mark my clock input as 'global', yosys gives me this error: "ERROR: BEL 'X6/Y9/io0' has no global buffer connection available"
<Vinalon>
so I'm guessing that is because of the lack of a 'GBIN' signal on the pin, right? My question is, what are these 'global buffer' signals for and when should they be used?
<ZirconiumX>
That's almost certainly *nextpnr* giving you that error, not Yosys
<Vinalon>
oh - yeah, that would make sense. Sorry, I'm running a script which runs all of those at once. D'oh
<ZirconiumX>
A "global buffer" is how an FPGA routes a global signal, like, say, a clock
<ZirconiumX>
This is really a question for daveshah, but he mentioned he was busy earlier
<Vinalon>
Ah, thanks. No worries; I'm mostly just curious. When I remove the 'global' label, the error disappears. I was just wondering if using global signals was 'cheaper' or more efficient or something.
<ZirconiumX>
More efficient and usually designed with very low skew for clock signals
<Vinalon>
okay; I'll use those pins for clock inputs in the future then. Thank you!
<ZirconiumX>
Resets, too
<ZirconiumX>
Thus why they're called "global" inputs
<Vinalon>
huh, thanks for the tip. Sounds like I should take another look at the datasheets
<daveshah>
Even if you don't use a dedicated global pin, you can still drive the global from anything using a SB_GB
<daveshah>
It just might not be quite as low skew
<daveshah>
ZirconiumX: about the ECP5 globals
<daveshah>
A bit of a horrible hack for the deduplication to work means that globals aren't properly connected in the routing graph
<daveshah>
This is in my long term TODO list to fix but it's backlogged on some other things
<daveshah>
As a result there is a somewhat specialised "router" to deal with the connectivity of these
<daveshah>
For some reason certain connections to logic, as you would have for resets, don't work
<ZirconiumX>
Didn't you mention you were going to revise the ECP5 dedupe to be like prjoxide's?
<daveshah>
I think this is just a bug in my code but it could be a hardware issue too (it might be worth seeing what diamond does)