Formal Verification: A Case Study
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.
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.