<ZipCPU>
awygle: Thought you might want to know .... that proof from a couple of days ago is still going.
q3k has quit [Read error: Connection reset by peer]
<awygle>
ZipCPU:... Wow
q3k1 has joined #yosys
q3k1 is now known as q3k
<ZipCPU>
It's been 41hours since the last basecase step, 13 since the last induction step completed
<shapr>
yikes
seldridge has joined #yosys
<ZipCPU>
See .... this is the problem with trying to formally verify a multiply
<cr1901_modern>
np-hard
<cr1901_modern>
?*
<ZipCPU>
Formal verification in general is roughly exponential in complexity
<ZipCPU>
The trick for the formal verification engineer is to manage that complexity, so as to keep the exponential from taking off.
<ZipCPU>
cr1901_modern: The interesting part of this is that I'm only verifying a butterfly that would be a component of an FFT.
<ZipCPU>
At this point, it would be impossible to aggregate the butterfly into anything more complex than this
maartenBE has quit [Ping timeout: 252 seconds]
maartenBE has joined #yosys
ym_ is now known as ym
<ZipCPU>
I wonder if another solver would work better. I've been using smtbmc. I tried abc pdr--it offered no insight into how far it had gotten, whereas smtbmc had. So I killed it. aiger avy immediately ran out of memory. Maybe aiger suprove will do something useful? It's certainly using all of my CPU cores.
<cr1901_modern>
I only recently learned about aiger as an alternate solver. Kinda amused it ran out of memory so quickly
<cr1901_modern>
But hey, "10 times faster in a binary format" is still... 4.1 hours :P?
<ZipCPU>
You think it'll be 10 times faster?
<cr1901_modern>
just a guess
<ZipCPU>
Morning will tell
<ZipCPU>
Just be aware ... that 41 hrs number? That was since the last step. I think the entire process has been going 48 hrs before I just killed it.
<ZipCPU>
(It's also running on a faster machine, so I haven't lost any of that work yet.)
<cr1901_modern>
It'd be nice if there were a way to get smt solvers to "feed back" how much more of the space they have to check.
<cr1901_modern>
Even as a hueristic
<ZipCPU>
The SMTBMC solvers do
<ZipCPU>
The aiger and abc solvers don't.
<pie__>
ZipCPU, what are you proving?
<ZipCPU>
pie__: Welcome to the forum! I'd like to blog about what it takes to formally verify an FFT. I've got all the pieces of the FFT verified but one: the butterfly that uses logic multiplies.
<pie__>
ah *thumbs up*
<ZipCPU>
I can formally verify the butterfly that uses hardware multiplication acceleration
<ZipCPU>
I can formally verify the last two butterflies that don't use any multiplies
<pie__>
will be interested to read the article when it comes out, if you remember, ping me :P
<ZipCPU>
I can formally verify the bit reversal stage, and the "fft stage" logic that feeds the butterfly.
<ZipCPU>
Expect the article sometime next week.
<ZipCPU>
Even if I can't solve this problem, I want to push the article out anyway.,
<pie__>
cool
<ZipCPU>
I would've published it already, save that ... I need to work to make an FFT understandable for a general audience
<ZipCPU>
That's what's holding me up right now.
<pie__>
i saw some good atricles on such a while back
<pie__>
well ok that may have just been the normal FT
<ZipCPU>
The FFT is just an implementation of a "normal" discrete FT
<ZipCPU>
My problem is that I've worked with FFT's for *SO MANY* applications and purposes, that it's become essentially to everything I think of. Now, how do you explain that? :D
<ZipCPU>
I'll probably punt and not explain it much at all.
<ZipCPU>
Then, I'll reference it in future articles discussing FFT applications
<pie__>
im in windows dependency compilation hell
<ZipCPU>
Ouch! What are you trying to build?
<pie__>
some backend library for some OSS chat program, there's deps on a couple enc/dec libraries, ffmpeg was nice enough to ship .libs, libvpx and libopus not so much
<ZipCPU>
Wow, okay, not something I have any experience with. Good luck, and I hope it goes well!
<pie__>
just a huge pain in the butt because im not used to dealing with this crap. one thing wants msys the other wants cygwin, cant tell how to compile it with the visual studio environment and this and that
<pie__>
</rant>
<pie__>
:P
<ZipCPU>
Yuck
* pie__
gets back to that
* ZipCPU
decides to dream about FFT's instead.
<pie__>
everyone should just use nixpkgs...
<pie__>
ZipCPU, good joice
<pie__>
choice
<pie__>
this isnt even grunt work its just blindly screwing about with commands.
<pie__>
waste of engineering time :P
<ZipCPU>
Voodoo computing! Fixing what isn't broken in an effort to find and fix what is
lutsabound has quit [Quit: Connection closed for inactivity]
seldridge has quit [Ping timeout: 252 seconds]
azonenberg_work has quit [Ping timeout: 272 seconds]
azonenberg_work has joined #yosys
rohitksingh has joined #yosys
dys has joined #yosys
rohitksingh has quit [Quit: Leaving.]
zkms is now known as __builtin_trap
__builtin_trap is now known as zkms
emeb_mac has quit [Quit: Leaving.]
dys has quit [Ping timeout: 264 seconds]
GuzTech has joined #yosys
fsasm has joined #yosys
rohitksingh has joined #yosys
rohitksingh has quit [Quit: Leaving.]
lvrp16 has joined #yosys
rohitksingh has joined #yosys
mirage335 has quit [Ping timeout: 252 seconds]
rohitksingh has quit [Ping timeout: 244 seconds]
rohitksingh has joined #yosys
rohitksingh has quit [Read error: Connection reset by peer]
xdeller_ has joined #yosys
xdeller has quit [Remote host closed the connection]