<cr1901_modern>
>ZipCPU: I imagine things will change once some genius gets to thinking about it hard enough.
<cr1901_modern>
(assert (= (* a b) $SOME_LARGE_NUMBER))
<cr1901_modern>
^This is equivalent to determining whether a number is prime or not, which doesn't have an efficient algorithm. So I don't think it's possible to make reasoning about multiplies fast in general.
<cr1901_modern>
(assert (and (not (= a 1)) (not (= b 1))))
<awygle>
cr1901_modern: i take your point but what is needed to use multipliers in formal verification is to prove that the circuit yields (* a b) for any a, b in (some number space)
<awygle>
so hopefully we're not into quantum computing to make it work
<awygle>
for instance we can formally prove adders without solving subset sum
<ZipCPU>
Yet ... some things regarding multiplies *can* be handled. For example, a beginning solver should be able to determine that (a+b)*c = a*c+b*c
<ZipCPU>
Just some simple logic like that would help me prove that y[n] = SUM_k h[k] x[n-k]. I don't really need to know that the multiply *works*, but what I do need to know is whether or not I implemented such an equation properly.
<sorear>
PRIMES has been known to be in BPP for years
m_t has quit [Quit: Leaving]
m_w_ has quit [Quit: Leaving]
digshadow has quit [Ping timeout: 260 seconds]
ZipCPU|Laptop has quit [Quit: Warp drive ready at your command, Captain!]
heath has quit [Ping timeout: 256 seconds]
seldridge has joined #yosys
seldridge has quit [Client Quit]
seldridge has joined #yosys
heath has joined #yosys
seldridge has quit [Ping timeout: 240 seconds]
proteusguy has quit [Ping timeout: 240 seconds]
proteusguy has joined #yosys
srk has quit [Ping timeout: 256 seconds]
srk has joined #yosys
leviathan has joined #yosys
adj__ has quit [Quit: Leaving]
AlexDaniel has quit [Ping timeout: 265 seconds]
pie_ has joined #yosys
proteusguy has quit [Read error: Connection reset by peer]
pie_ has quit [Ping timeout: 240 seconds]
proteusguy has joined #yosys
proteus-guy has quit [Remote host closed the connection]
sklv has quit [Quit: quit]
proteus-guy has joined #yosys
proteusguy has quit [Ping timeout: 268 seconds]
dys has joined #yosys
xrexeon has joined #yosys
xrexeon has quit [Max SendQ exceeded]
proteusguy has joined #yosys
xrexeon has joined #yosys
jwhitmore_ has joined #yosys
xrexeon has quit [Read error: Connection reset by peer]
xrexeon has joined #yosys
proteus-guy has quit [Ping timeout: 256 seconds]
proteus-guy has joined #yosys
digshadow has joined #yosys
proteusguy has quit [Ping timeout: 265 seconds]
oldtopman has quit [Ping timeout: 276 seconds]
xrexeon has quit [Ping timeout: 240 seconds]
oldtopman has joined #yosys
proteusguy has joined #yosys
jwhitmore_ has quit [Ping timeout: 265 seconds]
eduardo_ has joined #yosys
eduardo has quit [Ping timeout: 248 seconds]
jwhitmore_ has joined #yosys
fsasm has joined #yosys
jwhitmore_ has quit [Ping timeout: 252 seconds]
cr1901_modern has quit [Read error: Connection reset by peer]
cr1901_modern has joined #yosys
_whitelogger has joined #yosys
pie_ has joined #yosys
ravenexp has quit [Ping timeout: 256 seconds]
ravenexp has joined #yosys
oldtopman has quit [Ping timeout: 255 seconds]
pie_ has quit [Ping timeout: 276 seconds]
cemerick has joined #yosys
oldtopman has joined #yosys
jwhitmore_ has joined #yosys
pie_ has joined #yosys
cemerick_ has joined #yosys
m_t has joined #yosys
pie_ has quit [Ping timeout: 255 seconds]
cemerick has quit [Ping timeout: 256 seconds]
Marex_ has joined #yosys
jophish has joined #yosys
Guest88515 has quit [Ping timeout: 264 seconds]
Marex has quit [Ping timeout: 264 seconds]
clifford_ has quit [Ping timeout: 264 seconds]
captain_morgan has quit [Ping timeout: 264 seconds]
captain_morgan has joined #yosys
clifford_ has joined #yosys
jwhitmore_ has quit [Ping timeout: 240 seconds]
jwhitmore_ has joined #yosys
captain_morgan_ has joined #yosys
captain_morgan has quit [Ping timeout: 264 seconds]
<daveshah>
promach__: I'm pretty sure `generate` isn't allowed in `always`
<promach__>
daveshah: I see, that is the bug
<ZipCPU>
A for loop is allowed within an always block, but you'll need an "integer" variable index instead of a "genvar"
<promach__>
is there way to use generate within always block ?
<daveshah>
promach__: No. You can either use a normal `for` loop with constant bounds, or put the `always` inside the `generate` instead
<promach__>
daveshah: ok
AlexDaniel has joined #yosys
jeandet has quit [Ping timeout: 255 seconds]
pie_ has quit [Ping timeout: 255 seconds]
pie_ has joined #yosys
jeandet has joined #yosys
<promach__>
daveshah: so, it is also not possible to assign genvar to wire as well ?
xrexeon has quit [Ping timeout: 276 seconds]
<daveshah>
promach__: not sure, you'll have to try
<promach__>
I tried, yosys threw out error
pie_ has quit [Ping timeout: 240 seconds]
pie_ has joined #yosys
pie__ has joined #yosys
pie_ has quit [Ping timeout: 256 seconds]
<promach__>
daveshah: I just got it working
<promach__>
but does yosys allows plotting of genvar with gtkwave yet ? I have passsed in the option "-wire", but I still could not see my genvar wavform in gtkwave
promach__ is now known as promach_
<promach_>
besides, have anyone tried asking the assert() to print out error message if it failed ?
<fsasm>
promach__: AFAIK are genvar evaluated at compile time and they don't change during run time. You most probably need an integer variable.
oldtopman has quit [Ping timeout: 276 seconds]
<promach_>
fsasm: gtkwave does not plot integer
oldtopman has joined #yosys
promach_ has quit [Quit: WeeChat 2.0.1]
<ZipCPU>
promach_: What variables are you trying to show and see?
<ZipCPU>
Forget the loop variable. It doesn't exist. What is it you want to see?
promach_ has joined #yosys
m_t has quit [Quit: Leaving]
m_w has joined #yosys
seldridge has joined #yosys
fsasm has quit [Ping timeout: 256 seconds]
promach_ has quit [Ping timeout: 248 seconds]
pie___ has joined #yosys
pie__ has quit [Ping timeout: 240 seconds]
FabM has quit [Quit: ChatZilla 0.9.93 [Firefox 52.5.0/20171114221957]]
cemerick_ has joined #yosys
cemerick has quit [Ping timeout: 248 seconds]
pie___ is now known as pie_
dys has quit [Ping timeout: 240 seconds]
cemerick has joined #yosys
cemerick_ has quit [Ping timeout: 256 seconds]
sklv has joined #yosys
xrexeon has joined #yosys
<mattvenn_>
hey ZipCPU, do you have a diagram of the zipcpu modules?
<ZipCPU>
Yes, many. What kind of diagram are you looking for.
<ZipCPU>
Just remember the FPU location hasn't been populated yet.
<ZipCPU>
(I haven't gotten around to building it and proving it)
<mattvenn_>
how many luts are you at ATM?
<ZipCPU>
Spartan S6?
<mattvenn_>
ice40?
<ZipCPU>
Ahh, yes ...
<mattvenn_>
not that important for my purposes, so yes spartans6 is fine
<mattvenn_>
I'm trying to give people an overview of fpga usage
<ZipCPU>
So, here's the problem with the question: 1) the CPU can be reconfigured for more or less LUTs, and 2) the CPU doesn't exist in a vacuum. All of the designs I have of the CPU include other components to make a realistic design.
<mattvenn_>
right
<ZipCPU>
However, I have numbers for fairly complete designs if you would like.
<mattvenn_>
yes please
sklv has quit [Remote host closed the connection]
<ZipCPU>
One design I have (icozip) uses 7887 cells on an iCE40, of those 5872 are LUT4's. Another design (tinyzip) uses 5510 cells, and among them 3261 LUT4's.
<mattvenn_>
thanks
xrexeon has quit [Ping timeout: 264 seconds]
sklv has joined #yosys
<ZipCPU>
I'm now working on a newer/better prefetch module as well. This should drop the usage by about 25 or so LUTs, but speed up the CPU by about a factor of more than two.
xrexeon has joined #yosys
<mattvenn_>
wowser
<ZipCPU>
Yeah. I was surprised.
<ZipCPU>
I was going to present my dblfetch prefetch unit, and as I was putting the description together I realized I had made some ... choices that increased usage and decreased performance.
<awygle>
tbh that's one of the best reasons to blog
<ZipCPU>
:D
<awygle>
or just explain things to other people generally
<mattvenn_>
thats what I'm in the process of doing now
<ZipCPU>
Not one I was expecting, but you point is well made.
<mattvenn_>
starting an fpga working group
<awygle>
"So uh... why is this so complicated?"
<awygle>
"... Because I messed up."
<ZipCPU>
awygle: it goes beyond that, though. I wouldn't have realized how complicated it was had I not asked yosys to calculate the module's usage.
<ZipCPU>
Changes to the prefetch and the flash controller brought the performance from 49 clocks per instruction to less than 8 clocks per instruction--when running from QSPI flash.
<cr1901_modern>
Why wouldn't it be 44 CPI (a finally-fetched insn can still go through the pipeline while the CPU reads from flash)?
<cr1901_modern>
Or might be 45 CPI. I can't math today.
<ZipCPU>
cr1901_modern: Yes, exactly. That's part of the discussion and the improvements I intend to present.
<cr1901_modern>
Ahh I see
sklv has quit [Write error: Connection reset by peer]
<awygle>
i had two breakthroughs on my current fpga project last night but couldn't follow through on them before bed. as a result, my actual day job feels incredibly slow...
<ZipCPU>
Sounds exciting.
<awygle>
well it will be, in about 7 hours
jwhitmore_ has joined #yosys
<shapr>
I have that feeling sometimes, I really want to write a tags program that understands C++11 using for typedef
jwhitmore_ has quit [Ping timeout: 264 seconds]
<awygle>
I take the fact that I went to bed instead of staying up to run them down as a sign I'm (finally) maturing as a person
<shapr>
I need to learn that :-(
sklv has joined #yosys
m_t has joined #yosys
TFKyle has quit [Ping timeout: 252 seconds]
TFKyle has joined #yosys
xrexeon has quit [Ping timeout: 240 seconds]
xrexeon has joined #yosys
TFKyle has quit [Ping timeout: 264 seconds]
TFKyle has joined #yosys
jwhitmore_ has joined #yosys
xrexeon has quit [Ping timeout: 264 seconds]
xrexeon has joined #yosys
sklv has quit [Remote host closed the connection]
sklv has joined #yosys
xrexeon has quit [Ping timeout: 264 seconds]
xrexeon has joined #yosys
xrexeon has quit [Max SendQ exceeded]
xrexeon has joined #yosys
xrexeon_ has joined #yosys
xrexeon_ has quit [Max SendQ exceeded]
xrexeon_ has joined #yosys
xrexeon has quit [Ping timeout: 240 seconds]
xrexeon_ has quit [Max SendQ exceeded]
xrexeon_ has joined #yosys
xrexeon_ has quit [Max SendQ exceeded]
xrexeon_ has joined #yosys
xrexeon_ has quit [Max SendQ exceeded]
xrexeon_ has joined #yosys
xrexeon_ has quit [Ping timeout: 264 seconds]
xrexeon_ has joined #yosys
xrexeon_ has quit [Ping timeout: 268 seconds]
xrexeon_ has joined #yosys
dys has joined #yosys
jwhitmore_ has quit [Ping timeout: 256 seconds]
leviathan has quit [Remote host closed the connection]