If I delete my ClockDomain and just replace m.d.ph1 with m.d.sync, BMC properly fails. So how do I define a ClockDomain correctly?

Aha. What you're hitting there is that verilog.convert / rtlil.convert (and therefore nmigen.cli.main) automatically create all missing clock domains with the default settings (i.e. they call ClockDomain(name)). When they do that, they also add the clock and reset to the list of ports.

So writing this:

m = Module()

# Cycle counter
cycles = Signal(6, reset=0, reset_less=True)
m.d.ph1 += cycles.eq(cycles + 1)

with m.If(cycles == 12):
    m.d.ph1 += Assert(cycles == 9)

main(m, ports=[cycles])

is equivalent to writing this:

m = Module()

ph1 = ClockDomain("ph1")
m.domains.ph1 = ph1

# Cycle counter
cycles = Signal(6, reset=0, reset_less=True)
m.d.ph1 += cycles.eq(cycles + 1)

with m.If(cycles == 12):
    m.d.ph1 += Assert(cycles == 9)

main(m, ports=[ph1.clk, ph1.rst, cycles])

(It works the same regardless of the domain name until you get to nmigen.build. nmigen.build does treat sync specially, in the sense that it is connected to the default platform clock when it is automatically created.)

Ah, so the absence of ph1.clk and ph1.rst in the ports passed to main was causing BMC to never hit the bad assert, because there was no clock for BMC to manipulate. Thus, it never encountered cycles==12. When I added ph1.clk and ph1.rst to the list of ports, BMC properly hits the assert and fails.

Indeed! Right now the SymbiYosys flow is not very ergonomic unfortunately. I'll make sure to improve this but this is more of a medium-term plan.