<Wolong>
Hello, I recently started learning nmigen. I got an error when installing nmigen according to the document here.:http://blog.lambdaconcept.com/doku.php?id=nmigen:nmigen_installThe error message is shown in the figure below. Will this affect my normal use of nmigen?
<Wolong>
Hello, I recently started learning nmigen. I got an error when installing nmigen according to the document here:http://blog.lambdaconcept.com/doku.php?id=nmigen:nmigen_install
<_whitenotifier-f>
[nmigen] Xiretza opened pull request #506: hdl.ir: Update error message for Instance arguments - https://git.io/JTZD5
jeanthom has quit [Ping timeout: 264 seconds]
<awygle>
whitequark: do you wanna talk about platforms here, the questionably-relevant github issue, or the relevant-but-very-old github issue?
<whitequark>
awygle: hmm
<whitequark>
either works, let's start with platforms because people are really persistent about them, which means there's a significant need for improvement
<awygle>
(also, do you want to discuss it now, after you've kept your house from burning down, or at the meeting next week)
<whitequark>
lol
<whitequark>
let's push it to the meeting
<awygle>
mkay
<awygle>
real quick tho, i now think i understand your concerns about defining how such a platform would work. do you feel like you understand why people keep asking for sim/formal platforms? you are giving a slight "why do people want this" vibe, similar to the Array stuff
<whitequark>
no, i don't, that would be the first step
<whitequark>
figure out what people actually want when they say they want a sim/formal platform
<awygle>
well that's a slightly different thing
<awygle>
"why do they ask" and "what do they want" are related but distinct
<whitequark>
"why do they ask" because there's something nmigen doesn't do well, that much is clear
<_whitenotifier-f>
[nmigen] whitequark commented on pull request #506: hdl.ir: Update error message for Instance arguments - https://git.io/JTZ7n
<FL4SHK>
seems I misunderstood `word_select`
<FL4SHK>
I was doing the multiplication in advance!
<FL4SHK>
It acts just like Verilog `+:`
<FL4SHK>
I was treating things more like VHDL
<FL4SHK>
*now* my long divider works
<FL4SHK>
now exhaustively testing a 16/10=16 divider
<FL4SHK>
won't take that long
<FL4SHK>
so far results are good
<FL4SHK>
I suspect that since it worked for smaller stuff it'll "just work" for bigger stuff
<FL4SHK>
*not* sure whether I should pipeline it
<FL4SHK>
I lean towards not doing that since I need to include a lot of these
<lkcl>
FL4SHK: nice
<lkcl>
we didn't take any chances with the DIV unit, created a massive suite of unit tests covering corner-cases.
<lkcl>
if you're doing a formal correctness proof - and get it right - you should be fine
<FL4SHK>
I'm surprised that this is going so quickly...
<FL4SHK>
so I think my divider is not bugged, but rather my formal stuff is
<FL4SHK>
I really don't think this should be finishing so quickly?
<FL4SHK>
I think I see
emeb_mac has joined #nmigen
<whitequark>
formal verification mostly shines when you verify *multiple things*
<whitequark>
if you just verify one, you're as likely to have bugs in your spec as in your design
<awygle>
on the other hand, at least you don't have to write tests
<awygle>
(ok you still do, let me dream...)
<whitequark>
yeah
chipmuenk has quit [Quit: chipmuenk]
chipmuenk has joined #nmigen
Asu has quit [Remote host closed the connection]
chipmuenk has quit [Client Quit]
<lkcl>
FL4SHK: so what whitequark is saying is: that if we (libre-soc team) use your formal proof and test *our* DIV engine...
<lkcl>
basically, as the author of both your own code *and* the formal correctness proof, you have no idea if both are correct, or both are wrong.
<lkcl>
i.e. the proof could be 100% verifying - correctly - that the *implementation* is producing wrong divide answers.
<whitequark>
it's not just that, though it's that too
<whitequark>
it's also omissions in the proof
* lkcl
interested to know the other things
<lkcl>
ah yeah
<whitequark>
formal verification is most powerful when you write a proof against multiple existing designs
<whitequark>
like it happened with riscv-formal
<whitequark>
it also works reasonably well if you're verifying several generations of a single design
<whitequark>
but for one-offs it's not all that better than tests IMO
danfoster has joined #nmigen
<lkcl>
well, ALUs are a little different we've found
<lkcl>
however for POWER9 multiply pipeline, the code written for the formal test is.. er... a leeetle bit too much like the actual implementation
<lkcl>
but in other areas it's been incredibly useful.
<lkcl>
we have complex optimised algorithms (recursive trees) that are hard to understand
<lkcl>
but the core algorithm behind the proof is err... 3 lines (just horribly inefficient if put into silicon)
emeb has quit [Quit: Leaving.]
<lkcl>
i can't explain how the "optimised" algorithm works... but because the proof says "it's equivalent", i don't care! :)
<whitequark>
oh yeah, it makes sense to distinguish equivalence proofs and behavioral proofs
<whitequark>
if you can implement what you want in a simpler but inefficient way it often pays off to prove the equivalence of the complex thing with that
<whitequark>
but if you're just stating properties it can be a lot harder