Overview

Symbolic QED is a verification-oriented test-generation approach for processor designs. The available evidence describes it as an approach that generates minimal tests for verification, including post-silicon verification, by using a formal model of the pipeline.[1]

Role in verification

Symbolic QED is presented in the TestRIG paper as "another approach" in the broader space of processor verification and test generation. In that comparison, TestRIG emphasizes randomized direct instruction injection and sequence shrinking, while Symbolic QED is distinguished by its use of a formal pipeline model to generate minimal verification tests.[1]

Evidence status

The supplied evidence is limited to a mention in the paper Randomized Testing of RISC-V CPUs using Direct Instruction Injection. No further implementation details, supported ISAs, algorithms, or tool interfaces are provided in the supplied material.