Thanks for the review!! The integration test has been added.

By the way, I will keep working on circt-bmc until it can accept Chisel-generated circuits. Please let me know if you have any suggestions since I'm new to this tool.

For a small example, we still need the support of:

• seq.firreg
• verif.has_been_reset
• verif.clocked_assume
• verif.clocked_assert

I will open another PR for seq.firreg after this one is merged.
As for the verif.has_been_reset, I'm considering adding a registor to record the circuit has_been_reset or not.
And then maybe adding an option to let bmc assume the reset is true at the first step (or replace initialValues). In this case, we wouldn’t need an extra register.

Cool!

Do you need async resets for the designs with firregs that you're looking at? I guess with synchronous resets you don't need anything new over compreg, but I can imagine async might be a bit more complex (that said, I could also believe that all you need to support them is another multiplexer like you do in this PR that additionally multiplexes between the register output and the reset value. The only unusual case I can think of off the top of my head is one where an async reset starts low, goes high between clock edges, then goes low again, but I think we cover that anyway in circt-bmc's default mode since it evaluates the negedge too. I suspect there'll be a corner case or two that I'm not thinking of anyway).

A register to track whether the circuit's been reset or not sounds sensible to me.

Do you have merge permissions, or should I hit merge on this PR for you?

I don’t need async resets, but you’re right! I will handle it as you said.
Processing async reset on both the posedge and negedge (in default mode) is good enough for BMC. The faster and shorter reset signal transitions are beyond the scope of step-by-step modeling method of BMC.

Yes please merge this! I dont have merge permissions.