ChanServ changed the topic of #nmigen to: nMigen hardware description language · code at · logs at
Degi_ has joined #nmigen
Degi has quit [Ping timeout: 256 seconds]
Degi_ is now known as Degi
<ianloic> shouldn't it just be subtraction & checking the underflow?
<awygle> Yeah
<zignig> ianloic: , it's verilog, but detailed and explains well (as with all ZipCPU's stuff)
<awygle> lol that's kinda doofy
<zignig> doofy ? , kind of silly , but still works?
<awygle> yeah
<awygle> like i would not go into a design with that as the plan
<awygle> but it's a fun little game
<awygle> and it might be a good back-pocket trick to save you if you mess up something greiviously and are trying to hack around it
<zignig> indeed, did you manage to sort out your SLIP .vcd weirdness ?
<awygle> i did by rewriting the module >_> and it magically went away
<awygle> but i was doing some iffy stuff, so i think i maybe had a combinational loop
<zignig> BORK! , glad you fixed it.
<awygle> thanks :)
<awygle> how's your bonelessing going?
<zignig> getting there, just updating it to the new instruction set. Looking to put a streaming uart so it can store unprocessed char without exploding.
<awygle> cool cool
<zignig> and then CSR integration, I wrote my own , but nmigen-soc is a better plan.
<zignig> jnfg as been working on some peripheral designs in , looks kind of cool.
<zignig> *jfng
<awygle> yep
<awygle> this is maybe a poorly formed question but is there a way in nmigen to indicate that a set of conditions should be mutually exclusive? for guard in guards: if guard: action, and make sure all the "guard"s are orthogonal?
<awygle> that might be undecidable or something i guess
<zignig> in terms of an FSM or general logic ?
<awygle> my specific case is FSM transitions
<awygle> wanting to make sure they're not conflicting
<awygle> but i could see it being useful in other contexts
<zignig> perhaps a one hot encoder (lib/ in your FSM logic could force mutual exclusivity ?
<awygle> hm
<awygle> maybe
<awygle> i'll think about that approach, thanks
<zignig> no problem
____ has joined #nmigen
thinknok has joined #nmigen
chipmuenk has joined #nmigen
thinknok has quit [Ping timeout: 246 seconds]
Asu has joined #nmigen
futarisIRCcloud has quit [Quit: Connection closed for inactivity]
thinknok has joined #nmigen
FFY00 has quit [Remote host closed the connection]
FFY00 has joined #nmigen
FFY00 has quit [Max SendQ exceeded]
FFY00 has joined #nmigen
Ultrasauce has quit [Ping timeout: 240 seconds]
<MadHacker> awygle: Can't you just use a normal assert and do signal1 & (signal2 | signal3 | signal4) == 0 for example?
Ultrasauce has joined #nmigen
Asuu has joined #nmigen
Asu has quit [Ping timeout: 264 seconds]
thinknok has quit [Ping timeout: 272 seconds]
proteus-guy has quit [Ping timeout: 256 seconds]
FFY00 has quit [Remote host closed the connection]
FFY00 has joined #nmigen
proteus-guy has joined #nmigen
thinknok has joined #nmigen
<Sarayan> gtkwave has the most atrocious coding style ever
<Sarayan> at least for a non-joke one
<daveshah> As far as indentation goes, arachne-pnr was quite interesting...
<whitequark> doen't arachne-pnr use the gnu style?
<daveshah> Oh, maybe it does
<daveshah> I don't think I've ever really looked at the source of any gnu stuff
<whitequark> i love how the gnu code all uses \t as a shortcut for 8 spaces
<whitequark> but uses 2 columns for indentation
<whitequark> so it's quite literally combining the worst things about tabs *and* space.
<daveshah> Yeah, my experiences of editing arachne while preserving formating were never fun
<whitequark> apparently emacs does it automatically, because conserving space characters was important in 1980 was important or something idiotic like that
<whitequark> this is one of the reasons to never contribute to gnu code
<daveshah> If nextpnr didn't exist and maintenance of arachne continued, then I had plans to run the whole code base through clang format
<Sarayan> arachne was a better name :-P
<Sarayan> I need to convert the output of a LA to something gtkwave handles. Any recommendations? The gtkwave guys seem to like the fst format the most, but that may not be for the right reasons
<Sarayan> (like it's our format ! it's cool ! and it's compressed and stuff !)
<whitequark> never really looked close at FST
<whitequark> what kind of LA? how much data?
<Sarayan> Agilent LA, ala/alb formats
<Sarayan> never really big
<Sarayan> Phil is doing probes for me :-)
<whitequark> pyvcd should be ok
<Sarayan> hmmm, and do the converter in python? That makes some sense
<whitequark> ye
Vinalon has quit [Ping timeout: 264 seconds]
<MadHacker> Sarayan: If it's an *old* agilent LA I may have code for doing that already.
<MadHacker> I have an HP1661CS that you can pull the data off via FTP, and I've code for that -> vcd in python somewhere.
<Sarayan> dunno, the alb format is quite generic
<MadHacker> Looking at the code that's here (was written by a friend, not me) I don't think it's suitable. Seems to read a setup binary config from the scope and then a raw buffer of the data.
<Sarayan> that's must be the ala format, seems way more model-specific
<Sarayan> alb is a text description of the contents followed by the uncompressed contents in binary
<Sarayan> easy, tbh
thinknok has quit [Ping timeout: 272 seconds]
<awygle> Fst is actually quite reasonable afaict
<awygle> I read the paper and some of the source code
Asuu has quit [Read error: Connection reset by peer]
Asuu has joined #nmigen
Vinalon has joined #nmigen
<tpw_rules> is there a guide or tutorial or notes anywhere on testing and formal verification with nmigen?
<whitequark> tpw_rules: it is unfortunately somewhat incomplete, in the sense that there is no good integration with sby
<whitequark> Robert Baruch has been using it extensively though so I would look at his tutorial
thinknok has joined #nmigen
Asuu has quit [Ping timeout: 256 seconds]
Asuu has joined #nmigen
____2 has joined #nmigen
____ has quit [Ping timeout: 264 seconds]
Asuu has quit [Read error: Connection reset by peer]
Asu has joined #nmigen
<awygle> g'morning
<whitequark> hi!
<awygle> how's everybody doing today?
<whitequark> i made cxxrtl 30% faster
<whitequark> and opened the way towards making it 3 times faster on top of that
<whitequark> i... might actually achieve parity with single-threaded verilator? not just "order of magnitude" but "basically the same speed"
<awygle> i saw that
<whitequark> not sure yet
<awygle> dorbs little diff
<awygle> must have been a _very_ hot path
<whitequark> nope
<whitequark> it's in a code generator
<whitequark> not in the generated code
<whitequark> it changed the way some things are scheduled, eliminating a lot of delta cycles
<awygle> ah, ok
<awygle> well excellent work :)
<Sarayan> I don't think verilator does anything special, does it?
<awygle> it cheats in a few ways but i suspect cxxrtl cheats in those same ways (e.g. two-valued logic)
<Sarayan> oh, you need to -I share/yosys/install
<Sarayan> oh, you need to -I share/yosys/iclude that is
<Sarayan> oh, you need to -I share/yosys/include that is
<whitequark> awygle: cxxrtl doesn't cheat by assuming purely sync logic
<whitequark> unlike verilator
<awygle> ah ok
<awygle> i had forgotten verilator does that
<whitequark> literally the only thing that cxxrtl does if you make a latch from NAND cells is it becomes a lil bit slower
<awygle> that's a _big_ cheat
<whitequark> yes.
<whitequark> and it is much more insidious than you think
<awygle> speaking of latches, does nmigen warn on inferred latches? my guess is "no"
<awygle> because that's a backend thing
<whitequark> do you ever think why verilator always flattens your designs?
<Sarayan> urgh, everything is broken, life is terrible
<awygle> i don't actually use verilator
<awygle> Sarayan: i think you've migrated your terribleness from #yosys to #nmigen without realizing :)
<whitequark> because if you have e.g. comb feedback in wishbone, if you do not flatten your design, you will get apparent feedback arcs
<Sarayan> awygle : indeed
<whitequark> (lots of other things too)
<whitequark> so verilator, which cannot cope with any feedback loops *at all*, even apparent ones, has to require you to flatten
<awygle> sure, absolutely
<whitequark> cxxrtl on the other hand, you can even compile every verilog module as a separate c++ file
<Sarayan> do you topo-sort if flattened?
<whitequark> this... is unlikely to lead to an overall decrease in compile+run time unless your designs are stupidly large, but you can do it
<whitequark> Sarayan: better
<Sarayan> Oh?
<whitequark> i do not just topo-sort
<whitequark> topo sort doesn't work on graphs with loops, right?
<whitequark> so if i have a graph with a loop, i actually *minimize the amount of edges that loop back*
<Sarayan> well, you can always BFS it, but otherwise no
<whitequark> meaning that cxxrtl not just simulates your designs with feedback loops, but it does so in a near-optimal way
<whitequark> (with a heuristic, the optimal solution is NP-complete)
<whitequark> awygle: also, i plan to add X-propagation to cxxrtl
<whitequark> not sure about full 4-valued logic because i kind of hate the way Z works inside a design
<awygle> that np-complete problem is at generation time though, right? if it has a well-known solution (e.g. graph coloring) it might be nice to have a switch to use it if sim time is more important than compile/generation time
<whitequark> yes, at generation time
<whitequark> the problem is called "feedback arc set"
<sorear> you like X more than Z?
<awygle> so the "Well known solution" would be the Berger/Shor algorithm then i guess
<whitequark> they claim O(edges) runtime, which is actually not true, because they suggest I "obviously" use a data structure which does not appear to exist
<whitequark> >. Unfortunately, the Berger/Shor algorithm
<whitequark> is complicated and requires running time O(mn). In this paper we present a simple
<whitequark> FAS algorithm which guarantees a good (though not optimal) performance bound
<whitequark> and executes in time O(m). Further, for the sparse graphs which arise frequently in
<whitequark> graph drawing and other applications, our algorithm achieves the same asymptotic
<whitequark> performance bound that Berger/Shor does
<whitequark> the algo in this paper is stupidly simple
<Sarayan> X and Z tend to not exist in fpgas, right?
<Sarayan> not much in ICs either
<awygle> yeah doesn't sound worth it then
<awygle> whitequark: in defense of Z, we have talked about wanting to simulate e.g. Pins for whole-system simulation before, which would benefit from having Zs
<awygle> if it can be had without costing too much perf in the non-z case
<whitequark> 140 lines including all the C++ junk
<sorear> real Z was common when verilog was new, not so much now
<awygle> lol "it is clear"... no it isn't
<whitequark> now the funny thing about this paper is they suggest a data structure that gives you O(1) unlink *and* O(1) find-max-key
<Sarayan> awygle: Lately I tend to just set the output to ff for Z, and and every output
<whitequark> i have no earthly clue how such a structure would even look like
<Sarayan> depends on the O() of insert?
<Sarayan> I mean, sorted linked lis?
<whitequark> unlink and relink
<awygle> use an O(1) unlink structure and store index(max-key) on insert?
<mwk> ... wait, RTLIL doesn't allow logic loops?
<awygle> oh, relink also
<sorear> van der warden tree and play dumb if anyone asks you about the word size dependence?
<Sarayan> Errr, O(1) link, unlink and find-max makes sort O(n), so dream on paper author
<whitequark> mwk: RTLIL requires logic loops to be broken up with `sync always` rule
<awygle> that would be easy for me, because idk what that is :)
* awygle googles
<mwk> the what
<mwk> the process thing?
<Sarayan> wq: You can have O(log(n)) link unlink and O(1) find max with a heap, that's oflen good enough before log is low
<sorear> sorry, van emde boas
<whitequark> Sarayan: yes, there are tons of ways to get it "fast enough"
<whitequark> Sarayan: and in fact right now i literally sort the entire bin mappign each time i need a max key
<Sarayan> ok, not a real issue then
<sorear> but the "play dumb about whether the word size counts as an O(1) or O(log)" is the important part
<whitequark> which is totally braindead and yet never shows up in profile
<whitequark> it's just uh
key2 has quit [Ping timeout: 245 seconds]
<whitequark> i spent literal days trying to figure out how the fuck their O(m) bound can possibly be real
<whitequark> and i still have no idea
<Sarayan> nlog(n) find-max is bad you know :-)
<whitequark> oh wait
<whitequark> Travis Downs figured it out
key2 has joined #nmigen
<mwk> so what happens when you have a logic loop (say you implemented a latch thru gates) and are far enough in synthesis flow that there are no more processes? is the netlist invalid?
<whitequark> this is *extremely* not obvious but i guess it's fair
<Sarayan> heh
<Sarayan> "obvious structure, geee"
<whitequark> mwk: i think logic loops are only invalid for assigns within the non-sync part of a process
<awygle> lol
<whitequark> i lost some context in that explanation
<mwk> ... ah
<sorear> by the time you start caring about log factors you often have to care about the whole "random-access machines don't exist" thing as well :/
<whitequark> awygle: re nmigen and latches: you literally cannot write any nmigen code that *infers* a latch
<whitequark> awygle: you *can* currently write some nmigen code that makes a latch out of gates using a logic loop, but this is considered a bug (at least the fact that it won't warn)
<Sarayan> .comb loop?
<whitequark> Sarayan: think of the textbook latch from NAND gates
<Sarayan> Sure, but you'd need a .comb loop, right?
<whitequark> yes
<whitequark> and that is invalid RTLIL
<Sarayan> which is something I tend to consider verboten in nmigen
<Sarayan> yeah
<whitequark> yes
<whitequark> it's certainly intended to be banned
<whitequark> i just never got around to properly forbidding it yet
<Sarayan> technically, verilator has it right... to simulate nmigen, not verilog :-)
<whitequark> yes
<whitequark> verilator is perfectly suited to simulating the kinds of designs nmigen is perfectly suited for
<whitequark> this is not a coincidence
<awygle> whitequark: what does `s = Signal(); with m.Switch(..): with m.Case(0): s.eq(1): with m.Case(1): pass` do?
<Sarayan> s.eq(1) is a bug
<whitequark> nope
<Sarayan> m.comb += s.eq(1) or m.sync += s.eq(1) ?
<awygle> ok pretend i have the required boilerplate lol
<whitequark> er
<whitequark> yes
<Sarayan> it's not boilerplate, it changes the behaviour massively
<whitequark> i will pretend you wrote `m.comb += s.eq(1)`
<awygle> m.d.comb += s.eq(1)
<whitequark> in that case, suppose `..` is some expression `expr`. your code is equivalent to `m.d.comb += s.eq(~expr)`
<Sarayan> then it's equivalent to m.d.comb += s.wq(~(..))
<whitequark> undriven comb signals just return to their reset value
<whitequark> which is what you will find as a recommendation in any verilog style guide
<Sarayan> (yay I'm really starting to understand base nmigen, weeee)
<awygle> ahhh ok
<awygle> i literally have `# don't infer a latch` as a comment on like six lines of code in this document
<awygle> so i should go investigate whether that's needed
<Sarayan> .sync otoh makes s a latched value
<whitequark> a... flopped value?
<awygle> well sure, it's flip-flopped because it's in a clock domain
<awygle> in verilog the comb version infers a latch, which is why i asked
<whitequark> awygle: bottom line: in nmigen i consider footguns reportable bugs
<whitequark> you know, like reportable incidents in some industries
<Sarayan> wq: call them UB and call it a day ;-)
<awygle> sure
<whitequark> Sarayan: hey, you invented synthesizable verilog!
<Sarayan> was it inspired by C?
<Sarayan> (probably was, too)
<awygle> i kinda want to argue that assigning a signal in one branch of a switch but not the other should be an error... but i won't
<whitequark> awygle: so, if you really want to have belt *and* suspenders, how about writing an nmigen linter?
<whitequark> the AST is close to fully stable, the IR is not quite there but will be soon
<whitequark> I can even show you some examples
<awygle> uhhhhhhhhhhhhhhhhhhh 1) i am definitely interested in that 2) i have already signed up for too much stuff
<whitequark> you really can go as pedantic about it as you want. prohibit x.eq(y) where len(x) != len(y) for example, easily
<whitequark> well, feel free to open an issue on the tracker, and i'll post a simple example linter there, maybe for the two cases we discussed here
<awygle> sure
<whitequark> there's a reason every damn AST node has precise source locations, and it is to enable downstream tooling
<whitequark> sorear: i like X more than Z, yes
<whitequark> well, it's a bit "i like eggs more than public transport"
<_whitenotifier-3> [nmigen] awygle opened issue #360: nMigen Linter -
<awygle> i am not sure whether i like eggs or public transport more. in both cases i am pro in principle but lukewarm in practice.
<_whitenotifier-3> [nmigen] whitequark commented on issue #360: nMigen Linter -
<whitequark> Z gives you... well, tristates
<awygle> also you have (sunny side up, seattle busses) on one side and (deviled, shinkansen) on the other lol
<Sarayan> I read that as "downstream trolling", make of that what you want
<whitequark> and the thing is that you only really ever have tristates in a very small area of the toplevel module
<whitequark> (nmigen, of course, always instantiates IOBs in toplevel module, since some toolchains break if you don't do that)
<whitequark> (and don't flatten)
<awygle> i could see Z being lifted to some other level, like an IBIS-type system sim
<whitequark> mhm
<awygle> on the other hand if you want nmigen to be usable for asics it feels like you'd need to handle z someday
<whitequark> IMO, for Z, it is sufficient to have some yosys pass that maps `inout x` to `input i_x, output o_x, output oe_x`
<whitequark> (assuming you want to simulate with the vendor libs at all; otherwise you can just stick the Pin in your ports=[] array)
<whitequark> regarding ASICs: this came up for negative level resets
<mwk> ... that pass is on my TODO list, by the way
<whitequark> the problem here is that we cannot *simply* add an option for active low resets because there's a bunch of code that's like `with m.If(ResetSignal()):` which will get broken immediately
<Sarayan> awygle: do asics do Z internally?
<awygle> :shrug: they certainly uh... could.
<mwk> Sarayan: they can, and back in the olden days they actually did
<whitequark> I asked an ASIC guy on the nmigen issue tracker what he thinks we should do, and the answer is basically "add an inverter, then expect the inverter to be folded away in synthesis"
<mwk> as in, I'm reasonably sure ~2000-era nvidia GPUs did
<sorear> that recently?
<whitequark> which is fair? the only thing nmigen can do here is to add this inverter itself, twice, but it's really hard and probably isn't any better
<mwk> think so, yes
<whitequark> you are probably being pretty careful about the way your ASIC is reset, anyways, not something you can fuck up easily
<Sarayan> Of course in nmos we're usually working with pullup and Z/0, but nmos is beyond obsolete at this point :-)
<mwk> also note that in the old days, *FPGAs* could do internal Z
<whitequark> there is actually a similar issue with ClockSignal
<mwk> as in, every xilinx FPGA from xc3000 up to Virtex 2 supported internal tristate buses
* sorear thought the old days for this purpose ended at roughly 1µm and 1990
<whitequark> in that the code you write does not necessarily know whether the flops it requests are posedge or negedge triggered
<whitequark> because of DomainRenamer
<Sarayan> I'm pretty sure I don't understand reset in nmigen yet. One day maybe :-)
<mwk> and Virtex 2 was 2001
<whitequark> Sarayan: it's just late binding. you know how environment in UNIX works?
<whitequark> Sarayan: imagine that each elaboratable is a single UNIX executable, and it does getenv("RESET_SIGNAL") each time you write ResetSignal(), and the toplevel (or some module in between) can set that variable for its children
<whitequark> does this analogy help?
<Sarayan> oh-kay
<Sarayan> well
<Sarayan> you know I'm playing "reimplement the schematics in nmigen"
<whitequark> sure
<Sarayan> whre the reset line is explicit, and resets some things and not others
<whitequark> how many reset lines do you have, compared to clock lines?
<Sarayan> one of each
<Sarayan> even in the real world
<whitequark> oh
<Sarayan> at the pin level of couse
<Sarayan> I have phi2 and... rs? mr? not sure, depends on the chip
<whitequark> so, if a register has reset, you write Signal(...), if it has not, Signal(..., reset_less=True)
<whitequark> that's it
<Sarayan> oh
<whitequark> reset_less=True literally disconnects it from this "implied" reset line
<Sarayan> but reset is synced on a specific phase
<whitequark> ooh!
<whitequark> can you explain more about that?
<Sarayan> sure
<tpw_rules> phi2? what are you reimplementing?
<Sarayan> reset is a signal like any other for the chip, and iirc it's latched on one of the three phases
<Sarayan> need to recheck though
<Sarayan> tpw: via6522
<tpw_rules> figures. i know that signal name
<Sarayan> One of the two otput clocks from the 6502 :-)
<Sarayan> output
<MadHacker> For a 6502 in nmigen or similar, why not just double the clock rate?
<Sarayan> MH: I triple the clock rate, but yes
<MadHacker> Or have a phase signal for different bits of the signal.
<MadHacker> Ew. Triple why??
<MadHacker> It's a two-phase clock.
<MadHacker> + explicitly has no overlap so it's not like you need to cover all four hypothetical combinations of the two bits.
<Sarayan> because the via, internally, generates three phases
<Sarayan> up edge, down edge, just after down edge
<Sarayan> analog ftw
<MadHacker> For sampling on the shift register bits?
<Sarayan> for everything
<MadHacker> You *sure*? I mean, I've got two of them within arms reach and I've been programming them for the last 35 years and never noticed. :D
<MadHacker> I'll trust you if you've checked. :)
<whitequark> Sarayan: so, reset is latched in one of the phases, I get that
<whitequark> when does it actually reset the registers?
<whitequark> instantly? when the corresponing clock occurs?
<Sarayan> instantly, I think
<whitequark> okay, so it's an async reset latched in one of the phases
<whitequark> fortunately, nmigen can represent that!
<whitequark> (migen couldn't, and i remember getting into an argument with its author about whether such a thing is desirable...)
<Sarayan> an no, misremembered, it's not even latched
<Sarayan> it's just full async
<whitequark> oh! that's super easy then
<whitequark> right now you have three clock domain right?
<Sarayan> no, one
<Sarayan> three phase signals
<whitequark> ah, and three phase signals
<Sarayan> yeah, I've learned my lesson :-)
<whitequark> create the domain with `ClockDomain(async_reset=True)`
<MadHacker> I haven't, I'm doing a 6502 in nmigen for fun and because my logic design's rusty af.
<whitequark> drive `cd.rst` as active high
<whitequark> that's it
<whitequark> awygle: sorear: back to X-prop
<whitequark> in Verilog, X does three totally unrelated things
<Sarayan> MH: The small mess of mosfets under the phi2 pad (top left mostly) generates a small pulse on neg edge (bottom) and the top part does ~phi2 & ~pulse, so it's active in ~phi2 but only *after* the pulse is done
<Sarayan> hence the third pahse
<whitequark> awygle: sorear: first, it means "uninitialized but determinate value". second, it means "indeterminate value", e.g. as a result of setup/hold violation. third, it means "don't care for synthesis", aka LLVM undef
<MadHacker> OK, but are you reimplementing from schematic, or reimplementing just the datasheet behaviour?
<Sarayan> From schematic
<MadHacker> OK, then fair enough indeed.
<Sarayan> shematic I've built from extracting the mosfets from a vectorization of die shots
<MadHacker> I would have done a 6522 from datasheet, but I understand where you're coming from now.
<Sarayan> there are four different and somewhat contradictory datasheets
<MadHacker> As I said, I have two 6522s within arms' reach. I'm painfully aware. :D
<whitequark> awygle: sorear: i like (1) because i don't have a choice. real hardware does not always let you initialize things. even if it does, resetting a domain with reset_less=True registers effectively sets them to X in general (though in certain specific circumstances they may be assumed to be set to their reset value, e.g. on FPGA after bitstream load)
<MadHacker> I learned to code on a KIM-1, and I've a BBC master sitting next to me here.
<MadHacker> Somewhat used to the 65xx chaos. :)
<Sarayan> I *think* my closest 6522 is in the cave, unless it's still at my mother's
<awygle> i accept 1 and like 3, and don't like 2
<whitequark> awygle: sorear: (2) is not applicable to either nmigen (which attempts, although for now not very insistently, to prevent setup/hold violations in first place) or cxxrtl (which uses zero delay model, though more on that later)
<MadHacker> The beeb has the joys of clock-stretching for the 6522s because the 6502s existed in faster speed-grades than the 6522s did at the time.
<MadHacker> So the clocking there I somewhat understand too.
<Sarayan> wq: there's reset and there's reset, you reset a 68000 it just won't touch the registers for instance
<awygle> although i suspect the tools are not really set up to take advantage of 3
<Sarayan> note that they're random at poweron
<whitequark> awygle: unfortunately they are, and this is a massive problem no one in HDL properly acknowledges IMO
<Sarayan> so well... :-)
<whitequark> awygle: sorear: so what happens there is that if you put 'x somewhere, it will behave like LLVM undef, meaning that constant propagating one 'x makes it into two 'x, which the optimizer can then assume have different values later in the pipeline
<Sarayan> but that means you don't want to clear them on simulated reset, but you don't want them indeterminate at startup on a fpga because indeterminate is bad
<whitequark> this means that you can make a design where a module enforces certain invariant, and this specific module can even be formally verified to do it
<whitequark> but then, in a bigger design, you feed it 'x... and if the synthesizer can statically prove that it has 'x as an input, it can, and often will, "optimize" your module into something that violates the invariant
<whitequark> e.g. if you had `s & ~s` in that module, and the synthesizer can prove that s=='x, then it can optimize `s & ~s` to `1`
<awygle> sure. that's a bit different than what i was talking about, which is "if the synthesizer can statically prove it has an 'x as an input it should throw an error"
<awygle> or... not quite that but closer to that than the other
<whitequark> as an input where?
<awygle> i don't think i actually want 'x anyway
<whitequark> the whole point of synthesis don't-cares is that they *do* propagate
<whitequark> the problem with them is that there is no way to tell the synthesizer "ok buddy. i know you love optimizing stuff so that it breaks. but. i know that this wire is ACTUALLY either 0 or 1 not both. so please give me something that will never be both"
<whitequark> in LLVM parlance this operation is called "freeze" and it stops const-propagation of 'x
<whitequark> i have proposed it for yosys and Claire has tentatively accepted it
<Sarayan> don't-care-but-defined
<whitequark> so you could freeze all of your inputs for example, and then your internal invariants will be maintained
<sorear> did freeze actually happen? I remember the extremely long thread proposing it
<whitequark> the problem is there is absolutely no way to (a) express this in synthesizable Verilog that Xilinx, Altera, etc understand
<whitequark> or (b) stop *other kinds of 'x* from becoming *this* kind of x because they're all conflated
<whitequark> for example, suppose the synthesizer statically proves you never write to BRAM and the BRAM is not initialized
<whitequark> then it will drag 'x out of that BRAM and fuck up your perfectly well defined design
<whitequark> in the sense that not only will the design not work, but it will also have violations of safety invariants
<Sarayan> otoh, the design not owrkign tends to be a hint
<Sarayan> working
<daveshah> Interestingly, I have had a few people report things like this as a supposed Yosys bug. Usually disconnected submodule inputs, which the vendor tools tend to assume as 1'b0 but Yosys treats as undefined, sometimes resulting in very different behaviour.
<whitequark> Sarayan: the real issue is when this happens in generic reusable code that you convince yourself works fine
<whitequark> or when two such pieces of code interact in unexpected ways
<whitequark> there are *lots* of subtle ways to statically get a 'x in verilog where you really don't intend to
<whitequark> awygle: X-propagation in case (1) is super handy because if you have a bench that's all lit up with red it means you fucked up some reset
<whitequark> and, moreover, it is required to be supported in nmigen for ASICs
<whitequark> since ASICs don't really have initializable BRAMs
<whitequark> so you *have* to have some way to say "uninitialized memory" and then you have to support it in sim, too, or you'll get sim/synth mismatch
<whitequark> the good thing about case (1) is that it requires no language support
<whitequark> only simulator support, and toolchain support to a degree
<whitequark> of course, without the $freeze cell, it is not actually safe, but it is impossible to fix it on nmigen side, even though it is a flaw literally all of the industry suffers from
<whitequark> it should be safe enough for real designs though
<whitequark> sorear: i think freeze is still not in llvm
<whitequark> Sarayan: nmigen will never initialize signals to indeterminate values on FPGA
<whitequark> it... can't even do that if it tried, I think
<whitequark> since most FPGAs have a global post-configuration reset for all flops
<whitequark> so if you model 68k registers as reset_less, then it will work as you expect
<MadHacker> Need a chaos monkey on reset option. :D
<daveshah> Oh, I think I know an obscure edge case where FPGA flops have an indeterminate state
<whitequark> MadHacker: i have had this request for nmigen pysim, actually
<daveshah> If you use partial reconfiguration on an ECP5, the PUR isn't activated (which is good for many things) but as a result any flops have the value of the flop previously placed at that location, if any
<whitequark> and i imagine you could do it for a real FPGA by permuting post-place flop init values with a tcl script or something
<whitequark> daveshah: I was actually expecting this
<sorear> so you transform the design to add a "soft" scan chain, then connect it to a random bit generator, ,
<whitequark> but the key part is that nmigen can't really decide to do that on its own
<daveshah> Yeah
____2 has quit [Quit: Nettalk6 -]
<MadHacker> If we can pass it through to nextpnr then it can generate random values based off the seed. :)
<Sarayan> wq: Very nice
<whitequark> Sarayan: which part?
<Sarayan> So it's pretty much reset_less by default, unless there's an explicit reset signal in there
<Sarayan> (when translating shcematics that is)
<whitequark> yes
FFY00 has quit [Remote host closed the connection]
FFY00 has joined #nmigen
_whitenotifier-3 has quit [Ping timeout: 260 seconds]
thinknok has quit [Ping timeout: 272 seconds]
Asu has quit [Quit: Konversation terminated!]
FFY00 has quit [Read error: Connection reset by peer]
FFY00 has joined #nmigen
chipmuenk has quit [Quit: chipmuenk]
<ktemkin> whitequark: are we okay to start using the nextpnr --12k option that was added a month or so ago, in master?
<ktemkin> (for ECP5, sorry)
<ktemkin> I'd love to make a change like this: , but I don't know if breaking compat with earlier nextpnr versions is an issue
<awygle> ktemkin: the current "treat it like a 25F" doesn't actually work (can't program) so I can't imagine there's a compat hazard. I'm not wq tho
<ktemkin> it does if you add an IDCODE overrride
<ktemkin> so there /are/ valid platform files that could contain 12F and --idcode{}; those'd be broken on older nextpnrs
<cr1901_modern> 25F and idcode override doesn't continue to work for back compat?
<ktemkin> cr1901_modern: it does; but every platform needs to specify the override itself
<ktemkin> nmigen doesn't automatically add it on getting device = "<...>-12F"
<ktemkin> I'd expect user expectations going forward to be that they can set "LFE5U-12F" and it'd just work, since nextpnr now does
<ktemkin> (an option that'd both compat friendly and user-friendly might be to set the override ourselves -and- set 25F; but that feels a bit like carrying around legacy cruft)
<cr1901_modern> I don't see the issue w/ keeping 25F and override for existing platforms, but for new platforms use 12F
<cr1901_modern> but admittedly I'm not following this closely :P
<whitequark> ktemkin: sometimes you have to break the code to fix it
<whitequark> this case is unambiguously "make the change"
<awygle> woo
<awygle> score one for the future
<daveshah> If you are making the change you can also remove the um and um5g 12k parts from the list as they don't exist
<ktemkin> I though those looked off
_whitenotifier-9 has joined #nmigen
<_whitenotifier-9> [nmigen] ktemkin opened pull request #361: vendor: use nextpnr -12k for -12F devices; remove theoretical devices -
<_whitenotifier-9> [nmigen] ktemkin edited pull request #361: vendor: use nextpnr -12k for -12F devices; remove theoretical devices -
<ktemkin> daveshah: added to the (now open) PR :)