Xekri

Nope, still fails.

Indeed! [toplevel.il.zip](https://github.com/nmigen/nmigen/files/5491860/toplevel.il.zip)

Hmm. Here's the .v file if that helps, along with the sby for that. Adding `(* gclk *)` before the clk signal causes BMC to pass. ``` [tasks] cover bmc...

I'm not sure how I could tell. I do know that the Cover trace looks absolutely correct.

Yikes. There are a lot of intermediate wires in the cover trace now... but I guess I'll take it? Oof! 

Also, special thanks to you. I hope this does get fixed without having to do a rewrite, but in the meantime I am definitely unblocked. Thank you!!!

No, that fails BMC :(

Oof. Well, it does work. This is still a workaround, though, right?

Hmm. I'm not sure I follow? In my example, really the only clock I had was that local clock, so it isn't exposed to the top-level module. The other clock...

Additional: I've just learned about the ["A Simpler Connective System"](https://solpahi.wordpress.com/2016/09/20/a-simpler-connective-system/) proposal (20 Sep 2016) that this seems to implement. So I guess these rules are meant to allow either the...