<phire>
hmm, the splice pass appears to miss some multi-bit signals
philtor has quit [Remote host closed the connection]
philtor has joined #yosys
digshadow has quit [Ping timeout: 248 seconds]
<phire>
if I haven't specified any selection, does that mean all cells/wires are selected?
<ZipCPU>
?
<ZipCPU>
phire: Can you share more of what you are doing?
<phire>
I've written a hacky prototype which takes json output from yosys and generates c++ code
<phire>
along the same lines of verilator, except its ~500 lines of python
<phire>
so I've got a synthisis script which flatterns, optimises, pmuxtrees, wreduces before using splice to generate explicit $slice and $concat nodes
<ZipCPU>
Wow. That does sound rather hacky.
<ZipCPU>
What are you trying to accomplish?
<phire>
I want to be able to write emulators in HDL
<ZipCPU>
Impressive.
<phire>
I got a little annoyed writing emulators in procedural languages
<ZipCPU>
And ... it turns the results into C++ or python? I think you said C++, right?
<ravenexp>
what's wrong with verilator?
<phire>
python script which generates c++
<phire>
ravenexp, I found it too slow and wanted to drop some fundamental functionality to get faster results
AlexDaniel has quit [Remote host closed the connection]
<phire>
also, sometimes I find the best way to lean a new domain is to try and implement it myself
<ZipCPU>
Hmm ... I think Verilator's output is more readable. ;) Still, it looks like you've got a nice start.
<phire>
oh yeah, verilator output is more readable and probably faster.
<phire>
the key is that was generated with a short yosys synthesis script and 500 lines of python.
<phire>
anyway, I think I've traced my current bug down to the fact that the output of splice still has unspliced wires.
<phire>
and I'm trying to work out why
pie__ is now known as pie_
pie__ has joined #yosys
pie_ has quit [Ping timeout: 268 seconds]
<ZipCPU>
:)
<phire>
oh, some are caused by insufficient wreducing
<phire>
a loop of wreduce; opt; catches things that a single wreduce doesn't
pie__ is now known as pie_
digshadow has joined #yosys
digshadow has quit [Ping timeout: 268 seconds]
<phire>
ah, splitnets -driver is important to split up buses which are only partially driven
<phire>
that gets rid of all the missing $concats
<phire>
well, most of them
digshadow has joined #yosys
sklv has quit [Quit: quit]
nrossi has joined #yosys
dys has quit [Ping timeout: 240 seconds]
eduardo__ has joined #yosys
eduardo_ has quit [Ping timeout: 240 seconds]
AlexDaniel has quit [Ping timeout: 256 seconds]
m_t has joined #yosys
leviathanch has joined #yosys
pie_ has quit [Ping timeout: 240 seconds]
proteusguy has quit [Remote host closed the connection]
proteusguy has joined #yosys
dys has joined #yosys
leviathanch has quit [Remote host closed the connection]
AlexDaniel has joined #yosys
AlexDaniel has quit [Read error: Connection reset by peer]
sklv has joined #yosys
AlexDaniel has joined #yosys
leviathanch has joined #yosys
leviathanch has quit [Read error: Connection reset by peer]
leviathanch has joined #yosys
sklv has quit [Quit: quit]
sklv has joined #yosys
<ZipCPU>
cr1901_modern: I listened to a talk by Clifford the other day which did a better job of discussing how to simplify the proof of an entire system.
<ZipCPU>
Remember the other day when we were trying to figure out how to solve a proof in parts?
<ZipCPU>
Imagine this, suppose you had a property that said if (A is a prime) then B must be true.
<ZipCPU>
If you instead proved that if (A==2) then B, and if (A is odd) then B, you would then know that if (A is prime) then B.
gnufan has quit [Ping timeout: 265 seconds]
m_t has quit [Quit: Leaving]
gnufan has joined #yosys
gnufan has quit [Ping timeout: 268 seconds]
<ZipCPU>
Formally, if you prove: if (A) then C, then you know that it will also be true that, if (AB) then C
gnufan has joined #yosys
<cr1901_modern>
ZipCPU: Noted, and I won't have time to really parse what you say until later, but: that z3 example I did really bothered me.
gnufan has quit [Ping timeout: 260 seconds]
gnufan has joined #yosys
gnufan has quit [Ping timeout: 240 seconds]
gnufan has joined #yosys
gnufan has quit [Ping timeout: 276 seconds]
gnufan has joined #yosys
sklv has quit [Remote host closed the connection]
sklv1 has joined #yosys
pie_ has joined #yosys
gnufan has quit [Ping timeout: 240 seconds]
gnufan has joined #yosys
leviathanch has quit [Read error: Connection reset by peer]
m_t has joined #yosys
nrossi has quit [Quit: Connection closed for inactivity]
sklv1 has quit [Remote host closed the connection]