Move part of formal proof to the implementation

Move part of formal proof to the implementation

For induction, some state has to be synchronized with the
device under test. Make the device itself responsible for checking
this, to avoid exposing its internal workings, and making the proof
more generic.
This is done for PhasedDualPortRegfile, the rest will follow.