Decoding Formal 
Rob van Blommestein
Rob van Blommestein is the Vice President of Marketing at Oski Technology. He has over 20 years of experience in the semiconductor and EDA industries. Rob was most recently the Vice President of Marketing for S2C where he lead the way for their FPGA prototyping and FPGA accelerator technology … More » The ABCs of Winning at the 2017 Hardware Model Checking CompetitionMarch 7th, 2018 by Rob van Blommestein
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.
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. Read the rest of The ABCs of Winning at the 2017 Hardware Model Checking Competition Implementation of an Architectural Formal Verification Methodology by ArterisIPDecember 19th, 2017 by Rob van Blommestein
Chances are you’re probably reading this blog post on a mobile device with the utmost confidence that it is doing what you intend it to do. As consumers, we place a lot of demands on not only our mobile gadgets but also the rest of our personal electronics. We want them to perform all sorts of tasks efficiently, accurately, and with minimal power consumption. All this is, of course, important. But if you look beyond your own microcosm, you will soon realize that everything electronic these days must meet the same if not much more stringent operational standards. Today’s electronic systems are embedded in every aspect of our lives from energy consumption to manufacturing to finance to travel and beyond. Undetected bugs may simply be seen as an annoyance when we experience them in our personal devices, but they can have very profound disastrous effects when we look at the larger electronic ecosystem. Today’s embedded SoCs that drive the world’s electronic ecosystem are high performance, heterogeneous, and multi-processing systems. Most of these embedded SoCs are likely to contain multiple caches that share a single memory resource. At a high level, cache coherency means that two caches cannot have the same cache line in a dirty state and that if a cache contains a cache line in a unique state, that line must not be in another cache. In addition, at least one transaction must always be able make forward progress (no deadlock). Read the rest of Implementation of an Architectural Formal Verification Methodology by ArterisIP What Arm Achieved by Graduating to a Formal Sign-Off MethodologyNovember 6th, 2017 by Rob van Blommestein
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. Use Formal Like Your Life Depended On ItJune 7th, 2017 by Roger Sabbagh - VP of Applications Engineering at Oski
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. Recap: Decoding Formal Club, Spring 2017March 29th, 2017 by Roger Sabbagh - VP of Applications Engineering at Oski
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.
Seven Ways That Formal Verification is Like a Team SportFebruary 15th, 2017 by Roger Sabbagh - VP of Applications Engineering at Oski
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
“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. Part 3: Formal Verification Program Leader: Finishing Well and Learning from the ExperienceDecember 29th, 2016 by Vigyan Singhal
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. Oski Decoding Formal Club – A First-Timer’s PerspectiveDecember 12th, 2016 by Claire Kimple, Marketing Manager at Oski Technology
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. Read the rest of Oski Decoding Formal Club – A First-Timer’s Perspective Another Reason to Stay an Extra Day in AustinJune 3rd, 2016 by Pippa Slayton
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. Part 2: Formal Verification Program Leader: The Critical Role of Planning and MeasurementMay 17th, 2016 by Vigyan Singhal
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. |
|
|
|||||
|
|
|||||
|
|||||
