Xekri

I found that if the `x` signal in the example above is in a separate module, nMigen gives you a warning, similar to this: ``` /mnt/f/riscv_pysim/sequencer_card.py:32: DriverConflict: Signal '(sig _pc)'...

I'd rather not, since that solution requires me to know what the RTLIL name of the signal is, and to manually add such a line to the sby file, for...

Oh I wasn't ignoring it. I thought you meant that I should use it to get around the fact that it can't be done in any other way. I'd rather...

But then how would I specify that I want some signals to be initialized (e.g. internals), and some to not be initialized (e.g. the states I'm really interested in initializing...

I'm grateful that you're looking into this. Thank you!!!

BTW, I *suspect* that what should be happening is that Past, Fell, Rose, Stable, and Sample should be forbidden in the combinatorial domain, based on Claire's documentation for SymbiYosys: >...

@cr1901 It's pretty much what I concluded. At issue here is, I think, nMigen, not SymbiYosys, although I could be wrong.

BTW, I replaced `m.d.comb` with `m.d.sync` for the cover and asserts, and then I generated the verilog via `generate -t v`, and manually edited the file to include `(* gclk...

Yes, that was also my conclusion. So aside from outputting that diagnostic, the second issue here is that we need a way to specify the `gclk` annotation for the default...

Hmm, did I put it in the right place? BMC is still failing: ``` [tasks] cover bmc [options] bmc: mode bmc cover: mode cover depth 10 multiclock on [engines] smtbmc...