Correspondence checking formally verifies that a pipelined microprocessor realizes the serial semantics of the instruction set model. By representing the circuit state symbolically with Ordered Binary Decision Diagrams (OBDDs), this correspondence checking can be performed directly on a logic-level representation of the circuit. Our ongoing research seeks to make his approach practical for real-life microprocessors.