During post-silicon validation and debug, manufactured integrated circuits (ICs) are tested in actual system environments to detect and fix design flaws (bugs). Existing post-silicon validation and debug techniques are mostly ad hoc and often involve manual steps. Such ad hoc approaches cannot scale with increasing IC complexity. We present Symbolic Quick Error Detection (Symbolic QED), a structured approach to post-silicon validation and debug. Symbolic QED combines the following steps in a coordinated fashion: 1. Quick Error Detection (QED) tests that quickly detect bugs with short error detection latencies and high coverage. 2. Formal analysis techniques to localize bugs and generate minimal-length bug traces upon detection of the corresponding bugs. We demonstrate the practicality and effectiveness of Symbolic QED using the OpenSPARC T2, a 500-million-transistor open-source multicore System-on-Chip (SoC) design, and using "difficult" logic bug scenarios that occurred in various state-of-the-art commercial multicore SoCs. Our results show that Symbolic QED: (i) is fully automatic (unlike manual techniques in use today that can be extremely time-consuming and expensive); (ii) requires only a few hours in contrast to manual approaches that might take days (or even months) or formal techniques that often take days or fail completely for large designs; (iii) generates counter-examples (for activating and detecting logic bugs) that are up to 6 orders of magnitude shorter than those produced by traditional techniques; and, (iv) does not require any additional hardware.