July 23, 2009 -- Bugs in RTL code are problematic, but a bug in an architectural specification can be catastrophic. If the bug remains undetected until post-silicon debugging, the design process essentially starts all over again. Thus, it’s crucial to move the verification process as far forward as possible.
With that motivation in mind, engineers at Sun Microsystems recently applied formal verification to an application that commercial tools have not generally addressed—architectural-level protocol verification.
Sun’s engineers modeled a complex cache-coherence protocol, with parallelism and multi-threading, for a high-performance processor. They also used a commercial formal property-checking tool from Jasper Design Automation to verify this protocol. Initially, Sun engineers used Murphi, an academic tool developed for protocol verification in the 1990s that includes a modeling language and a state model checker. Although specifically designed for architectural verification, Murphi lacked the capacity to thoroughly verify the protocol. It soon became apparent that for architectural verification, a commercial tool with much more powerful underlying formal engines would be needed.
By Norris Ip, Scott Meeth, and Holly Stump. (Meeth is a design/architecture formal verification engineer at Sun; Ip is Director of Engineering at Jasper Design Automation; and Stump is Vice President Of Marketing at Jasper Design.)
This brief introduction has been excerpted from the original copyrighted article.
View the entire article on the Electronic Design Magazine website.
Read more about
Jasper Design Automation