ChanServ changed the topic of #nmigen to: nMigen hardware description language · code at https://github.com/nmigen · logs at https://freenode.irclog.whitequark.org/nmigen
rohitksingh has joined #nmigen
<awygle> do FSMs reset their states if not assigned?
<ZirconiumX> I assume they keep their state and so infinitely loop there
<ZirconiumX> I suppose I don't understand the question actually
<awygle> that was my expectation but my BMC trace seemed to imply otherwise
<awygle> it happily made what should have been an illegal/impossible transition back to the reset state
<awygle> maybe it pulled reset behind my back but it didn't look like it did
<awygle> oh well, this module is hopelessly wrong anyway so :shrug:
proteus-guy has quit [Ping timeout: 246 seconds]
Degi has quit [Ping timeout: 260 seconds]
Degi has joined #nmigen
____ has joined #nmigen
avg has joined #nmigen
<avg> I'm trying to have a default value for a comb signal which is overridden on certain conditions.
<avg> If I have multiple m.d.comb += sig.eq(x) lines in my module, is the last guaranteed to override the first?
<awygle> Yes (provided it applies and isn't like, under an If)
<awygle> An If whose condition is false rather
<avg> Right. so m.d.comb += sig.eq(0) followed by m.If(condition): m.d.comb += siq.eq(5) should set sig to 5 if condition, else 0
<avg> thanks
enok has joined #nmigen
enok has quit [Ping timeout: 246 seconds]
enok has joined #nmigen
enok has quit [Ping timeout: 272 seconds]
chipmuenk has joined #nmigen
lkcl has quit [Ping timeout: 260 seconds]
Asu has joined #nmigen
Asuu has joined #nmigen
Asu has quit [Ping timeout: 256 seconds]
lkcl has joined #nmigen
avg has quit [Remote host closed the connection]
enok has joined #nmigen
avg has joined #nmigen
pinknok has joined #nmigen
enok has quit [Ping timeout: 258 seconds]
avg has quit [Ping timeout: 245 seconds]
chipmuenk has quit [Quit: chipmuenk]
chipmuenk has joined #nmigen
____ has quit [Quit: Nettalk6 - www.ntalk.de]
<_whitenotifier-9> [nmigen] awygle opened issue #376: Allow selecting proof engine in FHDLTestCase - https://git.io/Jf3ki
<awygle> it's nice when formal finds you a bug. makes it feel worth it.
<awygle> pdr is so much more intuitive than k-induction, like damn
<daveshah> Shame it tends to blow up on non-trivial designs
<daveshah> at least ime
<daveshah> and doesn't support memories other than bit-blasted (I think this is a fundamental limitation of ic3)
<awygle> define "blow up" and "non-trivial"
<daveshah> I think it was something CPU-like (maybe part of picorv32), it was a while ago
<awygle> ah
<daveshah> But in general, I think ZipCPU has had similar experiences, pdr usually either takes a few seconds or never completes
<awygle> what algorith does avy use? or suprove?
<awygle> PDR and Interpolation, i see
<awygle> i can barely find anything about suprove/superprove/super_prove on google
<awygle> ok so superprove simplifies, abstracts, speculates, and then hits it with PDR, BMC, interp, and BDD all at once. "super" indeed.
Asu has joined #nmigen
Asuu has quit [Ping timeout: 264 seconds]
<_whitenotifier-9> [nmigen] whitequark commented on issue #376: Allow selecting proof engine in FHDLTestCase - https://git.io/Jf3mD
<_whitenotifier-9> [nmigen] whitequark closed issue #376: Allow selecting proof engine in FHDLTestCase - https://git.io/Jf3ki
<whitequark> what's pdr?
<daveshah> Property driven reachability
<daveshah> *directed
cckonnok has joined #nmigen
pinknok has quit [Ping timeout: 272 seconds]
<awygle> Ah, my misconception then.
<awygle> It's pretty convenient tho...
<cr1901_modern> Is PDR/ic3 support something that's semi-new in yosys/sby? Never heard of these myself before now.
cckonnok has quit [Ping timeout: 246 seconds]
<awygle> Na it's been around but none of the resources discuss it
<awygle> Perhaps because K-induction is easier to explain
<awygle> Or is more "interpretable" in that you can probably figure out why you're failing what should be a valid proof
<cr1901_modern> Okay, I seem to very vaguely recall Claire talking about this in one of her old presentations: http://ecee.colorado.edu/~bradleya/ic3/ic3_bradley.pdf
<cr1901_modern> And I must've stuffed this away for "study later", and later never came.
<vup> whitequark: would you consider something akin to FHDLTestCase to the public nmigen API? I thinks its really useful.
_whitelogger has joined #nmigen
FFY00 has joined #nmigen
<whitequark> vup: that's the plan, but for now it's not clear to me what sort of API it should provide or how it would be implemented exactly
<ktemkin> https://github.com/greatscottgadgets/luna/blob/master/luna/gateware/test/utils.py <-- I do a similar thing in LUNA; it's not fully generic, but it might have ideas worth observing
<whitequark> yup, the idea is that we'll take a look at how people actually write formal test cases and then aggregate it
<awygle> sensible
<awygle> i guess i'll just copy-paste FHDLtestCase into my project with my modifications then, for now
Asuu has joined #nmigen
Asuu has quit [Remote host closed the connection]
Asu has quit [Ping timeout: 265 seconds]
<vup> yeah makes sense
cckonnok has joined #nmigen
cckonnok has quit [Ping timeout: 265 seconds]
cckonnok has joined #nmigen
cckonnok has quit [Ping timeout: 265 seconds]
samlittlewood has quit [Quit: samlittlewood]