Decoding Formal Case Studies

SoC – All Domains

Erik Seligman: Logical Paradoxes, Mathematical Oddities, and Lessons for Formal Verification

Arteris IP:  Architectural Formal Verification of Cache Coherent Protocols

NVIDIA:  Architectural Formal Verification of Coherency Models

Arteris IP:  Formal Sign-Off of a Configurable Cache Controller

CPU

Arm:  Lessons learnt from a deployment of sign-off formal on a high-performance ARM CPU

AMD (by Oski):  Verifying Datapath for an AMD Processor

Rambus:  Meltdown and Spectre

GPU / AI

Qualcomm:  Formal Sign-off Meets Real-World Tapeout Schedules

AMD:  Formal Verification of a GPU Shader Sequencer

PCIe / Ethernet

Broadcom:  A Novel Approach to PCIe Receiver Framing Checks

Wireless

Qualcomm:  Architectural Formal Verification of System-Level Deadlocks

Networking

Fungible:  Formal Verification of a Resource Allocator Unit

Cisco:  From Formal Verification Training to Methodology Development for Networking Designs

Cavium:  Methodology for Formally Verifying Software Defined Networking Silicon