Formal Verification: A Case Study

Shahid Ikram
Professor
Cavium Networks
Date and Time: 
December 6, 2013 - 11:15am - 12:05pm
Location: 
Gunness Student Center Conference Room
Host: 
Maciej Ciesielski
Contact the host: 
ciesiel@ecs.umass.edu

Formal Verification is one of the tools used in design-verification efforts of hardware as well as software. This talk will give a brief overview of Formal Verification followed by a case study of using it to model and verify a cache coherence protocol.  The study will cover the requirements of the protocol verification, their modeling, verification and description of the bugs found. In the process, we will look at an academic FV tool and a commercial FV tool and their usage in our case study.

Bio: 

Dr. Shahid Ikram has a Ph.D in Computer Engineering from Syracuse University with a concentration in Process Algebras and their application to Instruction set architecture design and verification. He initially, worked in academia, teaching for few years before joining Alpha processor team in Shrewsbury, MA. The group was later acquired by Intel Corp, and Dr. Shahid spent 10+ years doing formal verification, dynamic verification, coverage and tool-development assignments. Currently, Dr. Shahid is employed at Cavium Networks, doing multichip protocol verification and helping dynamic verification teams.