Posts Tagged ‘#ARM’
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 »
Thursday, September 24th, 2015
On the radio yesterday, we heard that the song “Happy Birthday To You”, one of the most widely sung tunes in the world, was ruled by federal judge George H. King to finally be in the public domain!
This welcome news seems to come at the right time, as Oski Technology plans to celebrate the second anniversary of the Decoding Formal Club at our quarterly meeting on October 21 at Computer History Museum, in Mountain View.
Since it was founded in October 2013, the Decoding Formal Club has drawn the attention of engineers, designers and verification managers. In a relatively short time we have covered much ground, and become a forum where formal knowledge and experience can be shared among the growing community of formal enthusiasts. In turn, Oski’s featured presentations have covered many aspects of formal sign-off methodology: Bounded Proof, Abstraction Models, Formal Test Planning, End-to-End Checkers and Constraint Management.
(more…)
Tags: "Decoding Formal" Club, #ARM, formal analysis, formal verification methodology, Oski "Break the Testbench" Challenge 2015 DAC, Oski Technology, Oski Verification Challenge, Prashant Aggarwal, Vigyan Singhal
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 »
Friday, January 16th, 2015
According to statistics published in 2014 by the University of Scranton in Pennsylvania in the Journal of Clinical Psychology, 45% Americans usually make New Year’s Resolutions. And people who explicitly make resolutions are 10 times more likely to attain their goals than people who don’t.
The largest resolution category –– 47%, is related to self-improvement and education. This is me, trying to squeeze time in my busy schedule to work out and keep my brain sharp by learning new things. This year, our family joined a new health club where I can watch TED Talks as I walk, and I am embarking on a learning journey with my sixth grader on Machine Learning & Robot Design. It has been fun!
As the Director of Marketing at Oski Technology, my New Year’s Resolution for Oski is simple –– Treading Deep into Formal. In the past 18 months, we successfully hosted five Decoding Formal Club events where we, and our invited guests, shared some of the deepest knowledge and practical experiences about formal that cannot be found elsewhere.
We have covered many deep formal topics such as Abstraction Models, Bound Analysis, End-to-End Checkers, and Formal Test Planning, all with the goal to achieve Formal Sign-off. Invited guests from industry formal leaders, such as NVIDIA and Broadcom, shared their experiences deploying formal. With deep formal talks, opportunities for formal networking, good food and cool gifts, Decoding Formal Club has become a magnet that attracts formal enthusiasts. It is where deep formal learning happens.
Carrying on the theme of Treading Deep into Formal into 2015, our first Decoding Formal Club meeting will be held Monday, February 9, from 11:30 a.m. until 4:15 p.m. at our usual location, the Computer History Museum in Mountain View.
We have an agenda packed with Deep Formal Talks and lots of fun! It will include talks by:
- Vigyan Singhal, chief executive officer of Oski Technology, who will share another important topic in Formal Sign-off –– constraint management.
- NVIDIA Principal Engineer Jon Michelson, co-author of “The Art of Verification with SystemVerilog Assertions” and “The Art of Verification with Vera,” who will present “A Practical Viewpoint on Liveness versus Safety.”
- Ross Weber, Staff Design Engineer at ARM and author of the best paper award at the Jasper User Group 2014, who will discuss formal achievements at ARM.
While attendees tread deeply into the formal space, we will bring them back with a special invited guest Cliff Stoll. His TED Talk, “The Call to Learn” inspired us to offer one of his Acme Klein Bottles as a giveaway. And with the Chinese New Year coming February 19, attendees will be in for Chinese flair and other surprises.
The event space can hold only 40 people, and we intentionally keep the event small to offer the best learning and networking experience. Our goal is to make it the best four hours of an attendee’s work week.
Come and join us as we Tread Deep into Formal in 2015. It will be exciting!
Visit the Decoding Formal registration page, here.
Tags: "Decoding Formal" Club, #ARM, Cliff Stoll, constraints, Jin Zhang, Jon Michelson, NVIDIA, Oski Technology, Ross Weber, Vigyan Singhal
No Comments »
Friday, February 28th, 2014
The countdown to DVCON 2014 has begun! With more exhibitors and attendees than ever before, new programs and technical sessions, longer exhibit hours, DVCON 2014 is shaping up to be another outstanding event for the industry.
At Oski Technology, we are excited to offer many opportunities to connect with verification experts in the industry at DVCON – share ideas, discuss problems and solutions related to formal technology and formal sign-off methodology.
• Monday March 3rd 5:00 – 7:00pm, Oski will join the inaugural DVCON Booth Crawl and offer healthy stacks – nuts, veggie sticks and wine, while we enjoy great conversations. Come and chat at the Oski booth #305. (more…)
Tags: #ARM, DVCon, DVCon 2014, formal and semi-formal techniques, formal sign-off, formal verification of cache coherency with ARM ACE/CHI protocols, Samsung Electronics, sign-off with bounded formal verification proof
No Comments »
|
