Questions about DFFE cells and retiming

[leeway64]

I was reading this Reddit post about clock domain partitioning, and I just have a few questions about it. I've copied the relevant part:

PS: I don't recommend performing standard cell mapping using abc -dff -D on a design with DFFE cells in it. The additional clock domain crossings introduced via the DFFE cells can prevent individual ABC instances from seeing all timing paths from driving FF to driven FF, rendering the -D option useless.

1. I understand that abc -dff -D <picoseconds> will perform retiming. Will abc not retime a design with DFFE cells in it?
2. If that's the case, then are there any options or workarounds for retiming DFFE cells?
3. Why do the DFFE cells introduce clock domain crossings?
4. This may or may not be related, but I've been having issues with logical equivalence checking with DFFE cells. Is it possible to use commands like equiv_simple and equiv_induct to check for logical equivalence in designs with DFFE cells, or are there additional assumptions I need to make first to simplify the design?

Any help would be appreciated. Thank you so much!

[leeway64]

Does anyone have any feedback or advice? I'm open to suggestions! 😄