Posts Tagged ‘formal verification’
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.
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.
Wednesday, February 15th, 2017
I recently started to develop an appreciation for the sport of cricket during our Oski company-wide, off-site meeting in beautiful Udaipur, India. Before that, if you had mentioned cricket, I would be more likely to think of the bugs I hear chirping on summer nights and that sometimes find their way into my garage.
John Wright speaks at the Oski off-site
However, that began to change on January 26, 2017, when Oski employees were treated to a talk by legendary cricket player and coach, John Wright. Wright was propelled to stardom when he enjoyed a successful 5-year stint as the first foreign coach of the Indian national team between 2000 and 2005. With the support of Indian captain, Sourav Ganguly, he transformed the Indian cricket team from a group of super-talented individuals, but under-achievers as a team, to consistent world champions. Highlights included beating the Australian juggernaut, who were on a run of sixteen consecutive test wins, and beating Pakistan on their home turf for the first time in more than 50 years.
Interestingly, it was not through a new team system nor by adding new individual skills that this was accomplished. As an outsider, he succeeded against all odds by a series of small, thoughtful behavioral changes. Let’s examine these changes and the lessons we can learn from them as formal verification engineers.
John Wright answers questions after his talk
- Team First
“Don’t do anything to hurt the team”, says Wright. A winning team must have good chemistry. They must portray an image of being the model team. That means individuals must prioritize the team’s schedule and not keep everyone else waiting. It means warming up as a team before games; treating each other with respect; having a positive attitude, while not being afraid to deal with the negative. This is the responsibility of all team players, but the tone is set by the leaders, starting with the team captain and coach.
Monday, December 12th, 2016
It’s undeniable: I am a newcomer to the formal verification scene. As one of the newest members of the Oski team, I didn’t know what to expect when I attended the Oski Decoding Formal Club meeting on October 11th. Oski hosted the event at the acclaimed Parcel 104 Restaurant in the Santa Clara Marriott hotel. The ever popular event was sponsored by Synopsys, and provided attendees from semiconductor companies like Apple, Cavium, Cisco, Intel, NVIDIA, Qualcomm, Western Digital and Xilinx with a great opportunity to network with other formal verification experts and engineers. Our taste buds were treated to a delectable meal made with locally harvested and sustained California ingredients, a Parcel 104 specialty, while Mandar Munishwar (Qualcomm), Ankit Saxena (Oski) and Vigyan Singhal (Oski) engaged our minds with presentations on intriguing formal topics.
Ankit Saxena (Oski) started off the series with a deep dive into “Verifying the Datapath for an AMD Processor”, which he worked on jointly with Sankar Gurumurthy (AMD), Farhan Rahman (AMD) and Ashutosh Prasad (Oski). Ankit’s talk described how data transform designs such as complex multipliers and dividers can be formally verified. View talk here.
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.
Tuesday, May 17th, 2016
As in any engineering endeavor, formal verification involves engaging individuals in many different roles, often including formal managers and, given the technically deep and complex nature of FV, nearly always one or more formal experts. The manager of the formal verification effort on a project may have formal as his or her primary or sole responsibility, or may manage multiple aspects of verification (e.g. both simulation and FV). However, even a full-time formal verification manager may or may not drive the overall formal program in their company or organization.
In part one of this discussion, I talked about the emerging role of the Formal Verification (FV) Program Leader, an individual who enables and drives the formal process by navigating organizational dynamics, understanding designs and their verification complexities and schedules, developing and presenting ROI trade-offs, etc.; all to help achieve project goals. I listed six aspects of this role that the FV Program Leader must master in order to effectively lead the adoption and deployment of formal verification: Organization, Training and Upskilling, Test Planning, Progress Metrics, Sign-off Process, and Post Mortem Analysis.
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…)
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…)
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.
Wednesday, August 12th, 2015
EDA’s verification market segment is not the only place where something’s named for the Cal (University of California, Berkeley) mascot Oski. A Blue and Gold Fleet boat named Oski sails out of Pier 39 in San Francisco and takes visitors around the Bay and Alcatraz.
When I saw the Oski pulling away from the pier, I couldn’t help but draw an analogy between Oski Technology’s mission and the choppy waters the boat was heading into on that sunny day. Sunny days and choppy waters are something verification engineers can face on a daily basis. Verification tasks are so challenging in today’s for system-on-chip (SoC) designs that verification alone takes more than 60% of the project cycle. What’s more, simulation alone for SoC designs will leave large holes for bugs to sneak through, all the way to silicon. The challenge of verification actually is more daunting than the choppy waters of San Francisco Bay.