<whitequark[cis]>
hm, that is pretty dirty. interesting that boneless benefits from it far more too
<whitequark[cis]>
i think the main thing that stops me is that some other reasonable looking rules are counterproductive
<whitequark[cis]>
as a result i have no faith that this is actually the right change to make
<mei[m]>
it would probably make sense to modify the assign lowering to not emit this instead
<mei[m]>
the issue with that is that it requires a refactoring that looks painful
<whitequark[cis]>
since some of the other reasonable patterns are *counter*productive im happy to keep the PR open until someone does the refactoring i think
<galibert[m]>
huhu, for once arch is not up-to-date enough to reach edition2024
<mei[m]>
not using rustup?
<galibert[m]>
no, trying to follow the system distribution
<galibert[m]>
there are pro and cons for that, of course
<galibert[m]>
they put a new version in testing yesterday, so that should be ok in a handful of weeks
<widlarizerEmilJT>
Trying to use prjunnamed/amaranth in a nix flake and getting my teeth kicked in by pdm-backend version "2.4.3" not actually being 2.4.3 and I have no idea what's going on. Repro is `nix develop`
<widlarizerEmilJT>
Wait, this pulls in 2.1.8. I think I know what's going on, I was previously overriding the version, but didn't override the hash, which would use 2.1.8 and call it 2.4.3. Yikes.
<widlarizerEmilJT>
Nothing particularly standing out in my five stage pipelined RV32IM
<widlarizerEmilJT>
this is targeting siliconblue for the demo
<widlarizerEmilJT>
<povikMartinPovie> "if you want to look at the code:..." <- Wanna push what it to a fork? I'd like to poke around and this isn't self-contained enough for that
<povikMartinPovie>
I guess it could be written as "to.x implies from.x"
<ignaloidas>
seems fairly confusing for me to compare whether two bit vectors are the same by comparing whether left == (left & right)
<povikMartinPovie>
feels like there's something subtle going on, I don't know
<povikMartinPovie>
note that they are not being tested for equality, this is a test of to refining from, so an x-state in from can be refined to 0/1 in to, though not the other way around
<povikMartinPovie>
with that the code just looks to be the way Catherine has decided to write "implies"
<ignaloidas>
oh, found my problem elsewhere
<ignaloidas>
implementing traits from name inference isn't the best strategy to avoid subtle bugs
<whitequark[cis]>
<povikMartinPovie> "with that the code just looks to..." <- yes
<whitequark[cis]>
there is no 'bvimplies' in SMT
<whitequark[cis]>
you kind of have to write it out
<whitequark[cis]>
i think Wanda also found it confusing during review
Guest53 has joined #prjunnamed
Guest53 has left #prjunnamed [#prjunnamed]
<ignaloidas>
implemented ~90% of SAT verification backend (passes all but 5 tests because of missing implementations), and it seems to be almost 100x faster
<ignaloidas>
code is a horrific mess that will take a while to fix into something acceptable
<whitequark[cis]>
i presume it is not using stdio to talk to the solver?
<whitequark[cis]>
i think that is the bulk of the time taken by the current SMT impl
<whitequark[cis]>
i don't love it but i'm also unconvinced this is the way to go
<ignaloidas>
It's actually writing the solution to a temp file and getting the output from solvers stdout
<ignaloidas>
the format is extremely simple, just lines of numbers, so formatting is essentially free
<povikMartinPovie>
I'm lacking a way to debug print a single cell
<povikMartinPovie>
not really, there's design.display_cell
<Wanda[cis]>
oh hey, I managed to create a perfectly unhinged issue as #69
<Wanda[cis]>
excellent, I wasn't even trying
<cr1901>
What
<cr1901>
s icecube-based*?
<galibert[m]>
Catnip overdose
<leocassarani[m]>
nice
<leocassarani[m]>
I like what you've done with the sub-issues for the roadmap btw! I didn't even know GitHub supported that
<Wanda[cis]>
sorry we have decided that reversing bitstreams is too hard, we will only use vendor P&R from now on
<mei[m]>
seems to be a recent feature
<Wanda[cis]>
yeah it's some recent stuff
<galibert[m]>
Yeah, must have been good catnip
<cr1901>
Oh I should've actually opened the link...
<galibert[m]>
of course within the umbrella of #17 is suddendly makes complete sense
<Wanda[cis]>
the last step is cutting the umbilical icecube.
<galibert[m]>
yeah :-)
<Wanda[cis]>
it's a very good plan
<Wanda[cis]>
but I can't take credit for it
<galibert[m]>
I think xilinx stuff may allow something similar. Quartus is very unwilling at showing its work though iirc
<Wanda[cis]>
Cat convinced me to do it like that. I considered it completely batshit at first, then it dawned on me that it's actually the only reasonable way to do this
<galibert[m]>
well, you're in a domain where batshit is the most reasonable
<Wanda[cis]>
yeah this is also going to be the blueprint for xilinx (though reduced in scope because the common infra will be already in place)
<Wanda[cis]>
galibert[m]: what do you mean? quartus emits perfectly reasonable P&R data
<galibert[m]>
hmmmm
<galibert[m]>
oh yeah, yeah it does. What it doesn't allow iirc is giving your stuff to turn into a bitstream, like xilinx allows with xdl
<galibert[m]>
(or did, I haven't used xilinx stuff in years)
<mei[m]>
galibert[m]: isn't quartus showing its work the key reason why prjcombine has a relatively easy time with xilinx?
<Wanda[cis]>
that doesn't sound right either, you can actually give quartus a routing file
<Wanda[cis]>
(not that we'd need it)
<cr1901>
> parse icecube placer PCF to obtain final placement, back-annotate it onto the netlist <-- icecube emits a PCF with the final placement of everything?
<mei[m]>
ah, wait, quartus is the altera stuff
<cr1901>
As opposed to having to also disassemble the bitstream to get placement info*?
<Wanda[cis]>
cr1901: several PCFs actually! I have no clue why it emits so many PCFs
<Wanda[cis]>
but yes
<mei[m]>
this is a certified neocat_woozy moment on my part
<Wanda[cis]>
it also emits the complete routing graph
<cr1901>
Huh... :o
<Wanda[cis]>
though it's easier to parse the bitstream.
<galibert[m]>
you can? I missed that when I started the RE. Oh well
<Wanda[cis]>
(prjcombine does a really weird combo of recovering most routing information from the routing graph via atrocious name conversion code, but also filling in missing data from btistream disassembly for hard IP related wires, which are a pain to deal with otherwise)
<Wanda[cis]>
(or, um, will, when I get around to writing that part)
<Wanda[cis]>
ohhh hold on
<Wanda[cis]>
I actually implemented that already
<Wanda[cis]>
I have no memory of it
<Wanda[cis]>
mmm yeah
<Wanda[cis]>
that's some cute code
<Wanda[cis]>
I particularly like the circular dependency involved
<mei[m]>
bootstrapping :3
<Wanda[cis]>
it's reversing the bitstream format, but for that it needs routing information, which it obtains partially by disassembling the bitstream
<Wanda[cis]>
and it does that by pulling in the already-done bitstream database for an earlier device that doesn't have hard IP and uses that for disassembly
<Wanda[cis]>
it may be a little mismatched, but the routing bits are the same, so oh well
<Wanda[cis]>
one day I should write down all the weird tricks that make prjcombine capable of reversing FPGAs at scale.
<galibert[m]>
that will be a fun read
<Wanda[cis]>
well. the good news is that the bitstream disassembly in prjunnamed won't be anywhere near as batshit, since it can just use the final database