A computer implemented method for the post-silicon validation and debug of a digital hardware system, wherein: the digital hardware system is a System on a Chip having at least one programmable processor; and the post-silicon validation method executed by the computer is a Symbolic Quick Error Detection (Symbolic QED) method employing bounded model checking that operates by inserting, automatically and systematically a number of change detectors into the digital hardware system during a design phase of that hardware system; running, by a QED module integrated with a fetch unit, a number of quick error detection tests using QED-compatible traces on that hardware system having the inserted change detectors wherein the change detectors record debug information during the running, the QED-compatible traces comprising a sequence of inputs that are valid instructions obtained from an instruction set architecture of the programmable processor, wherein register and memory spaces are divided into two halves, one for original instructions and one for duplicated instructions, the sequence of original instructions and duplicated instructions execute in the same order, and a comparison between an original register R and its corresponding register R' occurs only if the original and duplicate instructions are in sync; determining, by the computer performing the BMC, whether an error (bug) was detected by the QED tests, wherein an initial state of the BMC is a QED-consistent state wherein a value of each register and memory location allocated for original instructions matches the corresponding register or memory location for duplication instructions such that no false counter-examples are generated; and if a bug was detected by the QED tests then localizing the detected bug and generating a minimal bug trace having less than 10 instructions. the digital hardware system is a System on a Chip having at least one programmable processor; and the post-silicon validation method executed by the computer is a Symbolic Quick Error Detection (Symbolic QED) method employing bounded model checking that operates by inserting, automatically and systematically a number of change detectors into the digital hardware system during a design phase of that hardware system; running, by a QED module integrated with a fetch unit, a number of quick error detection tests using QED-compatible traces on that hardware system having the inserted change detectors wherein the change detectors record debug information during the running, the QED-compatible traces comprising a sequence of inputs that are valid instructions obtained from an instruction set architecture of the programmable processor, wherein register and memory spaces are divided into two halves, one for original instructions and one for duplicated instructions, the sequence of original instructions and duplicated instructions execute in the same order, and a comparison between an original register R and its corresponding register R' occurs only if the original and duplicate instructions are in sync; determining, by the computer performing the BMC, whether an error (bug) was detected by the QED tests, wherein an initial state of the BMC is a QED-consistent state wherein a value of each register and memory location allocated for original instructions matches the corresponding register or memory location for duplication instructions such that no false counter-examples are generated; and if a bug was detected by the QED tests then localizing the detected bug and generating a minimal bug trace having less than 10 instructions.