develonepi3 has quit [Remote host closed the connection]
develonepi3 has joined #yosys
promach_ has quit [Ping timeout: 252 seconds]
develonepi3 has quit [Remote host closed the connection]
m_t has joined #yosys
Kooda has quit [Remote host closed the connection]
emeb has joined #yosys
maikmerten has quit [Remote host closed the connection]
m_t has quit [Quit: Leaving]
emeb has quit [Quit: Leaving.]
develonepi3 has joined #yosys
emeb_mac has joined #yosys
emeb_mac has quit [Quit: Leaving.]
azonenberg_work has quit [Ping timeout: 252 seconds]
azonenberg_work has joined #yosys
m_t has joined #yosys
X-Scale has quit [Ping timeout: 264 seconds]
develonepi3 has quit [Remote host closed the connection]
X-Scale has joined #yosys
DeadSanity has joined #yosys
DeadSanity has left #yosys [#yosys]
emeb_mac has joined #yosys
gnufan_home has quit [Ping timeout: 244 seconds]
<ZipCPU>
awygle: (Now that I've made fun of your answer ...) Did you actually find a reason why the quiz would've failed induction? Or did you just guess? (which was my assumption)
<awygle>
ZipCPU: it'll pick an initial state which is nonzero
<awygle>
and fail immediately when the clock ticks
<ZipCPU>
You cant. It's given an initial zero state.
<awygle>
induction doesn't respect initial blocks
<awygle>
it's not time 0, it's "some time T"
<ZipCPU>
Ahh, I get it. And how many induction clocks would it take before it succeeds?
<awygle>
it's only initial from the perspective of the counter example trace
<awygle>
ZipCPU: you mean if it did start with counter == 0?
<ZipCPU>
No. Let's assume it starts with counter == 512.
<ZipCPU>
Why not? counter == 512 on step one. What happens on step two of induction?
<awygle>
it'll fail on the first tick of smt_clock or whatever it's called
<awygle>
due to the MAX_AMOUNT assertion
<ZipCPU>
And ... then what happens?
<ZipCPU>
If the induction length was more than two states?
<awygle>
i_clk doesn't even need to tick
<awygle>
it actually can't start with 512, that's an invalid state
<awygle>
I feel like I'm misunderstanding your question lol
<ZipCPU>
No, i_clk ticks on every interval.
<ZipCPU>
Try it. Go ahead, type it in and try it and see what happens.
<ZipCPU>
No one seems to have done that yet.
<awygle>
it doesn't have to, necessarily. it probably will in this case though.
* awygle
seizes the opportunity to avoid cleaning for a bit
<awygle>
I feel like trying it without giving an answer first would be cheating
<awygle>
how many bits is counter?
<awygle>
I assume 32 since you're not sizing anything
<ZipCPU>
Five or more. It doesn't matter that much.
<ZipCPU>
MAX_AMOUNT should be set to 23.
<ZipCPU>
Sorry, I mean 24.
<awygle>
i suppose i should update yosys... it's been like six months
<ZipCPU>
Wow, yeah, a lot has changed.
<awygle>
i really should have submitted that "build on cygwin" patch
<ZipCPU>
Does it not build on cygwin currently?
<awygle>
cr1901_modern: want to patch yosys' makefile so it stops trying to pass -fPIC on cygwin?
<awygle>
i can't remember the right way to detect cygwinness or i'd do it myself
<awygle>
tsk tsk, a warning in verific.cc
* awygle
should have given this build more cores
<awygle>
i keep forgetting i upgraded all my systems
<awygle>
so, while i wait for this to build, how are things with you, ZipCPU?
<ZipCPU>
They are going okay.
<awygle>
raking in the dough from your many and varied activities? ;)
<ZipCPU>
I tried building an analytical placer for nextpnr last night.
<awygle>
oh do tell
<ZipCPU>
No, not raking any dough at all.
<ZipCPU>
Well, not that much, but having fun.
<ZipCPU>
Okay, so ... nextpnr
<awygle>
did you find nextpnr easy to work with? what algorithm did you use?
* awygle
shuts up and lets you talk
<ZipCPU>
An analytical placer is one that tries to place the elements in a design based upon the direct solution to a matrix equation.
<awygle>
i am familiar with the theory (and even some of the practice)
<ZipCPU>
I got the matrix equation up and running. I was surprised at how fast it solved the 4500 element linear algebra equation.
<ZipCPU>
That didn't come out right--hopefully you understand what I meant. 4500 unknowns, 4500 equations, etc.
<awygle>
yup
<ZipCPU>
I had a couple problems.
* awygle
notes that abc has moved to github, removing the hg dependency from yosys. awygle approves.
<ZipCPU>
1) I'm trying to solve a minimum distance problem, i.e. put a number of quadratic (distance) equations together, and then find the minimum
<ZipCPU>
2) At one point, the entire solution landed on the trivial answer (zero)
<ZipCPU>
3) I couldn't figure out how to get the minimum eigenvalue that I needed for the non-trivial solution
<ZipCPU>
4) I then tried to map the points I had, and resolve, hoping it would move from the non trivial solution
<ZipCPU>
5) Then I noticed it was placing everything at 1,1, so dug into how to tell if something was assigned already
<ZipCPU>
6) That broke something else, so I'm now stuck on an assertion failure and just working on blog posts.
<awygle>
the algorithms i've looked at take two approaches to solving this - one, they assign fixed values (e.g. IO pads) first, and two, they have some kind of legalization step (recursive bipartition for example)
<ZipCPU>
Yes, so here's how that worked for me ...
<ZipCPU>
1) Assigning I/O's got me in trouble with an assert elsewhere in the design. (That's the one I need to dig into and debug still)
<ZipCPU>
2) I had a really cool idea for legalization: Search through all unplaced cells, and calculate the distance to their nearest (legal) placement. For each cell, pick the closest placement. Then place the cell that has the farthest distance to its closest placement.
<ZipCPU>
I'm going to need to speed up #2, right now, though, 'cause it's taking about 2 seconds per each cell it places (of 4500 or so)
<ZipCPU>
I figured that was a fun approach to legalization.
<ZipCPU>
Sadly, it's not really good enough. I'm going to need to get that minimum eigenvalue solution somehow intertwined with this.
<ZipCPU>
Are you familiar with the eigenvalue method?
<ZipCPU>
It was one of the first articles I found on the topic of building placers--that made clear sense to me.
<awygle>
i'm familiar with eigenvalues generally, but it's been a while since i did my linear algebra course. not completely sure what you're referring to
<ZipCPU>
Would you like me to explain? It's kind of a fun and neat algorithm.
<awygle>
sure!
* awygle
tries to remember how to convince yosys to run a proof...
<ZipCPU>
Use SymbiYosys--it's a lot easier.
<awygle>
yeah i'm pulling up my old stuff
<ZipCPU>
Ok, eigenvalue stuffs: start by setting up a sum of all the squared distances between related elements. We'll let the vector x be the locations of all the items that need to be placed (x and y), and A be the quadratic relations between them.
<ZipCPU>
The goal of the placer is then to minimize x^T A x. The trivial solution x=0 is the immediate result.
<ZipCPU>
If you then insist that x^T x = 1 (i.e., don't accept the trivial solution), you can dig into the minimum eigenvalue for A.
<ZipCPU>
Let's assume that is lambda, and it's associated eigenvector is v. Set x = v.
<ZipCPU>
The article notes that if you hvae both x and y coordinates in A, then you might need to use two eigenvectors--one for x positions and one for y positions.
<ZipCPU>
Use those (one or two) eigenvectors for the positions of your elements, and you have your minimum solution.
<ZipCPU>
Aside from figuring out how to do the eigenvector calculation, my next problem is how do I properly scale the result to the design array.
<ZipCPU>
(I have that currently as is)
<ZipCPU>
One thought is to calculate sigma_x^2 = SUM (all placed locations x'values)^2, and scale the design so sigma_x^2 matches the device and then repeat for sigma_y.
<ZipCPU>
Still trying to work out that part.
<awygle>
hm, i'd like to see the article
<ZipCPU>
I also like my "least worst" solution that I'm currently trying to work with, although I'm not yet convinced it'll work yet.
<awygle>
but yes, this makes sense
<ZipCPU>
Want the article? I can dig it up around here somewhere ...
<awygle>
how do i tell sby to give me an example trace again? it's like -g to something... can't remember where tho
<ZipCPU>
No, not at all.
<awygle>
oh cool, multiple verification tasks are a thing now, that's extremely useful
<ZipCPU>
For any failing design sby gives you a trace automatically.
<awygle>
right, but i meant for success
<ZipCPU>
sby -f script.sby
<ZipCPU>
Ahh ... for success you need a cover statement.
<ZipCPU>
And mode cover as well.
<ZipCPU>
The -g only ever gave me trivial solutions.
<awygle>
where would it go though?
<ZipCPU>
? Not sure I follow your question. Where would (SymbiYosys, placer, ??) go through (where)?
<awygle>
where do i put a -g to get a (trivial) example trace?
<ZipCPU>
BTW, the article is: "An r-Dimensional Quadratic Placement Algorithm" by Kenneth M. Hall, published in Management Science, Volumne 17, No 3, Theory Series (Nov 1970, pp 219-229
<awygle>
it's an argument to yosys smtbmc but i don't know where to put it in an sby file
<ZipCPU>
Forget the -g. It was a useless argument.
<awygle>
basically, it claims induction passed, and i want to see how
<awygle>
because i don't believe it :p
<ZipCPU>
Lol
<awygle>
also i failed bmc because of not having an f_past_valid, which feels like a dirty trick :p
* ZipCPU
gets suddenly quiet
m_t has quit [Quit: Leaving]
dys has quit [Ping timeout: 252 seconds]
<awygle>
i got it to pass bmc without changing the code :p
<awygle>
(i passed -t 2:20 to yosys-smtbmc. which, yes, is also cheating)
<ZipCPU>
:D
<awygle>
i don't understand why it's passing induction though. it must have to do with how $past is handled in induction mode initial state selection, which i don't really have a firm grasp on
<awygle>
or, no, hang on
<awygle>
induction goes the other way
<awygle>
that's why this works
<ZipCPU>
Neat, huh?
<awygle>
it must "start", at the end, in a valid state. then it works backwards and tries to find an invalid one. and since $past(counter == 0) is true at the end, it must always be true
<awygle>
i see how i got this wrong, though - it's almost as though somebody with a blog wrote " The induction step works by picking random initial values for every registered signal within the design. " :p
<ZipCPU>
:P
<ZipCPU>
Got to go. Thanks for the fun chat! (Hope you don't mind me making fun of you on twitter .... too much)
<awygle>
not at all
<awygle>
thanks for the paper reference, i'll read it
<awygle>
and i may ping you about nextpnr related things later this evening, if you're around/have time
<awygle>
hm, the paper makes sense, but sort of begs the question on discretization/legalization at the end. especially since the referenced term "minimum squared motion" appears to not be a thing
digshadow has quit [Ping timeout: 252 seconds]
<ZipCPU>
Minimum squared *motion* ?
<awygle>
right, i've never heard it either
<awygle>
but it's mentioned in the conclusion as a possible way to discretize results
<ZipCPU>
"Also, it may serve as a basis for mapping problems, where the analog positions of the nodes must be mapped into discrete locations (perhaps with minimum squared motion)." Yeah, makes you wonder.
<ZipCPU>
So, my thought was to calculate an initial solution, x0, and then to add some amount of this eigenvector solutoin to it, x0 + lambda v, to get to a final solution.
<ZipCPU>
I'm facing a couple problems when doing so.
<ZipCPU>
1) what lambda to use?
<awygle>
my short-term intent is to try Parallel Tempering as it's a straightforward(ish) extension of SA
<ZipCPU>
2) What happens when the entire design aggregates around one or two pins, and hence needs to be expanded?
<ZipCPU>
3) What happens if the design isn't centered like it needs to be?
<ZipCPU>
4) If there are columns of "special" cells (memories, DSP blocks, etc) that don't fit the model at all.