svenn has quit [Read error: Connection reset by peer]
svenn has joined #yosys
promach__ has joined #yosys
ZipCPU|Laptop has quit [Ping timeout: 240 seconds]
cemerick has joined #yosys
seldridge has quit [Ping timeout: 260 seconds]
promach__ has quit [Ping timeout: 268 seconds]
xrexeon has quit [Ping timeout: 256 seconds]
emeb_mac has joined #yosys
ZipCPU|Laptop has joined #yosys
ZipCPU|Laptop has quit [Quit: Warp drive ready at your command, Captain!]
digshadow has quit [Ping timeout: 276 seconds]
jkiv has joined #yosys
emeb has quit [Quit: Leaving.]
promach_ has joined #yosys
jkiv has quit [Quit: Leaving]
digshadow has joined #yosys
AlexDaniel has quit [Ping timeout: 268 seconds]
promach_ has quit [Quit: WeeChat 2.1-dev]
X-Scale has quit [Read error: Connection reset by peer]
pie___ has joined #yosys
digshadow has quit [Ping timeout: 255 seconds]
cemerick has quit [Ping timeout: 260 seconds]
philtor has quit [Ping timeout: 240 seconds]
philtor has joined #yosys
promach_ has joined #yosys
emeb_mac has quit [Quit: Leaving.]
sklv has quit [Quit: quit]
GuzTech has joined #yosys
pie___ has quit [Read error: Connection reset by peer]
pie_ has joined #yosys
digshadow has joined #yosys
promach_ has quit [Quit: WeeChat 2.1-dev]
promach_ has joined #yosys
svenn_ has joined #yosys
shapr_ has joined #yosys
Max`P has joined #yosys
indy_ has joined #yosys
svenn has quit [*.net *.split]
indy has quit [*.net *.split]
fouric has quit [*.net *.split]
quigonjinn has quit [*.net *.split]
philtor has quit [*.net *.split]
Max-P has quit [*.net *.split]
shapr has quit [*.net *.split]
Max`P is now known as Max-P
philtor has joined #yosys
promach_ has quit [Quit: WeeChat 2.1-dev]
fouric has joined #yosys
leviathan has joined #yosys
eduardo_ has joined #yosys
eduardo__ has quit [Ping timeout: 264 seconds]
indy_ is now known as indy
indy has quit [Read error: Connection reset by peer]
indy has joined #yosys
proteusguy has quit [Ping timeout: 256 seconds]
xrexeon has joined #yosys
maartenBE has quit [Ping timeout: 264 seconds]
cemerick has joined #yosys
maartenBE has joined #yosys
leviathan has quit [Remote host closed the connection]
leviathan has joined #yosys
cemerick_ has joined #yosys
cemerick has quit [Ping timeout: 240 seconds]
seldridge has joined #yosys
pie_ has quit [Read error: Connection reset by peer]
<cr1901_modern>
ZipCPU: The TLDR to where I'm stuck is basically "verifying a design for a parametric module w/ arbitrary value for the parameter". I don't have time right now to go into detail, but >>
<cr1901_modern>
(emphasis on _I believe is analogous_. When I have more time I could come up with a minimal example and corresponding visual aid lol.)
<ZipCPU>
cr1901_modern: I haven't gotten there yet, but I do know Clifford's solution which I intend to apply soon.
<ZipCPU>
Clifford's solution is based around "task"s within SymbiYosys.
<ZipCPU>
You can create a SymbiYosys file that sets parameters to a particular solution, and then split that file further into "tasks"--each of which sets the parameter values to a different value.
<ZipCPU>
I've also used a different approach for my multiply: I've created an abstract multiply that returns a result in 1-8 clocks. (My true multiply returns a result in 1, 2, 3, or 4 clocks--never changing)
<ZipCPU>
By using this abstract multiply, I can prove that *all* of the parameter based multiplies will work.
<ZipCPU>
(Incidentally, the result of the abstract multiply is ... random--part of the abstraction)
* cr1901_modern
is trying to remember how to code verilog... please stand by
<cr1901_modern>
I thought you could only do that with, well, parameters
<ZipCPU>
No, it's not possible. Let me clarify:
<ZipCPU>
wire [5:0] width = $anyconst; wire [63:0] my_wire; // is possible however.
<ZipCPU>
Then, you can choose to only pay attention to the lower width bits of my_wire.
<cr1901_modern>
Hmmm...
* cr1901_modern
is thinking
<cr1901_modern>
I'm guessing cover can't be used w/ induction
<ZipCPU>
Sigh. No, it cannot.
<ZipCPU>
However, you could do the assertion: "assert(!|my_wire[63:width] || ov);"
<ZipCPU>
That'd pass induction nicely.
<cr1901_modern>
>Then, you can choose to only pay attention to the lower width bits of my_wire.
<cr1901_modern>
Did you mean higher width bits?
<cr1901_modern>
B/c that's what that assert does afaik- only considers the higher width bits
<ZipCPU>
No, I meant lower bits when I said it, the higher bits idea was only a more recent one.
<cr1901_modern>
ZipCPU: Oh sorry, I can't do OR to save my life
<cr1901_modern>
!| == "if any of the bits are 1, the whole expression is 0"?
<ZipCPU>
That's what I meant, yes.
<ZipCPU>
I haven't actually tried that expression through a Verilog parser to know that it works though ....
<cr1901_modern>
Okay, this approach assumes you've put an upper limit to the counter width you want to check. What I had intended to check for in my counter example w/ the parameter was:
<cr1901_modern>
No upper limit. Prove for finite-"n"
<ZipCPU>
Yeah ... I'm not sure how to do that.
<cr1901_modern>
counter could be 1 bit, 64 bits, 1024 bits, 65536 bits
<ZipCPU>
For a fixed counter, it's easy.
<cr1901_modern>
We both know that no matter how big the counter is, it will eventually overflow for all finite values of parameter "width"
<ZipCPU>
Yeah, but the proof for 65536 bits isn't trivial. :P
<cr1901_modern>
I simply wonder if there is a way to express this without e.g. actually having to check the 65536 bit proof
<ZipCPU>
At this point in our discussion, I do not know of a way. I know of a way to check counters of width 1-N, for fixed N, but not 1-infinity.
<cr1901_modern>
ZipCPU: Well, I need some time to think before we continue (I understand the convo isn't done- you were about to discuss abstractions). Is that okay?
<ZipCPU>
Well, okay, sure, let's move on to abstractions then.
<ZipCPU>
The idea behind abstractions is that if you can prove "A -> B", then it must also be true that "(AC) -> B"
<ZipCPU>
I would need to use abstractions to cover your 65536 bit case, otherwise cover (which must start at init, as currently written) would never get there.
<ZipCPU>
To do that, we make an abstract counter instead, and then step by an amount chosen by the formal solver subject to your constraints.
<ZipCPU>
The abstract counter doesn't step by one, in other words, but it might step by one.
<ZipCPU>
Hence, the case that you are interested in is one of many cases described by the abstraction.
<ZipCPU>
If the formal properties you choose still succeed, then you know they will succeed even if the counter only steps by one.
seldridge has quit [Ping timeout: 255 seconds]
<cr1901_modern>
Hmmm
<ZipCPU>
Hence, if "(counter monotonically increases) -> B" is true, then so also must be if "(counter increments by one) -> B"
<ZipCPU>
On the other hand, it might be true that "(counter monotonically increases)" doesn't imply B, but "(counter increments by one)" does.
<ZipCPU>
In other words, if "A -> B" is false, it might still be true that "(AC)->B". So failing to prove "A -> B" (the abstract version) doesn't really tell you that "(AC)-> B" will fail to prove as well.
cemerick_ has joined #yosys
* cr1901_modern
is plugging "(A -> B) -> ((AC) -> B)" into z3
<cr1901_modern>
so (counter monotonically increases) is "A" in your example and (counter increments by one), being more specific is "(AC)" in your example?
<ZipCPU>
Yes
proteusguy has joined #yosys
AlexDaniel has joined #yosys
<cr1901_modern>
This is really weird (and profound), and messing w/ my head
shapr_ is now known as shapr
shapr has quit [Changing host]
shapr has joined #yosys
<ZipCPU>
Would you like me to share an example that I'm currently using?
<cr1901_modern>
Not right now, I would prefer to struggle/sit on this some more if that's okay :)
cr1901_modern has quit [Read error: Connection reset by peer]
cemerick_ has quit [Read error: Connection reset by peer]
<ZipCPU>
Ok, I'll post it to my dev branch of the ZipCPU then if anyone else requests it.
cr1901_modern has joined #yosys
cemerick_ has joined #yosys
promach__ has joined #yosys
<cr1901_modern>
It seems like to take advantage of "(A -> B) -> ((AC) -> B)", you not only have to prove "A" holds, but also that "AC" holds
quigonjinn has joined #yosys
<cr1901_modern>
ZipCPU: I have to go right, now. Would you be willing to paste a link to your example?
<ZipCPU>
Exactly. However, I think the formalism is getting to you. My formal proof is going the other way.
<ZipCPU>
Ok, sure, I'll paste the link ... one moment ....
<cr1901_modern>
(Well I assume proving "A -> C" is enough to show that "AC" holds)
<ZipCPU>
True.
<ZipCPU>
Ahh, sorry about my criticism starting with "Exactly. However, ..." ... looking over it again, I think you got it right.
* ZipCPU
is reminded never to do (predicate) math in public ...
<cr1901_modern>
No worries, I didn't even notice what you meant the first readthru :P
<cr1901_modern>
The reason I bring that up is because you could choose a "C" that has no relation to the truth value of "A" whatsoever and make "(A -> B) -> ((AC) -> B)" hold.
<cr1901_modern>
But choosing a "C" that's not derived from "A" is useless for the proof I want to do
<ZipCPU>
Not quite. In the example I gave of (counter is monotincally increasing), (counter increments by one) was not derived from "A"
<cr1901_modern>
(Perhapos I meant you need to show C -> A
<ZipCPU>
Ok, that makes sense.
<ZipCPU>
I like to think of C as a subset of A, but in predicate math C -> A might be just as equivalent.
<cr1901_modern>
e.g. A = (counter is monotincally increasing) and C = (true) satisfies "(A -> B) -> ((AC) -> B)"
<cr1901_modern>
err, crap
<cr1901_modern>
I'm gonna stop while I'm ahead and think more
<cr1901_modern>
tyvm, I'll take a look when I have more time :)
* cr1901_modern
splits for a bit
<cr1901_modern>
thanks for the help as always
<awygle>
I never thought of using $anyconst like that! Great idea
maartenBE has quit [Ping timeout: 260 seconds]
seldridge has joined #yosys
maartenBE has joined #yosys
seldridge has quit [Ping timeout: 240 seconds]
maartenBE has quit [Ping timeout: 265 seconds]
maartenBE has joined #yosys
<keesj>
do you guys also use gtkwave for looking at change value dumps or are you using..somethine else?
<ZipCPU>
I personally use gtkwave all over the place.
GuzTech has quit [Quit: Leaving]
<awygle>
I use gtkwave but I'm sad about it
cemerick_ is now known as cemerick
promach__ has quit [Ping timeout: 260 seconds]
emeb has joined #yosys
AlexDani` has joined #yosys
AlexDaniel has quit [Ping timeout: 255 seconds]
cr1901_modern1 has joined #yosys
cr1901_modern has quit [Ping timeout: 240 seconds]
cr1901_modern1 has quit [Read error: Connection reset by peer]
cr1901_modern has joined #yosys
digshadow has quit [Ping timeout: 240 seconds]
sklv has joined #yosys
seldridge has joined #yosys
digshadow has joined #yosys
GuzTech has joined #yosys
seldridge has quit [Ping timeout: 255 seconds]
cemerick_ has joined #yosys
cemerick has quit [Ping timeout: 255 seconds]
<keesj>
awygle: why?
<keesj>
I have some asserts in my test code (and quite happy about it) but do use gtkwave to view stuff. There are small things I would like changed (and like sigrok's puslveview ) would like logic analysers
<keesj>
(but sigrok/pulseview currently are not ... 100% ready for handling many singals)
<keesj>
and ... just out of curiosity... what do you use when it does not work on the "real" hardware?
<awygle>
keesj: it's not well integrated on windows, the UI is unintuitive, and it doesn't support real time streaming afaict
<awygle>
on real hardware I currently use vendor tools, but hope to develop a suite of tools along the lines of what ZipCPU discussed on his blog in the future
seldridge has joined #yosys
<ravenexp>
what's wrong with good old procedural testbenches?
<ravenexp>
it's been quite a while since I've last stared on the marching waves
<keesj>
I have only limited experience but on the papilio pro I used sump / ols (e.g. http://papilio.cc/ only 32 channels and 200Mhz ) but did get the job done) but it did not feel a professional as some vendor tools
<awygle>
I am astonished that no one has yet implemented a live debugger for FPGAs
<ravenexp>
does chipscope count as a live debugger?
<ravenexp>
not to speak of the soft cpu trace ports
<keesj>
ravenexp: what do you mean by procedural testbenches?
<awygle>
ravenexp: can you single step the clock? Can you modify the HDL on the fly?
<awygle>
(no and no)
<ravenexp>
I can't thing of why it would be a good idea to single step an fpga
<keesj>
I mean: testing works fine .. but ... what do you do when it does not
<ravenexp>
keesj: I stop and think about my tests
<ravenexp>
then I fix them and it works both in tests and on the live hw
<awygle>
Granted something like that is more often useful in a simulator but it doesn't exist even there
<awygle>
I want to step through my state machines and figure out why the valid signal is getting asserted one cycle before the data is actually valid
cemerick has joined #yosys
<ravenexp>
you can do that in like 10 lines of verilog
<awygle>
But every time I bring this up I get the same "just be perfect" response, so... *shrug*
<ravenexp>
and one you've written this test, it stays there
<ravenexp>
so you won't ever regress on it
<awygle>
you can verify correctness in 10 lines, but determining the cause of incorrectness is still done with very blunt tools
<ravenexp>
many small module-level tests are way better at catching logic errors than whole system debuggers could ever be
<awygle>
FPGA debugging sucks primarily because of how comically long the feedback loops are
<awygle>
why not both?
<ravenexp>
pls, some people do asics
<keesj>
well. I think I have written decent tests and (this is my first real project) and I felt happy about it. I even had some kind of confidence. building up tests and seeing it pass was awesome. using gtkwave was only a basic .. visualisation but I needed real... failing? tests
<awygle>
I imagine Asic debugging sucks worse. Doesn't mean fpga debugging doesn't suck.
cemerick_ has quit [Ping timeout: 255 seconds]
<ravenexp>
complaining about fpga loopback cycles is somehat...
<keesj>
but I feel there is still a distance between that and .. the real thing
<ravenexp>
keesj: I use verilog models for things both inside and outside the fpga
<keesj>
because of bad simulation?
<ravenexp>
you can do board level debugging before you can even get your hands on the real hw
<ravenexp>
when I was an fpga noob I used chipscope and real logic analyzers a lot
<ravenexp>
nowadays I mostly do "make ; make program" and things just work...
* keesj
did use a real logic analyzer today
<ravenexp>
you can't do CI with people with logic analyzers
<ravenexp>
with good test suites you actually can
GuzTech_ has joined #yosys
GuzTech has quit [Ping timeout: 255 seconds]
jkiv has joined #yosys
seldridge has quit [Ping timeout: 256 seconds]
GuzTech_ has quit [Read error: Connection timed out]
GuzTech_ has joined #yosys
seldridge has joined #yosys
dys has joined #yosys
GuzTech__ has joined #yosys
GuzTech_ has quit [Ping timeout: 265 seconds]
<keesj>
are there travis/github type hosted CI projects I might want to look into ?
<keesj>
(example stuff)
<ZipCPU>
What sort of stuff are you looking for?
cemerick_ has joined #yosys
cemerick has quit [Ping timeout: 265 seconds]
<ZipCPU>
awygle: I've single stepped my FPGA designs before.
<ZipCPU>
It's not all that hard to do, but you do need to plan to be able to do so from the beginning.
<ZipCPU>
Further, I think a lot of ASIC engineers single-step their designs once the ASIC comes back from the fab--usually they have a logic chain of some type (can't remember the name off the top of my head) that allows them to see everything and then step everything.
<keesj>
ZipCPU: I don't really know what I am looking for sorry, I guess information on how others deal with this type of issues and good examples
<keesj>
(but ... I won't start doing it today so mostly out of interest)
<ZipCPU>
I have a lot of example designs at https://github.com/ZipCPU feel free to browse and then come back with questions if you would like.
<sorear>
those are called scan chains, and they are primarily used to test the chip as manufactured against the netlist, not for finding new problems in the netlist
<ZipCPU>
Ahh ... that's the word I was looking for. Thank you, sorear! Thank you for the clarification as well.
<awygle>
ZipCPU: yes, it doesn't seem difficult, but it's very uncommon. and even when it is done, the surrounding tooling doesn't support it well (most vcd renderers won't do live update for example)
<ZipCPU>
That makes sense. When I did it last, I used a WB bus to read the internal state back off of the device, and then dumped the data into a file I could read and process using Octave.
<ZipCPU>
It worked really well when stepping through signal processing algorithms
<ZipCPU>
Indeed, I never used any simulation on that project at all--it was all HITL testing.
Kensan has joined #yosys
milkii has joined #yosys
jkiv has quit [Ping timeout: 256 seconds]
cemerick_ is now known as cemerick
jkiv has joined #yosys
leviathan has quit [Remote host closed the connection]