Verification of Pipelined Microprocessors by Comparing Memory Execution Sequences in Symbolic Simulation