Two recently announced vulnerabilities in major processor platforms should remind us that bugs don’t organize themselves to appear only in domains we know how to test comprehensively. Both Meltdown and Spectre (the announced problems) are potential hardware system-level issues allowed by interactions between speculative execution and cache behaviour under specialized circumstances.
Finding hardware weaknesses among highly complex interactions is where formal-proving excels, but common belief is that formal analysis on hardware systems of this complexity is beyond the reach of today’s tools, which are typically bounded to block/IP-level proving. This article highlights how to use formal verification for system level verification.
Find out how T&VS Formal Verification techniques helps to improve the quality of Verification.