At Oski, we’ve embedded ourselves in the world of Formal verification because we truly believe in the exhaustive nature of Formal to achieve significant confidence in design and verification sign-off.  So, it doesn’t surprise me that Arm’s initial experience with Formal compelled them to employ a much deeper Formal sign-off strategy with their latest design.  The endeavor resulted in a significant amount of and quality bug detection but as with any project, there are lessons to be learned about the best ways to take full advantage of what Formal has to offer.

At the latest Decoding Formal event at Oski, Vikram Khosa of Arm provided user of Formal with a comprehensive look into how Arm is looking to even further improve their Formal verification strategy, but before we go there, let’s give you a brief background on their project and how Formal was used.

On previous designs related to Cortex-A57/A72, Formal was used but with a small Formal team inside Arm sporadically utilizing homegrown methodologies and only piloted testbenches on a few select areas.  Despite this limited amount of Formal use, achievements with Formal were significant enough to prompt deploying a full Formal sign-off methodology on their next Cortex-A design.

The Next Gen project applied a mix of light and focused Formal efforts that not only included sign-off on the verification side to analyze proof depths and track and analyze coverage, but also sought to get the design teams more involved upfront.  Formal implementation started with higher-level planning to map out the scope and list of deliverables for target units spanning the entire CPU including Instruction Fetch, Core, and Memory System with an early estimation of time and resources.  Unit Formal testbench planning used Oski-certified test plans based on a proven Oski methodology.  The block diagram below shows the areas where Formal sign-off was utilized.
(more…)