Posts Tagged ‘formal sign-off’
Monday, November 6th, 2017
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…)
Tags: #ARM, Cortex-A, formal sign-off, formal verification
1 Comment »
Wednesday, March 29th, 2017
What better way to celebrate the arrival of spring than another meeting of the Decoding Formal Club! The Decoding Formal Club is a forum for formal verification enthusiasts, pioneers, leaders and friends who work to promote the sharing of ideas, advancement of formal verification technology, and adoption of formal sign-off methodology within the industry. On Tuesday, March 21, the club met to hear presentations from Oski, Nvidia and Arteris.
Vigyan Singhal, Oski CEO and formal verification visionary, started us off by introducing the concept of architectural formal verification. Some system level requirements are, by their very nature, well suited for formal verification. Cache coherence, absence of deadlocks and security features are examples of things that we would want to verify with formal. However, the complexity of today’s systems makes it impractical to do so at the RTL level. Instead, Vigyan talked about how Oski uses abstract components to build a system-level model that can be successfully analyzed by formal verification.
 Many in attendance liked this approach but also noted the challenge of ensuring that the behavior of the abstract components matches the implementation in RTL. Vigyan explained how Oski’s methodology has that covered when the properties of the abstract models are validated against the RTL designs to close the loop.
Tags: "Decoding Formal" Club, architectural formal verification, best practices formal verification, formal analysis, formal sign-off, formal verification
No Comments »
Friday, June 3rd, 2016
If you are attending the Design Automation Conference (DAC) in Austin, Texas, June 5-9, and need a good reason to stay an extra day, look no further. Oski Technology is offering a one-day primer on advanced formal verification techniques at the DAC Decoding Formal one-day training, “Achieving Formal Sign-off”, on Thursday, June 9, from 10 a.m. until 5 p.m. at the Hilton Hotel, Austin.
(more…)
Tags: "Decoding Formal" Club, #53DAC, advanced formal training, formal analysis, formal sign-off, formal verification, formal verification methodology, Oski Technology, Vigyan Singhal
No Comments »
Monday, May 2nd, 2016
Formal sign-off is possible with today’s technology and methodology. But to get to formal sign-off takes an understanding of what is possible with formal verification, and an immersion in ongoing practice with formal methods and techniques. Moreover, early experiences with formal can determine later success with formal verification and sign-off. Even with a deep knowledge of a formal verification tool and extensive training from the tool vendor, exponential formal proof complexity often gets in the way of exhaustive coverage. Often what is needed is training in formal verification methodology and formal test planning that includes an exhaustive list of end-to-end checkers, as well as the mastering of formal techniques that help overcome complexity. (more…)
Tags: #53DAC, advanced formal training, formal analysis, formal sign-off, formal verification methodology, HarGovind Singh, Oski Abstraction Models, Oski Technology, Pippa Slayton
No Comments »
Thursday, March 24th, 2016
In December 2015, Oski challenged formal users to build the fastest testbench to solve our Oski Formal Puzzler – the Chessboard Challenge, Berkeley Math Circle Monthly Contest 8, 2011, proposed and designed by Evan O’Dorney, three-time Putnam Fellow. Jesse Bingham from Intel submitted the winning entry, as was announced during a presentation at the recent meeting of the Decoding Formal Club in Santa Clara, CA on February 29, 2016. This was an opportunity to promote the adoption of formal verification across the semiconductor industry, and share formal techniques by showing how they might be used to solve a fun formal puzzle. (more…)
Tags: "Decoding Formal" Club, chessboard challenge, formal analysis, formal sign-off, formal verification, Oski Technology, Pippa Slayton, Vigyan Singhal
No Comments »
Monday, February 22nd, 2016
Formal verification of hardware designs has been around for more than 25 years. Commercial tools, for example from AT&T Bell Labs and IBM, started appearing in the 1990s. It’s only recently that formal verification has been adopted into design and verification flows, due to a number of reasons. It’s harder to learn than simulation or emulation because of its complexity, and it takes time for a verification engineer to become proficient in using it. Formal verification experts typically learn 100s of different techniques over the course of their careers.
Now that we are in the era of formal verification, an important new role is emerging –– the Formal Verification Program Leader (FV Program Leader). (more…)
Tags: formal sign-off, formal verification, formal verification methodology, Formal Verification Program Leader, organization, Oski Technology, post-mortem analysis, progress metrics, sign-off process, test planning, training, upskilling, Vigyan Singhal
No Comments »
Friday, November 13th, 2015
The recent Decoding Formal Club meeting hosted by Oski Technology on October 21, 2015 at the Computer History Museum in Mountain View celebrated the club’s 2nd anniversary with a “back to the future” twist.
While many of the predictions in the movie “Back to Future Part II” did not come true on October 21, 2015, the day of “the future” to which Marty McFly and Doc Brown time travel in a flying silver DeLorean sports car, that didn’t deter us from inviting attendees from Apple, ARM, Arteris, Broadcom, Ericsson, Google, Imagination, Microsoft, NVIDIA, Palo Alto Networks, Qualcomm and others to make some timely predictions for formal verification in 2025. The group was comprised of formal experts with years of experience, as well as engineers who are new to formal verification, so the predictions for 2025 were daring, but quite possible.
(more…)
Tags: "Decoding Formal" Club, formal sign-off, formal verification, Oski Technology, Pippa Slayton
No Comments »
Wednesday, September 9th, 2015
Gabe Moretti of Chip Design used several points from Jin’s blog post below, in his recent article titled, “Design and Verification Need a Closer Relationship.” The article can be found at: http://bit.ly/1fGyXW2
Today, verification engineers have a whole arsenal in their tool kit in order to combat hidden bugs in the design. Different verification techniques render different working relationship with the designers.
Formal verification is a white-box verification technique, which means formal engineers need to have a good understanding about the internals of the design in order to do effective formal verification. Therefore, formal engineers and RTL designers naturally have a much tighter working relationship than other disciplines.
First, a sound verification methodology should allow equal contribution from all effective techniques, which includes leveraging the exhaustiveness of formal to sign-off on design blocks that are harder to verify with simulation. The block partition between formal and simulation should be clean to simplify the effort on both ends. To achieve that, formal engineers should participate in the architectural planning and exploration stage of design development in order to help influence decisions regarding design partition and block interface. A well-partitioned design with a clean interface will make the decision on where to apply formal, as well as the actual formal verification tasks, much easier.
(more…)
Tags: #52DAC, best practices formal verification, Break the Testbench Challenge, formal sign-off, Oski Technology
No Comments »
Friday, June 19th, 2015
The story of Louis Zamperini, as told by Laura Hillenbrand in “Unbroken: A World War II Story of Survival, Resilience, and Redemption”, is a great testimony of the strength of human spirit. Going through unimaginable catastrophes, including drifting 47 days on the open sea with leaping sharks, thirst, starvation, and machine gun attack from a bomber plane, as well as enduring 3 years under severe and brutal conditions as a POW in Japan, Zamperini emerged unbroken with grace, humanity and love.
This is such an inspiring story that when I thought about writing about Oski DAC 2015 “Break the Testbench” Challenge results, the word “unbroken” came to mind. While this is no comparison in its scale to the story of Zamperini, the word “unbroken” succinctly summarizes the challenge result.
(more…)
Tags: "Decoding Formal" Club, #ARM, formal sign-off, Oski Technology, Vigyan Singhal
No Comments »
Saturday, June 6th, 2015
Oski Decoding Formal Events are usually hosted at the Computer History Museum in Mountain View and have attracted lots of formal enthusiasts in the bay area. Deep formal talks from Oski, lectures given by formal experts from different companies, good networking, cool gifts and museum tours have become the signature of these events that formal engineers look forward to, every quarter.
To reach out to formal enthusiasts around the world and create a bigger event than usual, the 2015 Q2 Decoding Formal event will be hosted at DAC. Our theme is proving completeness of End-to-End Formal for Sign-off.
(more…)
Tags: #52DAC, formal sign-off, formal verification, formal verification methodology, Oski Technology, Vigyan Singhal
No Comments »
|
