Formal verification of iterative algorithms in microprocessors