00:21 <_whitenotifier-1> [YoWASP/nextpnr] whitequark pushed 1 commit to develop [+0/-0/±1] https://git.io/JKl2T

00:21 <_whitenotifier-1> [YoWASP/nextpnr] whitequark 5f3b94c - Update dependencies.

01:01 <_whitenotifier-1> [YoWASP/yosys] whitequark pushed 1 commit to develop [+0/-0/±1] https://git.io/JKlwz

01:01 <_whitenotifier-1> [YoWASP/yosys] whitequark 422f096 - Update dependencies.

12:41 <FL4SHK> dragonmux: thank.

14:26 <FL4SHK> So, AXI uses 0 for reset assertion, so how can I represent that in nMigen?

14:32 <dragonmux> AXI usually names the signal RESETB (B meaning bar), so reset_n in nMigen scheme.. which you can drive from the clock domain ResetSignal() with `m.d.comb += reset_n.eq(~ResetSignal())`

14:32 <FL4SHK> Ah.

14:33 <FL4SHK> What is this RESETB?

14:33 <FL4SHK> I'm not familiar with this part of AXI

14:33 <FL4SHK> It's not part of the AXI4 stuff I've done at work.

14:33 <dragonmux> give us a sec, opening the AXI4 docs

14:33 <dragonmux> (spec)

14:34 <d1b2> <dragonmux> https://cdn.discordapp.com/attachments/726185180599156796/898942034730172436/unknown.png

14:34 <FL4SHK> `aresetn` is the name of the signal.

14:35 <dragonmux> it was ARESETn, our bad on the memory.. too wormed by Xilinx crimes where it becomes ARESETB

14:35 <FL4SHK> Ah.

14:35 <dragonmux> but as said, in nMigen naming scheme that's reset_n so can be driven as above from ResetSignal()

14:36 <dragonmux> in our experience that's sufficient

14:36 <FL4SHK> Yeah, that part I get.

14:36 <FL4SHK> It makes sense.

14:36 <dragonmux> :)

14:36 <FL4SHK> :)

14:57 <FL4SHK> Having a problem

14:57 <FL4SHK> Can't formally verify a signed divider

14:58 <FL4SHK> Oh, maybe there's a way

14:59 <FL4SHK> Yeah, I found a way.

15:15 <FL4SHK> Got it to pass!

23:06 <FL4SHK> Formally verified my pipelined long divider!

23:07 <FL4SHK> Next I need to work on my instruction set....