Presentation
Architectural Formal Verification of Configurable Address Translation Logic for Early Bug Exposers
DescriptionHighly configurable, hash‑based address translation logic is central to modern memory subsystems, enabling scalability, parallelism, and load balancing(fairness) across multiple clients and lanes. However, the resulting configuration and address spaces grow far beyond what simulation can feasibly explore. Even subtle specification‑level errors in hashing or decoding semantics can silently propagate into RTL and system software, leading to persistent data corruption and costly late‑stage debug. This paper presents an architectural‑level formal verification methodology that shifts correctness assurance left, before RTL development. The intended hash and decoder behaviour is captured using an executable architectural reference model, independent of RTL implementation. Architectural intent is expressed as global invariants—such as no aliasing, load balancing(fairness), address safety, lane conflict avoidance, and controlled error propagation—and proven symbolically across all legal configurations and the full address space. The same reference model and proven invariants are then reused directly at the RTL level to perform invariant‑guided equivalence checking. By integrating these already verified block‑level properties as assumptions in the existing end‑to‑end RTL formal environment, system‑level correctness is validated without building a new formal setup or re‑verifying internal blocks. This approach uncovers mis‑integration bugs while avoiding over‑constraint. Applying this methodology exposed multiple critical specification bugs prior to RTL. The results demonstrate a scalable, reusable, and production‑ready formal flow for complex memory systems.
Event Type
Engineering Presentation
TimeTuesday, July 284:45pm - 5:00pm PDT
LocationSeaside Ballroom A