A formal proof is needed which demonstrates the effectiveness and
correctness of the out-of-order execution engine: register dependencies,
memory dependencies, and the use of a "revolving door" set of SR Latches.
This is tricky because SR NOR Latches are not normally used in "industry"
designs. Consequently we need to formally prove that the HDL functions