x86

Concept

Based on the provided evidence, x86 is a family of microprocessor architectures referenced in multiple verification and fuzzing contexts. Evidence shows that Genesys, a test-program generator framework, has been used to verify large-scale processor families including x86 and PowerPC; that the formal semantics of non-volatile memory in x86-TSO has been studied; that industrial x86 microprocessor implementations have been formally verified at Centaur Technology; and that post-silicon x86 CPUs have been fuzzed via a microcode-guided framework called Fuzzilicon.

First seen 5/27/2026

Last seen 7/6/2026

Evidence 4 chunks

Wiki v2

WIKI

x86

Overview

Based on the provided evidence, x86 is referenced as a family of microprocessor architectures appearing in verification, formal semantics, and post-silicon testing research. The evidence spans DSP test-program generation, formal persistency modeling, industrial formal verification of x86 instruction implementations, and microcode-guided fuzzing of x86 CPUs.

READ FULL ARTICLE →

NEIGHBORHOOD

No graph connections found for this entity yet. It may appear in future ingestion runs.

explore full graph →

RELATIONSHIPS

3 connections

RISC-V ← compares with 88% 1e

RISC-V is presented as a reliable and secure alternative to x86 microarchitectures.

CPU part of → 90% 1e

x86 is a CPU family with complex undocumented behavior.

Genesys ← evaluates 95% 1e

Genesys has been used for verification of the x86 processor family.

LINKED ENTITIES

1 links

Genesys EVALUATES Extracted graph relationship

CITATIONS

7 sources

7 citations — click to expand

[1] Genesys is a test-program generator that has been used for verification of large-scale processor families including x86 and PowerPC. Fast Construction of Test-Program Generators for Digital Signal Processors

[2] A Genesys-based work-model built for the IBM C54XDSP demonstrates that a full test-program generator can be built quickly while improving verification coverage, by reusing a framework validated on architectures such as x86 and PowerPC. Fast Construction of Test-Program Generators for Digital Signal Processors

[3] x86-TSO persistency has been formally studied; a model with stronger persist semantics is equivalent to the POPL'20 Raad et al. model in reachable states, and a sequentially consistent persistency model with a sound mapping to x86 and a data-race-freedom guarantee was developed. Taming x86-TSO Persistency (Extended Version)

[4] Formal methods have been applied at Centaur Technology to verify modern x86 microprocessors, covering instruction decoding, micro-op translation, microcode-ROM traps, and micro-op execution, within a framework combining a theorem prover, verified symbolic simulator, and SAT solvers; the authors report no similar published results for x86 verification. Verifying x86 Instruction Implementations

[5] Fuzzilicon repurposes the x86 microcode-patch interface as a programmable introspection layer, using reverse-engineered microcode patches to instrument internal microcode execution paths and observe execution states such as microcode path transitions at runtime, without RTL access or specialized hardware. Fuzzilicon: A Post-Silicon Microcode-Guided x86 CPU Fuzzer

[6] Fuzzilicon uses a bare-metal, hypervisor-based framework that isolates the device under test, controls its environment, and continuously monitors execution, combined with a serialization oracle that synthesizes semantically equivalent variants of instruction sequences to enable feedback-driven fuzzing of post-silicon x86 CPUs with microarchitectural visibility. Fuzzilicon: A Post-Silicon Microcode-Guided x86 CPU Fuzzer

[7] Fuzzilicon's paper organization includes background on x86 microcode execution, instruction decoding, Red-Unlock mode, and microarchitectural introspection, followed by sections on challenges of fuzzing commercial x86 CPUs, design, implementation, evaluation, discussion, related work, and conclusion. Fuzzilicon: A Post-Silicon Microcode-Guided x86 CPU Fuzzer