Is there a way to pull out from a module a vector which represents all the DFFs in the module and it's submodules

[Topi-ab]

For formal verification, I could use a feature which allows me to instantiate two instances of the same module, and enforce them into a equal, but random, state, and then analyzing how the two modules deviate from each other during clock cycles.

Is there easy way to export an extra signal out from module, which would be a bitvector of all internal DFFs' outputs?