00:23 <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?

00:33 <_whitenotifier> [YoWASP/nextpnr] whitequark pushed 1 commit to develop [+0/-0/±1] https://github.com/YoWASP/nextpnr/compare/141f7b9d3902...c44409993d1e

00:33 <_whitenotifier> [YoWASP/nextpnr] whitequark c444099 - Update dependencies.

00:35 <tpw_rules> you have to add each stage to m.submodules

20:39 <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

20:41 <whitequark> formal verification isn't currently a topic that's well covered, unfortunately

20:42 <whitequark> that's something I plan to address in 2023

20:51 <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

21:38 <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