MONDAY June 03, 1:30pm - 3:00pm | N262
TOPIC AREA: DESIGN
KEYWORD: VERIFICATION/VALIDATION, FRONT END DESIGN
EVENT TYPE: DESIGNER TRACK
SESSION 5
Stop Wasting your Verification Budget – Know when to use Formal
Chair:
KiranKumar V.M. Achutha - Intel Corp., Bengaluru, India
Organizer:
Roger Sabbagh - Oski Technology, Inc., Ottawa, Canada

How would you verify that your PCIe receiver framer never confused payload data with framing tokens or packet header symbols? Imagine exhaustively testing every possible combination of payload data, packet lengths, modes, link widths and framing errors.

Or, how about verifying that your GPU shader sequencer always fetched, decoded and resolved dependencies between instructions correctly, for all possible types and sequences of instructions – all while simultaneously accounting for exceptions, configuration changes, stalls and control flow events?

What about verifying the correct ordering of register accesses across a CPU pipeline with aggressive out-of-order speculation in the presence of exceptions and flushes?

These are designs with too many corner case scenarios to cover with random or directed test cases. Formal verification is needed to solve hard problems like these. In this session, we present application specific verification challenges and examples of how formal verification has been used to develop practical solutions.


Thank you to our Designer Track Sponsor:


5.1A Novel Approach to PCIe Receiver Framing Checks
 Speakers: Joe Keirouz - Broadcom Corp., San Jose, CA
Vigyan Singhal - Oski Technology, Inc., San Jose, CA
 Authors: Joe Keirouz - Broadcom Corp., San Jose, CA
Vigyan Singhal - Oski Technology, Inc., San Jose, CA
Anant Verma - Oski Technology, Inc., Gurgaon, India
5.2Formal Verification of a GPU Shader Sequencer
 Speakers: Vaibhav Tendulkar - Advanced Micro Devices, Inc., Santa Clara, CA
Chirag Dhruv - Advanced Micro Devices, Inc., Santa Clara, CA
 Authors: Vaibhav Tendulkar - Advanced Micro Devices, Inc., Santa Clara, CA
Chirag Dhruv - Advanced Micro Devices, Inc., Santa Clara, CA
Ashutosh Prasad - Oski Technology, Inc., Gurgaon, India
5.3Effective Formal Solutions to CPU Verification Challenges
 Speaker: Vikram Khosa - Arm, Ltd., Austin, TX
 Author: Vikram Khosa - Arm, Ltd., Austin, TX