Tom Verbeure recently wrote an article on using Formal Verification tools to discover the cause of a bug in a communication protocol between 2 boards. After a board respin, very occasionally a phantom packet would be received - even if the boards were disconnected.
It was one of those situations where the original author of the design was long gone, and the code base was quite large. How would you go about debugging one of these annoying sporadic problems? Rare and seemingly random bugs are among the hardest to pin down, and either involve capturing a huge amount of data with a logic analyser or throwing a lot of random data in simulation.
As Tom says in his article, “it’s never too late to use formal verification: it isn’t only useful during the verification stage of a project, it can also be extremely useful to root cause a bug in an existing system”.
He was able to write a single cover statement that would produce a single trace of the problem:
cover(higher_level_packet_decode_valid && !low_level_packet_seen);
A few seconds later he was looking at a short trace that showed exactly what was necessary to produce the bug. The rest was easy.
Be sure to read the whole article to get the low down on the specifics of the bug and how he was able to put Formal tools to use in a debugging context. We particularly liked his conclusions!
Tom Verbeure is active on twitter and has written other articles you can find here.