cr1901_modern has quit [Read error: Connection reset by peer]
Degi has quit [Ping timeout: 260 seconds]
Degi has joined #nmigen
XgF has joined #nmigen
cr1901_modern has joined #nmigen
<ktemkin>
I don't know why I never thought of this before -- probably because it's incredibly cursed -- but creating module-level Signals is a really easy way to yoink a signal from like seven levels deep so you can shove it into an ILA
<ktemkin>
it is the worst and I hate it and it's probably the least keystrokes to getting quick debug output I've found
electronic_eel has quit [Ping timeout: 272 seconds]
electronic_eel has joined #nmigen
PyroPeter_ has joined #nmigen
PyroPeter has quit [Ping timeout: 260 seconds]
PyroPeter_ is now known as PyroPeter
futarisIRCcloud has quit [Quit: Connection closed for inactivity]
peeps[zen] has joined #nmigen
peepsalot has quit [Ping timeout: 264 seconds]
peeps[zen] is now known as peepsalot
hitomi2509 has joined #nmigen
emeb_mac has quit [Quit: Leaving.]
jeanthom has joined #nmigen
<ktemkin>
re-reading the backlog, I realize I should say Python-module-level
<ktemkin>
words have more than one meaning, it turns out
<lkcl>
whitequark, ktemkin: we have someone else interested in learning nmigen and HDL, i am referring people to robert baruch's tutorial for now, is there anything better available? (happy to link to "planned" tutorials as well)
<whitequark>
robert baruch's tutorial is a bit of a middle ground between a tutorial and a reference
<whitequark>
the tutorial parts are reasonable but the reference parts have a few significant inaccuracies
<Lofty>
The "Global FPGA Clocks" section describes five different clock frequencies
<Lofty>
On the plus side Quartus says I can run attosoc at 350 MHz
<Lofty>
For blinky turbo mode
<FL4SHK>
seems I'm able to formally verify my long divider!
<FL4SHK>
I messed up; I can actually use the yosys `/` operator
<FL4SHK>
my Python source code used `/` instead of `//`
<daveshah>
how long does the verification take, out of curiosity?
<FL4SHK>
I don't know yet
<FL4SHK>
I haven't finished writing it up
<daveshah>
oic
<FL4SHK>
I intend on verifying only a small divider
<FL4SHK>
I actually know that the thing is bugged
<FL4SHK>
I don't currently know why it's bugged
<FL4SHK>
when doing `m.Case(x)`, does `x` act like a normal python thing?
<FL4SHK>
wait, my `x` has don't cares in it
<FL4SHK>
"001", "01-", and "1--" for a 3-bit `x` in `m.Switch(x)`
<FL4SHK>
I think it's only `Cat` that's backwards from normal
<FL4SHK>
(though it being backwards finally makes sense to me)
<FL4SHK>
question about `word_select`
<lkcl>
daveshah: we've found that as long as you don't have shift or multiply operations in the proof, yosys completes within under 60 seconds
<FL4SHK>
I want to do `item[i * WIDTH +: WIDTH]`
<FL4SHK>
so do I do `item.word_select(i, WIDTH)` in nMigen?
<lkcl>
FL4SHK, that would be ... yes
<lkcl>
that's all you need :)
<FL4SHK>
cool, then that's not the source of the bug
<lkcl>
oh wait hand on
<lkcl>
that's item[i*width: (i+1)*width]
<daveshah>
lkcl: yeah, I am curious how divides behave performance wise
<daveshah>
I imagine they will have the same problem as multiplies
<lkcl>
if you genuinely want :width then you'll need to do it by masking and manual shifting
<FL4SHK>
Maybe I'm remembering wrongly
<FL4SHK>
no
<FL4SHK>
I used Verilog syntax
<FL4SHK>
notice the `+:`
<FL4SHK>
what I want is `item[i * WIDTH +: WIDTH]`
<lkcl>
daveshah: we've deliberately never tried to use nmigen (yosys) divide operator
<lkcl>
FL4SHK: ah you should have said - this is a python/nmigen channel :)
<FL4SHK>
You missed the `+`
<lkcl>
daveshah: so if you do a divider as "the usual iterative shift plus add" then aside from it being "multiple iterations" it should be pretty quick
<FL4SHK>
but okay
<FL4SHK>
I'm not doing shift and subtract here
<FL4SHK>
well
<FL4SHK>
there are shifts and subtracts...
<lkcl>
FL4SHK: i've never seen / used that syntax. however if it's what i think it is, then item.word_select(i, WIDTH) should be good
<FL4SHK>
I didn't implement binary long division
<FL4SHK>
I implement radix-k long division
<lkcl>
FL4SHK: we implemented... yes, we did a radix-k
<FL4SHK>
such that you provide a generic to say how many bits to compute in a clock cycle
<whitequark>
14:20 < FL4SHK> I want to do `item[i * WIDTH +: WIDTH]`
<whitequark>
14:20 < FL4SHK> so do I do `item.word_select(i, WIDTH)` in nMigen?
<whitequark>
yes.
<lkcl>
it was implemented by Jacob.
<FL4SHK>
thanks whitequark
<lkcl>
he also included radix-k square-root and reciprocal-square-root because it's essentially the same hardware
<whitequark>
that's an explanation in terms of Python; I'll write one in terms of Verilog later
<lkcl>
you end up with something like a 30-40% saving in gates/LUT4s when compared to separate radix-k div, separate radix-k sqrt and separate radix-k rsqrt
hitomi2509 has quit [Quit: Nettalk6 - www.ntalk.de]
<cr1901_modern>
whitequark: For assertFormal/FHDLTestCase... what specifically do you dislike about both as they exist right now such that they're only good for tests and not exposing it to user code?
<whitequark>
cr1901_modern: well, there's a hardcoded script, which uses a nonstandard mode that no one else uses
<cr1901_modern>
Yea, a lot appears to have changed since mid-2019. Looks like FHDLTestCase got exposed to user code (wasn't it originall internal only?), and is now deprecated (i.e. going back to internal mode)
<whitequark>
it was exposed completely accidentally
<whitequark>
this was the case since the 0.1 release, iirc
<whitequark>
there's been no actual chances besides excluding it from release packages
<cr1901_modern>
Anyways I'm playing w/ it now, and my intent at the meeting next week was to come up with a proof-of-concept for running formal scripts. But assertFormal... looks fine? (s/hybrid/prove/ for my purposes)
<cr1901_modern>
Like I don't see what's exceptionally wrong w/ it that you dislike it so much
<whitequark>
that it was not intended to be a public API is enough
<whitequark>
there's no other justification necessary to prevent it from being exposed
<whitequark>
if i change it later i do not want to worry about the consumers who are relyong on it
<whitequark>
*relying
<whitequark>
it doesn't even matter whether it's well-designed or not (though as a matter of fact it isn't)
<cr1901_modern>
Right. That's not what I'm asking.
<cr1901_modern>
>though as a matter of fact it isn't <-- that's what I'm asking.
<cr1901_modern>
why do you think it's not well-designed?
<whitequark>
well, i just told you? it doesn't let you customize a script and it has the weird "hybrid" mode that people probably shouldn't use
<cr1901_modern>
besides the hybrid part
<whitequark>
but more importantly, it's not even clear if assertFormal is the right thing to do here
<whitequark>
it has the platform="formal" hack which predates build.plat iirc
<whitequark>
should we just strip assertions if building for a non-formal platform? i don't know. maybe that's a good solution
<whitequark>
if i don't know that it's a good idea, then by default i treat it as something that isn't
<cr1901_modern>
To recap: last time we talked about this, you said you wanted a Transformer pass to potentially deal with opt_clean bugs when assume/asserts are stripped
<whitequark>
uh, opt_clean bugs?
<whitequark>
i don't have the context for that but opt_clean bugs should be just fixed upstream
<cr1901_modern>
That's the notes I wrote down :P
<whitequark>
that sounds like a miscommunication
<whitequark>
the problem is that synthesizers don't deal with assume/assert
<whitequark>
which is actually a shame--they *could* rely on them to improve QoS
<whitequark>
it's not clear whether a transformer pass is a good idea either
<whitequark>
nmigen elaboration isn't the fastest, and the best way to improve it is to not create things that will just be ripped off immediately after
<whitequark>
so a new platform property might be a better idea. replace `if platform == "formal":` with something like `if platform.has_assertions:`
<cr1901_modern>
Yup, I remember you saying that too :). The platform == "formal" hack does what you want, but it's a hack. Do you have any idea what such- aaand you just answered my q
<whitequark>
the entire scope of formal verification in nmigen at the moment is "it can generate verilog or rtlil with assert/assume statements"
<whitequark>
i do not, at the moment, provide anything beyond that, and doing it requires thinking first and coding second
<cr1901_modern>
I can copy FHDLTestCase for now. The main benefit for me rn is essentially "no intermediate files generated via python subprocess". But if there was a better way to do it that's also easy, might as well discuss.
<cr1901_modern>
If not, again, I'll just copy FHDLTestCase, make my changes, and call it a day
<whitequark>
can you explain re: immediate files?
<whitequark>
*intermediate files
<whitequark>
is it just that RTLIL is inlined into a script?
<cr1901_modern>
Well that, and the sby file comes from stdin
<cr1901_modern>
sby itself still requiresa work directory too; sometimes I think it would be nice to use a TempDir context manager for that
<Degi>
How can I best find an input name from its datasheet name of an instance? For example I have a DCUA in an ECP5 with a tx_div2_mode input, but i_CHx_tx_div2_mode doesnt work
<FL4SHK>
it was strange enough that `loc.gt_vec` never showed up in the VCD
<FL4SHK>
but when I remove these `Assume` lines, it doesn't even pass the base case
<FL4SHK>
the `loc.temp_denom_mult_lut_X` signals are *only* Assumed
<FL4SHK>
they are never read anywhere in this code
<FL4SHK>
whitequark: ^
<FL4SHK>
the `loc.denom_mult_lut` array also doesn't seem to be included in the VCD's list of signals
<FL4SHK>
this explains why I was having so many issues, I think
<whitequark>
that's pretty lengthy and a bit hard to read, not being formatted to PEP8; if you extract an MCVE from it i'll be able to take a look right away, but otherwise i can't do it at the moment
<FL4SHK>
not formatted to PE8?
<FL4SHK>
what do you mean?
<whitequark>
https://pep8.org/, mostly i just mean 8-wide tabs and unusual style
<whitequark>
which isn't a problem per se, but it is a problem for me when i'm reading unfamiliar code looking for something subtle
<FL4SHK>
I didn't use 8-wide tabs, just 4-wide ones
<FL4SHK>
github displays tabs as 8 spaces
<whitequark>
eh, i don't want to start a formatting holy war. i'm just saying that it's hard for me to navigate your code so i'd appreciate if you minimized the testcase
<whitequark>
formal has enough subtleties on its own
<FL4SHK>
it's not a bug I've run into before
<whitequark>
i've seen some strange behavior with sby that i don't entirely understand
<whitequark>
well, back then i had no idea how SMT solvers worked, so now i'm more equipped to use it
<whitequark>
but my overall impression is that Yosys formal is not yet at the stage where you can use it as a complete black box, and some digging in the internals is basically required
<FL4SHK>
My question is why signals would mysteriously disappear
<whitequark>
ah, that's easier to answer, let me see
<whitequark>
so you never assign to loc.gt_vec and it disappears, right?
<FL4SHK>
No, I assign to `loc.gt_vec`
<FL4SHK>
via `m.d.comb +=`
<whitequark>
ah yes
<whitequark>
okay, I think you'll have to minimize that
<FL4SHK>
I don't like that
<FL4SHK>
it'll slow down my implementation
<whitequark>
can you post the RTLIL?
<whitequark>
err
<whitequark>
sorry, by "minimize" I mean "minimize the problematic case"
<FL4SHK>
ah
<whitequark>
your code seems fine to me, at least it should not lead to disappearing signals
<whitequark>
this could happen if you never assign to one for complex reasons, but you do assign
<whitequark>
so it's an issue elsewhere in the toolchain
<FL4SHK>
I've been meaning to change some of my coding style in general
<FL4SHK>
so I'll adopt PEP8
<FL4SHK>
at least for Python
<FL4SHK>
is it `model/design.il`?
<whitequark>
PEP8 says use 4 spaces, nMigen normally places += [ on the same line as m.d.<domain>, other than that i think your code is reasonable
<FL4SHK>
oh, really?
<whitequark>
not sure about all the #-------- but that seems like a matter of preference
<whitequark>
which part?
<FL4SHK>
for the RTLIL
<whitequark>
sorry, I'm confused
<FL4SHK>
okay so
<FL4SHK>
I am looking for the RTLIL
<whitequark>
oh yeah, what are you using to run your formal cases?
<awygle>
that's where 99% of my unicode knowledge comes from (the last 1% is a computerphile video)
<d1b2>
<DX-MON> even better, whitequark.. in the strict UTF-8 specs, having a UTF-8 encoded UTF-16 BOM is actually even illegal
<lkcl>
alanvgreen: glad to help. honestly you'll get much better stability and flexibility out of nmigen, and if you want to run commercial synthesis / verification tools, "just to be sure / safe" then well you just import the verilog into them.
<whitequark>
FL4SHK: okay, i think you're hitting a yosys issue
<awygle>
i agree that FHDLTestCase isn't great as it stands (at a minimum you need to be able to specify the mode). as for what should be done with assertions in non-formal contexts, i'd like to see (the moral equivalent of) platform.has_assertions in concert with a pysim/cxxsim platform so that we can check Assert cells in simulation. it could be baked into the backend stuff i guess, making it platform-visible seems better to me offhand but debatable.
<awygle>
if cr1901_modern files an issue i'll add these comments there too
<whitequark>
awygle: sounds good, agree re pysim/cxxsim as well, which i forgot about earlier
<whitequark>
Assume cells too btw
<whitequark>
zince you should never violate those in simulation
<whitequark>
like... by definition of "assumption"
<awygle>
the semantics of Assume cells in simulation doesn't immediately jump out at me but i suppose they can be treated like Asserts
<awygle>
seem to remember that in some spec somewhere, or a blog post, or something
<FL4SHK>
can someone remind me how to have generated signal names in a module?
<whitequark>
the semantics of Assume is basically "Assert but it's proved elsewhere"
<FL4SHK>
maybe `m.signals["asdf"]`?
<whitequark>
if you do Assume(False) you basically say "always consider my design as proven"
<whitequark>
so if you ever violate Assume properties in simulation it means everything that comes after is not well-defined
<awygle>
FL4SHK: Signal(name="asdf")?
<awygle>
yeah makes sense
<FL4SHK>
awygle: ooh
<whitequark>
what do you mean by "generated signal names"?
<cr1901_modern>
>zince you should never violate those in simulation
<cr1901_modern>
You have restrict in systemverilog for "assumes that should be ignored in simulation, but should be used in formal"
<awygle>
yeah i also wasn't sure what you were asking but that should work
<FL4SHK>
well, I want like, an array of signals
<awygle>
oh yeah, thanks cr1901_modern, forgot about restrict
<FL4SHK>
not an `Array`
<FL4SHK>
though I think an `Array` would largely cover it, now that I think of it
<awygle>
FL4SHK: l = []; for i in range(n): l.append(Signal(name=f"sig{i}"))
<FL4SHK>
ah hah
<awygle>
you need Array if you want to index it with a Signal and not a python int
<FL4SHK>
right
<FL4SHK>
that distinction is fine by me
<awygle>
does nmigen even *have* restrict?
<awygle>
i imagine it does since it has e.g. Cover....
<FL4SHK>
I don't think yosys does?
<awygle>
almost sure yosys does
<FL4SHK>
oh it does?
<FL4SHK>
sounds like another tool to add
<whitequark>
awygle: nmigen doesn't inherently have restrict because it doesn't need that
<awygle>
it's basically an optimization iiuc
<whitequark>
well
<whitequark>
actually it might need that, now that i think about it
<whitequark>
yosys doesn't since yosys doesn't do simulation
<awygle>
ah it doesn't have it exposed currently
<awygle>
err, nmigen doesn't expose Restrict currently
<awygle>
in the way that it exposes Assume Assert and Cover
<whitequark>
i wasn't even aware of restrict until you mentioned it just now
<FL4SHK>
I don't know of it
<whitequark>
i don't know a lot about SVA sadly
<FL4SHK>
I don't get to use SVA at work
<FL4SHK>
only UVM
<FL4SHK>
I don't think UVM is the right answer, really
<awygle>
"restrict" { if (formal_mode) return TOK_RESTRICT; SV_KEYWORD(TOK_RESTRICT); }
<awygle>
oh cr1901_modern beating me again :p that's hte line in the verilog parser that supports the restrict keyword in yosys, which i know is not sufficient for support but is indicative
<whitequark>
i'm not really sure what UVM is either, since i never really worked with SV
<whitequark>
it seems very large and very enterprisey, but that doesn't necessarily make it bad
<FL4SHK>
UVM is verbose
<whitequark>
awygle: oh wait, i misunderstood what restrict() is
<FL4SHK>
I can, to a degree, get behind constrained random
<whitequark>
yeah we should just add that
<awygle>
mhm no nmigen involvement really, just passthrough
<awygle>
apparently it's not much used tho since nobody's asked for it lol
<whitequark>
there's no $restrict cell
<whitequark>
so it'll just be $assume but ignored in simulation
<awygle>
in yosys it probably turns into $assume
<awygle>
yeah?
<whitequark>
maybe Assume(..., formal_only=True) is better, even
<whitequark>
i don't know
<whitequark>
the SVA grammar is pretty large and making new importable keywords from it is kinda sketchy
<awygle>
or maybe it's used in the yosys sim stuff which i've never touched even once
<whitequark>
like, it's not in the prelude because it bloats the prelude a lot
<whitequark>
there is *definitely* no $restrict cell
<whitequark>
there's a -norestrict option in the verilog frontend
<whitequark>
which does let you use restrict with yosys sim
<awygle>
shrug. i dgaf about restrict on a personal level tbh. sounds like an "ask claire but no rush" to me.
<whitequark>
without any special support from the latter
<whitequark>
no no
<whitequark>
there isn't one cuz you don't need one
<whitequark>
it's a frontend issue
<awygle>
why would "norestrict" let you use restrict?
<awygle>
taht seems backwards
<whitequark>
uh, let me start over
<whitequark>
what i mean is that the behavior of the `restrict` syntactic construct is either the same as `$assume` cell, or nothing at all, depending on whether you do simulation or not
<whitequark>
this means that you don't need an IL entity so long as you know whether you simulate or not when you generate IL
<whitequark>
this means that a frontend can expose an option to change its behavior and that will be sufficient, without requiring a particular $restrict cell
<whitequark>
which is what yosys does
<whitequark>
the option is -norestrict just because the default in yosys is using it for synthesis/verification, not simulation
<awygle>
i see
<awygle>
so in nmigen Restrict would be emitted to rtlil as $assume
<FL4SHK>
seems my divider is working!
<awygle>
and ignored by e.g. pysim
<whitequark>
basically
<awygle>
that kind of argues for "bake it into the magic back layer" over "make it platform-visible", actually, since having .has_asserts, .has_assumes, and .has_restricts separately is annoying....
<cr1901_modern>
awygle: I'll write the issue over the weekend, please keep your feedback here in mind for a comment on the issue
<awygle>
wilco
<FL4SHK>
is the yosys bug I ran into a problem when *not* doing formal?
<awygle>
FL4SHK: if the problem is the disappearance of a signal you want to see, adding `attrs={'keep': 1}` to the signal constructor is worth a try
<awygle>
as a temp workaround
<FL4SHK>
awygle: ah, I see
<whitequark>
FL4SHK: yes, you can hit it if you constrain a clock and clean removes it
<whitequark>
the workaround is what awygle said
<whitequark>
the fix is to rewrite opt_clean to not do stupid things
<whitequark>
but ... it's sorta complicated
<awygle>
BREAKING: Yosys Codebase Complicated! News at 11! Stay Tuned!
<awygle>
i did enjoy that i looked up the _lexer_ file and saw a comment that was basically like "yeah this is a hack but doing it the other way is hard" lol
<whitequark>
well it's not that the codebase is complicated
<awygle>
(no shade, mad respect, just funny)
<whitequark>
it's that opt_clean does three different things and none of them correctly
<whitequark>
because different people had different ideas of what it should be doing
<whitequark>
the issue I linked teases out the things but someone still has to actually rewrite it
<whitequark>
this would also make cxxrtl work better in many cases
<whitequark>
mostly verilog-related
<awygle>
the codebase i'm working on at work has three different dependency-injection frameworks
<awygle>
not relevant, just like... i can relate to "different people had different ideas"
<whitequark>
uhuh
<whitequark>
also that sounds like a minor nightmare
XgF has quit [Ping timeout: 246 seconds]
XgF has joined #nmigen
jeanthom has quit [Ping timeout: 240 seconds]
<awygle>
it is, especially since they're all globally accessible. hard to tell when you've purged the uses.