ChanServ changed the topic of #nmigen to: nMigen hardware description language · code at · logs at · IRC meetings each Monday at 1800 UTC · next meeting October 12th
<miek> mithro: the ones in PyRTL?
<mithro> Ahh ha! It was PyRTL not PyMTL
emeb has quit [Quit: Leaving.]
<mithro> Hrm, maybe not -- I can't seem to find an example
<miek> this was the link you posted before: and there's also a few here:
<mithro> miek: Thanks!
_whitelogger has joined #nmigen
cr1901_modern1 has quit [Quit: Leaving.]
cr1901_modern has joined #nmigen
XgF has quit [Ping timeout: 240 seconds]
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
chipmuenk has joined #nmigen
cr1901_modern has quit [Quit: Leaving.]
cr1901_modern has joined #nmigen
<_whitenotifier-f> [nmigen] kowalewskijan synchronize pull request #504: Add quicklogic platform -
<_whitenotifier-f> [nmigen] kowalewskijan reviewed pull request #504 commit -
<_whitenotifier-f> [nmigen] kowalewskijan synchronize pull request #504: Add quicklogic platform -
<_whitenotifier-f> [nmigen] kowalewskijan reviewed pull request #504 commit -
<_whitenotifier-f> [nmigen] whitequark reviewed pull request #504 commit -
<_whitenotifier-f> [nmigen/nmigen] whitequark pushed 1 commit to cxxsim [+0/-0/±1]
<_whitenotifier-f> [nmigen/nmigen] whitequark 4dea799 - build.plat: avoid type confusion in _check_feature.
<_whitenotifier-f> [nmigen/nmigen] whitequark created branch cxxsim
<whitequark> ktemkin: yeah
<_whitenotifier-f> [nmigen/nmigen] whitequark pushed 1 commit to master [+0/-0/±1]
<_whitenotifier-f> [nmigen/nmigen] whitequark d22b2c5 - build.plat: avoid type confusion in _check_feature.
<_whitenotifier-f> [nmigen/nmigen] github-actions[bot] pushed 1 commit to gh-pages [+0/-0/±13]
<_whitenotifier-f> [nmigen/nmigen] whitequark b61078f - Deploying to gh-pages from @ d22b2c56041e27031690415d1fb23a09d17999e8 🚀
<_whitenotifier-f> [nmigen] whitequark reviewed pull request #504 commit -
<_whitenotifier-f> [nmigen] kowalewskijan synchronize pull request #504: Add quicklogic platform -
<_whitenotifier-f> [nmigen] kowalewskijan reviewed pull request #504 commit -
hitomi2509 has quit [Quit: Nettalk6 -]
<_whitenotifier-f> [nmigen] whitequark reviewed pull request #504 commit -
<_whitenotifier-f> [nmigen] whitequark reviewed pull request #504 commit -
hitomi2509 has joined #nmigen
<_whitenotifier-f> [nmigen] kowalewskijan synchronize pull request #504: Add quicklogic platform -
jeanthom has quit [Ping timeout: 258 seconds]
peepsalot has quit [Quit: Connection reset by peep]
jeanthom has joined #nmigen
<_whitenotifier-f> [nmigen-boards] kowalewskijan edited pull request #117: Add chandalar and quickfeather boards -
<_whitenotifier-f> [nmigen-boards] kowalewskijan edited pull request #117: Add quickfeather board -
peepsalot has joined #nmigen
<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
<lkcl> ah fantastic, thank you
<lkcl> added.
<Lofty> I'm trying to figure out what the reference clock is for the Cyclone 10 GX reference board
<Lofty> But there's so much marketing wank about how flexible their clocks are that I actually can't tell
<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
<FL4SHK> cool
<FL4SHK> non-overlapping is what I'm after
<lkcl> FL4SHK: the code's all here if you're interested;a=tree;f=src/ieee754/div_rem_sqrt_rsqrt;hb=HEAD
<lkcl> that's an *integer* div-rem-sqrt-rsqrt which we then "wrap" to make IEEE754 fpdiv/fpsqrt/fprsqrt
<FL4SHK> the "wrap" is something I've done before
<FL4SHK> I was planning on doing the same thing.
<lkcl> yeah once you have an integer divide it's pretty straightforward to use that to do mantissa-divide
<FL4SHK> yeah
<FL4SHK> I'll study your code
<lkcl> a tricky bit is the infrastructure needed to "share" the two so that you can use the same DIV unit for INT and FP
<FL4SHK> that's something I wasn't planning on doing
<FL4SHK> it'd cause them to be different speeds
<lkcl> saves silicon but has the disadvantage of... yeah that would be one
<lkcl> it has the disadvantage of leaking timing analysis information between different units, if you're hyper-interested in security
<lkcl> here's the "glue" code btw -;a=tree;f=src/ieee754/fpdiv;hb=HEAD
<FL4SHK> that's fair
<lkcl> it starts to get... a little involved, there, because we did pipelines constructed from multiple combinatorial "stages" as we call them
<lkcl> so there's two parameters:
<lkcl> 1) the radix depth
<lkcl> 2) the number of combinatorial stages per pipeline stage
<lkcl> line 166;a=blob;f=src/ieee754/fpdiv/;hb=HEAD
<FL4SHK> I haven't decided whether or not I'm going to pipeline the divider
<FL4SHK> I will be having many of them
<FL4SHK> due to the vector arch
<lkcl> yeah we don't know either, yet. might go with a FSM and have multiple of them
<lkcl> we planned in advance for that (in nmutil) so that we can use the same "combinatorial blocks" without doing a total code rewrite
<FL4SHK> my long divider's code is rather small
<FL4SHK> I'm thinking of adding in a pipelined version
<lkcl> yeah it's amazing how little code is actually needed
<lkcl> that's where it can get complicated :)
<lkcl> the microwatt entire FP code, done as a FSM, to support full OpenPOWER ISA FP32, is i think only around 4,000 lines of VHDL. it's a BIG FSM :)
<FL4SHK> SBY 9:43:37 [volt32_cpu/long_udiv_cover] smt2: ERROR: No such command: dffunmap (type 'help' for a command overview)
<FL4SHK> what program am I missing?
Asu has joined #nmigen
<lkcl> you've not got the latest version of yosys
<FL4SHK> gonna install yosys-git
<lkcl> yeh good idea :)
jeanthom has quit [Ping timeout: 272 seconds]
hitomi2509 has quit [Quit: Nettalk6 -]
<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
<whitequark> okay but... sby immediately creates intermediate files
<whitequark> hm
<whitequark> this is actually the opposite of the direction i want to go in
* cr1901_modern nods
<whitequark> i'm leaning towards having formal use
<whitequark> so you'd have and design.debug.v as well
<whitequark> (hell, one day we might have a design.debug.vhd, just needs yosys support)
<whitequark> cr1901_modern: if it was a tempdir then you'd have a hard time debugging assertion failures
<whitequark> since it puts the vcd inside
<cr1901_modern> Hmmm, that's true
<whitequark> i think formal toolchain integration needs an RFC
<whitequark> so feel free to open an issue for it without waiting for a meeting
<cr1901_modern> Alright, I'll think it over (If the past 20 mins is any indication tho, don't expect miracles from my RFC :P).
<cr1901_modern> (Then again, that's what RFCs are for...)
peepsalot has quit [Ping timeout: 260 seconds]
jeanthom has joined #nmigen
<whitequark> maybe open an issue first so everyone interested can chime into what they want from an rfc
<whitequark> afaik we don't have one at the moment
peepsalot has joined #nmigen
jeanthom has quit [Ping timeout: 240 seconds]
<_whitenotifier-f> [nmigen/nmigen] whitequark pushed 1 commit to master [+0/-0/±2]
<_whitenotifier-f> [nmigen/nmigen] whitequark e58233b - tests: keep comments up to date. NFC.
<_whitenotifier-f> [nmigen/nmigen] github-actions[bot] pushed 1 commit to gh-pages [+0/-0/±13]
<_whitenotifier-f> [nmigen/nmigen] whitequark f00546c - Deploying to gh-pages from @ e58233b44133577c54bc0ba575e8fe37a2d2215b 🚀
<_whitenotifier-f> [YoWASP/yosys] whitequark created branch release
chipmuenk has quit [Quit: chipmuenk]
<_whitenotifier-f> [nmigen] whitequark closed pull request #504: Add quicklogic platform -
<_whitenotifier-f> [nmigen/nmigen] whitequark pushed 1 commit to master [+1/-0/±0]
<_whitenotifier-f> [nmigen/nmigen] kowalewskijan 9746138 - vendor.quicklogic: new platform.
<_whitenotifier-f> [nmigen/nmigen] github-actions[bot] pushed 1 commit to gh-pages [+0/-0/±13]
<_whitenotifier-f> [nmigen/nmigen] whitequark c02ec9f - Deploying to gh-pages from @ 9746138e555828a74648d98d55bf732d762fd8f6 🚀
<_whitenotifier-f> [nmigen/nmigen] whitequark pushed 1 commit to master [+0/-0/±3]
<_whitenotifier-f> [nmigen/nmigen] whitequark 80194e1 - CI: fix code coverage collection.
<_whitenotifier-f> [nmigen/nmigen] github-actions[bot] pushed 1 commit to gh-pages [+0/-0/±13]
<_whitenotifier-f> [nmigen/nmigen] whitequark ff91825 - Deploying to gh-pages from @ 80194e1a7ee7d9423a102a8f9f9bc36602d76a2c 🚀
<_whitenotifier-f> [nmigen/nmigen] whitequark pushed 1 commit to master [+0/-0/±1]
<_whitenotifier-f> [nmigen/nmigen] whitequark a6db99b - README: Quicklogic EOS S3 is now supported.
<_whitenotifier-f> [nmigen/nmigen] github-actions[bot] pushed 1 commit to gh-pages [+0/-0/±13]
<_whitenotifier-f> [nmigen/nmigen] whitequark e48e9a9 - Deploying to gh-pages from @ a6db99b05e8bf3dcf90e0ebb06965b7e6b678006 🚀
<_whitenotifier-f> [nmigen-boards] whitequark commented on pull request #117: Add quickfeather board -
emeb_mac has joined #nmigen
<_whitenotifier-f> [nmigen/nmigen] whitequark pushed 1 commit to cxxsim [+3/-0/±4]
<_whitenotifier-f> [nmigen/nmigen] whitequark d2ddf65 - [WIP] sim: add cxxsim engine.
<_whitenotifier-f> [nmigen-boards] whitequark closed pull request #111: Arty S7 OpenOCD Support -
<_whitenotifier-f> [nmigen/nmigen-boards] whitequark pushed 1 commit to master [+0/-0/±1]
<_whitenotifier-f> [nmigen/nmigen-boards] cr1901 bcc1467 - arty_s7: add openocd and flashing support.
<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
<daveshah> Look here for something that matches: ?
<daveshah> Or look at the naming in a Diamond generated wrapper which should match those docs
<Degi> Oh neat
<Degi> Yeah, its called rate_mode
jeanthom has joined #nmigen
chipmuenk has joined #nmigen
chipmuenk has quit [Client Quit]
chipmuenk has joined #nmigen
Lord_Nightmare has quit [Quit: ZNC -]
Lord_Nightmare has joined #nmigen
chipmuenk has quit [Quit: chipmuenk]
<alanvgreen> lkcl Thanks for the advice re: nmigen/verilog/litex. This looks like it will fit our use case
<FL4SHK> so I'm not seeing my signal in the formal verification vcd?
<FL4SHK> I've assigned to it
<FL4SHK> this is some strange behavior
<FL4SHK> really irritating
<FL4SHK> It passed for the base case when I added in an `Assume` that doesn't affect anything but a formal-only signal that is never *read*
<FL4SHK> I declare it and assign to it *only*
<FL4SHK> I'm going to post my stuff here
<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>, 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/`?
<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?
<FL4SHK> let me post the script
<FL4SHK> and the thing calling formal
<whitequark> hm. but... aren't you setting the RTLIL location yourself?
<whitequark> i just need
<FL4SHK> ooh
<FL4SHK> yeah, that's where I ran
<whitequark> okay, so loc.gt_vec lives on line 76
<whitequark> you can see the \src attribute pointing to the place where you instantiate the signal
<whitequark> lol, your paste downloads as "New Paste 1.txt" and there's no way to get read_ilang to open that file
<whitequark> the yosys script parser is truly cursed
<awygle> o boi really
<awygle> awesome
<whitequark> yes
<whitequark> it sucks
<whitequark> so badly
<whitequark> you can't quote anything
<whitequark> worse, you can't escape anything
<whitequark> not even badly and in an inconsistent way. you just can't.
<whitequark> you can shell out with !ls and use shell escaping, if you really needed it, I think
<whitequark> *!cp or something
* awygle also likes formal and would like to see its integration improved but will read scrollback before talking out of turn
<whitequark> okay that paste service is cursed
<whitequark> it slaps a BOM in front of the file
<whitequark> yosys then breaks trying to read it
<FL4SHK> hm, should I use another?
<whitequark> in the future, probably; I'll just fix your file manually for now
<whitequark> I use usually
<whitequark> argh, how do I even remove a BOM easily
<FL4SHK> I don't even know what a BOM is
<whitequark> ah, sublime text can resave without BOM
<whitequark> byte order mark
<FL4SHK> ah
<whitequark> a non-printable Unicode character that, contrary to its name, isn't usually used to show byte order
<whitequark> because UTF-8 only has one
<whitequark> (still not as bad as the combining grapheme joiner, which does not join graphemes *ever*)
<awygle> lol
<whitequark> no really, let me show you the FAQ entry
<awygle> i know (because i follow manishearth on twitter) :p
<whitequark> oh
<whitequark> for everyone else:
<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
<whitequark> \gt_vec is removed by prep -top
<FL4SHK> I don't know my yosys that well any more
<whitequark> specifically by opt_clean
<whitequark> removing unused non-port wire \gt_vec.
* whitequark sighs
<FL4SHK> I hope you're not upset with me
<whitequark> so this is something i have been wanting to fix, and mwk was working on it too iirc
<whitequark> nope
<lkcl> FL4SHK: you can use pep8checker and if you're feeling brave autopep8. they're both well-known tools, search for them.
<whitequark> FL4SHK: absolutely not at all
<FL4SHK> cool, so this is a known issue
<whitequark> this is a yosys bug (upgrading it from an 'issue' since i know exactly what the problem is, and it's longstanding)
<whitequark> let me see what the tracking issue was
<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
<FL4SHK> I think formal is
<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.
<awygle> ah well
Asu has quit [Remote host closed the connection]
<_whitenotifier-f> [nmigen] whitequark commented on pull request #504: Add quicklogic platform -
<_whitenotifier-f> [nmigen] whitequark edited a comment on pull request #504: Add quicklogic platform -
<FL4SHK> whitequark: so I have another issue besides the signal disappearing
<FL4SHK> I mentioned this before but
<FL4SHK> this is a more pressing issue
<FL4SHK> line 462
<FL4SHK> `loc.temp_denom_mult_lut_X` is only read, never written
<FL4SHK> whereas `loc.denom_mult_lut[X]` is written to
<FL4SHK> hm
<FL4SHK> seems I might have made a mistake