Archive for the ‘Uncategorized’ Category
Wednesday, March 7th, 2018
Every year for the last nine years teams of researchers and software developers have come together to compete in the Hardware Model Checking Competition (HWMCC). This contest pits some of the brightest minds in design and verification against each other along with the solvers they have developed. Each team has worked tirelessly over the course of the past year to develop their solver and get it ready for the big day.
Vigyan Singhal (center), President and CEO of Oski, presenting the award at the HWMCC Award Ceremony to ABC member, Yen-Sheng Ho (far right). : Armin Biere, organizer of the HWMCC Competition shown far left.
The competition boasts benchmarks in three categories including single safety property track, liveness property track, and deep bound track of which Oski is a sponsor. The benchmarks come from a combination of missed benchmarks by competitors in previous years’ competitions and from leading companies in industry like Oski that directly relate to the most complex issues of the day. It is this combination of benchmarks that pushes these teams to develop solvers so robust in nature that after the competition many of the attributes are adopted by the large system houses to help tackle industrial strength challenges.
Of all the teams competing in the HWMCC, there is only one team that has consistently taken first place in the single safety property track since they entered the competition in 2008. This year however, they not only won the single safety property track, but also ran away with first place in the liveness track, and the deep bound track. No other team in the competition’s history has ever done that. The team that achieved this is the ABC team from the University of California at Berkeley. Recently, I got a chance to sit down with them to find out their secret to such unprecedented success.
(more…)
Tags: DVCon, EDA, HWMCC, Oski Technology, Oski Verification Challenge, Vigyan Singhal
1 Comment »
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, June 7th, 2017
CDNLive EMEA was held on May 15-17, 2017 at the Infinity Hotel and Conference Centre in Munich, Germany and Oski was there exhibiting as a Cadence partner in the vendor exposition. It was a privilege to attend and to meet many Cadence users from across Germany, plus a wide spectrum of other places including Brazil, the Czech Republic, England, France, Ireland, Italy, Netherlands, Scotland, Serbia and Spain.
It was there that Davide Santo, NXP Semiconductor’s Advanced Driver Assistance Systems (ADAS) visionary, delivered a standing-room-only keynote in which he described the coming revolution in automated and autonomous driving. He predicted massive growth in future computing requirements that will be necessary to achieve full vehicle automation. He explained how a hybrid topology of a central fusion unit and distributed smart sensors will be required to “sense”, “think” and “act” in unison.
(more…)
No Comments »
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 »
Thursday, December 29th, 2016
In this 3-part blog, I’ve been examining the emerging role of the Formal Verification (FV) Program Leader, an individual who plays a critical part in adoption of FV as part of an organization’s verification strategy, and its deployment on real projects. The FV Program Leader’s importance and value stems not from him or her being an expert in FV technology, techniques or tools, nor from being the direct manager of the FV engineers in the organization, although he or she may also be one or both of these things in addition to being the FV Program Leader. Rather, it comes from the FV Program Leader being an advocate, evangelist, facilitator and coordinator for the organization’s efforts to understand, adopt and utilize formal verification.
In part one of this discussion, I listed the six primary aspects of the FV Program Leader’s role: Organization, Training and Upskilling, Test Planning, Progress Metrics, Sign-off Process, and Post Mortem Analysis. In parts one and two, I talked in detail about the first four of these roles. In this, the third and final installment, I’ll discuss the last two: achieving final sign-off via formal verification and learning from the experience via post-mortem analysis.
Sign-off Process: Sign-off flows are, of course, very familiar to design and verification teams, who are accustomed to using them to sign-off various aspects of a design, such as timing via static timing analysis, functionality via simulation, netlists via RTL-to-gate equivalence checking, and final tape-out databases via LVS and DRC checking. Sign-off typically involves a checklist of gating criteria that must be reviewed and approved by a committee of stakeholders in the process. The sign-off process helps to determine when a given stage of the design flow is complete and enforces a minimum standard of quality control.
(more…)
No Comments »
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.
(more…)
Tags: "Decoding Formal" Club, Decoding Formal, formal verification, Oski
No Comments »
|
