whitequark changed the topic of #amaranth-lang to: Amaranth hardware definition language · code https://github.com/amaranth-lang · logs https://libera.irclog.whitequark.org/amaranth-lang
<d1b2> <widlarizer> py for i in range(self.depth): stages.append(Stage(self.width)) if i > 0: m.d.comb += stages[i].i.eq(stages[i - 1].o) m.d.comb += stages[0].i.eq(self.i) m.d.comb += self.o.eq(stages[i].o) Hi, any ideas what to do about this giving me UnusedElaboratable on all the stage objects?
lf has quit [Ping timeout: 252 seconds]
lf has joined #amaranth-lang
<_whitenotifier> [YoWASP/nextpnr] whitequark pushed 1 commit to develop [+0/-0/±1] https://github.com/YoWASP/nextpnr/compare/141f7b9d3902...c44409993d1e
<_whitenotifier> [YoWASP/nextpnr] whitequark c444099 - Update dependencies.
<tpw_rules> you have to add each stage to m.submodules
bl0x has joined #amaranth-lang
bl0x_ has quit [Ping timeout: 272 seconds]
Degi has quit [Ping timeout: 272 seconds]
Degi has joined #amaranth-lang
josuah has quit [Quit: WeeChat 3.4.1]
josuah has joined #amaranth-lang
josuah has quit [Read error: Connection reset by peer]
josuah has joined #amaranth-lang
josuah has quit [Ping timeout: 252 seconds]
josuah has joined #amaranth-lang
pie__ has quit []
pie_ has joined #amaranth-lang
pie_ has quit [Client Quit]
pie_ has joined #amaranth-lang
<koschei[m]> Are there any good examples of how to do formal verification that go beyond what https://github.com/robertbaruch/amaranth-exercises shows? I’m having a bit of trouble figuring out best practices for doing proof by induction on modules with FSM states and other complexities
<whitequark> formal verification isn't currently a topic that's well covered, unfortunately
<whitequark> that's something I plan to address in 2023
<koschei[m]> Ooh I’m looking forward to it! I’ve looked into using ZipCPU as an example, but I’m struggling a bit with how clunky Verilog’s formal verification syntax is
Raito_Bezarius has joined #amaranth-lang
<koschei[m]> Huh, it looks like they define a few registers so they only get instantiated during formal verification, and use those to track any state that’d otherwise be inaccessible outside the module, like which pipeline stage is active or how many times something occurred between resets. I kinda like that technique
feldim2425 has joined #amaranth-lang
smkz is now known as softminus