<cr1901_modern>
Actually I'm really happy it's the PLL... removes all sorts of potentially complicated errors
lutsabound has joined #yosys
kuldeep has quit [Ping timeout: 252 seconds]
kuldeep has joined #yosys
kraiskil has quit [Quit: Leaving]
rohitksingh has joined #yosys
seldridge has joined #yosys
rohitksingh has quit [Quit: Leaving.]
maikmerten has quit [Remote host closed the connection]
seldridge has quit [Ping timeout: 245 seconds]
mirage335 has quit [Ping timeout: 252 seconds]
tinyfpga has quit [Ping timeout: 264 seconds]
mirage335 has joined #yosys
seldridge has joined #yosys
dxld has quit [Quit: Bye]
dxld has joined #yosys
AlexDaniel has joined #yosys
GuzTech has quit [Quit: Leaving]
maikmerten has joined #yosys
kuldeep has quit [Ping timeout: 250 seconds]
kuldeep has joined #yosys
azonenberg_work has quit [Ping timeout: 272 seconds]
azonenberg_work has joined #yosys
rohitksingh has joined #yosys
emeb has joined #yosys
maikmerten has quit [Remote host closed the connection]
rohitksingh has quit [Quit: Leaving.]
s_frit has quit [Remote host closed the connection]
Ristovski has quit [Ping timeout: 245 seconds]
Ristovski has joined #yosys
kristianpaul has joined #yosys
zjoel has joined #yosys
m_t has joined #yosys
<shapr>
edmoore: you done any more FPGA stuff?
<edmoore>
shapr: at St John currently with some guests from JPL
<shapr>
oh cool!
<edmoore>
Fergus Henderson is one of my idols
<edmoore>
Will reply theoroughly later
<shapr>
fair enough :-)
<awygle>
good afternoon all
<awygle>
what's everyone up to today?
<ZipCPU>
I'm writing a blog article about what it takes to formally verify an FFT
<awygle>
I saw your tweets, sounds like it went reasonably well?
<ZipCPU>
Yes/no
<ZipCPU>
All of it works nicely but the soft-multiply enabled butterflies.
<ZipCPU>
I can prove the part that uses DSP's, just not the part that uses the soft (logic) multiplies.
<ZipCPU>
I've got the rest of it though. Well---not the top level. There's hardly any logic at the top level save glueing things together though
lutsabound has quit [Quit: Connection closed for inactivity]
<awygle>
Ah. Could you prove the soft multiply separately and simply assume that it works in the larger system?
<ZipCPU>
My problem was specifically that I didn't feel like I could do that.
<awygle>
It seems a small well defined submodule would be amenable to that
<ZipCPU>
I can separate the multiply nicely--it is such a small defined submodule.
<ZipCPU>
It's just that ... timing is everything.
<ZipCPU>
awygle: I might end up doing that in the end ... this proof is taking 14+ hours and hasn't finished.
<ZipCPU>
(I'm not letting it run too much longer than that.
<ZipCPU>
)
<awygle>
well I look forward to the blog post
<awygle>
if all goes well I will be back to working on my uart proof at some time today
<awygle>
I've been building out some supplemental infrastructure for things like automated performance regression tests
<ZipCPU>
Transmitter or receiver or both?
<awygle>
Receiver (much harder I know)
<ZipCPU>
Synchronous or multiclock?
<ZipCPU>
(I think you had done multiclock before, right?)
<awygle>
I'm not sure I fully understand the terms as applied to this situation. The receiver will be entirely on one clock domain, however the input is asynchronous
<ZipCPU>
The term references a SymbiYosys flag under options: "multiclock on"
<ZipCPU>
If you enable that flag, you then have to assume that your input clock toggles.
<awygle>
Ah, I hadn't used that no
<ZipCPU>
Have you used the Yosys option, clk2fflogic ?
<awygle>
Yes
<ZipCPU>
The "multiclock on" SymbiYosys option is intended to replace "clk2fflogic"
<awygle>
I see
<ZipCPU>
It's put in the [options] section, though, and not the [script] section of the SymbiYosys script.
AlexDaniel has quit [Read error: No route to host]
<ZipCPU>
awygle: So I just killed my longest running butterfly proof (23 hours) and started it again in a way that assume's that
<ZipCPU>
the multiply will work.
<ZipCPU>
Let's see if this new attempt runs any faster.
<awygle>
good luck!
pie___ has quit [Ping timeout: 245 seconds]
xerpi has joined #yosys
pie_ has joined #yosys
xerpi has quit [Remote host closed the connection]
xerpi has joined #yosys
xerpi has quit [Remote host closed the connection]
seldridge has quit [Ping timeout: 246 seconds]
m_t has quit [Read error: Connection reset by peer]