Formal Verification Engineer

Role Summary

AMD is seeking a Senior Formal Verification Engineer to own formal verification for complex GFXIP blocks and contribute to subsystem sign-off in partnership with FV tech leads. You will work closely with design and architecture to translate specifications into robust properties, improve convergence, and raise verification quality for high-impact blocks.

Experience Level

Level - Mid-Career

Responsibilities

• Own formal verification plans and execution for one or more complex GFXIP blocks; support subsystem sign-off with guidance from FV tech leads.
• Develop properties and constraints from architectural/design specs; partner with designers to clarify intent and improve verifiability.
• Build and maintain high-quality formal testbenches and assertion suites; ensure property soundness, non-vacuity, and constraint hygiene.
• Apply advanced formal techniques (abstraction, cutpoints, invariants, assume-guarantee, cone-of-influence reduction) to improve convergence and throughput.
• Drive closure on formal quality metrics for assigned blocks: proof convergence, property completeness, functional/code coverage; contribute to app-based checks (connectivity, CDC/RDC, X-prop) and equivalence checking as needed.
• Debug counterexamples efficiently; provide actionable feedback and collaborate on RTL/design fixes; prevent regressions through reviews and targeted automation.
• Contribute to methodology and automation via reusable assertion libraries, scripts, checklists, and CI integrations; share learnings across the team.
• Provide guidance to junior engineers through reviews, pairing, and knowledge sharing.
• Document verification plans, assumptions, findings, and lessons learned; provide clear status updates and risk/mitigation plans to stakeholders.

Requirements

• Digital design/verification with 2–4+ years focused on formal verification.
• Proven ownership of formal verification for complex blocks in GPU/CPU or high-performance IP; contribution to subsystem-level sign-off.
• Proficiency with formal tools: Cadence JasperGold, Synopsys VC Formal; familiarity with SEC and formal apps (connectivity, CDC/RDC, X-prop, deadlock/liveness).
• Strong SystemVerilog Assertions (SVA) skills; experience deriving properties from specs and building reusable assertion frameworks.
• Hands-on convergence techniques and counterexample debug; experience with abstraction/invariants/assume-guarantee.
• Scripting skills (Python, TCL); experience with automation and CI to scale formal runs and metrics.
• Solid understanding of processor/GPU microarchitecture, memory systems, interfaces, and power/clock/reset domains.

Education Requirements

Bachelors or Masters degree in Computer Engineering/Electrical Engineering.