Hybrid Verification of Protocol Bridges

It´s usually necessary to apply formal verification on very small modules or else be content with bounded proofs on realistically large modules. But there is no denying that despite its capacity problems, formal verification has its strengths and utility and is a complementary technique to simulation. Used judiciously, simulation and formal techniques can complement each other´s strengths, thereby balancing their respective weaknesses. There are different ways to combine these two techniques. In this article, we present two case studies of the application of one such technique: the hybrid verification of a serial protocol. We chose this example because of serial protocols´ added complexity compared to parallel protocols. Both case studies involve the same serial protocol (I²C) but demonstrate different aspects of its verification. Selection of the same protocol in both case studies also demonstrates the tremendous value of reuse in formal verification.