Concurrent Verification Experience of Cache Protocol in Real Development of Large SMP Server Product by Using Model Checking
Toru Shonai, Shoichi Hanaki, Yoshiaki Kinoshita · 2013
We have verified the cache protocol by using model checking in real development of the highly multiple-CPU server product. A formal verification engineer abstracted the models for model checking several times through the design process from the protocol specifications written in natural language by the architect team. We discovered actual nine complicated protocol bugs acknowledged by the architects in advance of logic simulation. Some bugs we found were too complicated to be replicated in logic simulation. This effort surely shortened the total design duration. We proved the effectiveness of formal verification of cache protocols in early design phase of real server product development.