Formal verification of a SONET data stream processor