Definition
In the evidence provided, symbolic simulation appears as a technique used in formal verification of pipelined microprocessors. Burch and Dill's key contribution was to show that an abstraction function, mapping microprocessor states to architectural states, could be computed automatically by symbolically simulating the microprocessor while it flushes instructions out of the pipeline. [symbolic-simulation-computes-abstraction]
Role in pipelined microprocessor verification
Formal microprocessor verification compares a pipelined implementation with an Instruction Set Architecture (ISA) model. The ISA model describes the effect of each instruction on architectural state, including registers, the program counter, and memory, under a sequential execution model. Pipelined implementations overlap multiple instructions, so verification must show that the pipelined execution faithfully implements the sequential ISA semantics for all possible instruction sequences. [isa-and-pipeline-verification]
In the Burch-Dill approach, the verifier proves that an abstraction function (\alpha) maps microprocessor states to architectural states and that this mapping is maintained by each cycle of processor operation. Symbolic simulation is used to compute this abstraction function by modeling the processor as it flushes its pipeline to a quiescent state. [abstraction-function-maintained]
Correspondence checking formulation
For a single-issue microprocessor, the verification task is described as proving equivalence between two symbolic simulations:
- The pipeline is flushed, and then a single instruction is executed in the ISA model.
- The pipeline operates for one normal cycle, and then the pipeline is flushed.
The cited source calls this verification approach correspondence checking. [correspondence-checking-equivalence]
Abstraction level
The evidence associates the Burch-Dill method with term-level modeling. In term-level modeling, details of data representations and operations are abstracted away, data values are treated as symbolic terms, and components such as instruction decoders and ALUs can be represented with uninterpreted functions. This abstraction lets the verifier focus on pipeline control logic rather than precise bit-level behavior. [term-level-modeling]
Verification scope and limitation
The cited source states that Burch-Dill verification proves a safety property: each processor cycle has an effect consistent with some number (k) of ISA-model steps, including (k = 0). This accommodates stalls and canceled instructions, but it also means a deadlocked processor could pass the safety check; liveness must be verified separately. [safety-not-liveness]