Posts Tagged ‘Oski Technology’
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.
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.
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…)
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…)
Wednesday, December 9th, 2015
“Jingle Bells”, “Silent Night”, “We Wish You a Merry Christmas”… It has been several weeks since my youngest daughter started practicing for her upcoming violin concert. I grew up in China and missed out on the fun of Christmas festivities and holiday music. Now that we live in the United States and have had the full holiday experience, I learned that Santa Claus comes to town – two months early!
With the holiday season upon us and reflecting on the past year, 2015 has been a very busy and rewarding time for Oski. The hard work put in by each of our colleagues is paying off – with the growing adoption of formal technology and formal sign-off methodology at many companies across the globe. Formal Verification is finally coming to town!
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.
Thursday, October 29th, 2015
This year’s Oski Deep Bound Track Hardware Model Checking Competition (HWMCC) was a thrillingly close contest that came down to just one benchmark design of more than 100 benchmarks. The winner was announced at the Hardware Model Checking Competition Report session of the annual Formal Methods in Computer-Aided Design (FMCAD) Conference, held in Austin, Texas, on September 30, 2015. Winner Norbert Manthey of the Institute of Artificial Intelligence and a graduate of TU Dresden, Germany, took the prized first place from runners up Alberto Griggio, and Marco Roveri, researchers at Fondazione Bruno Kessler, and graduates of the University of Trento, Italy.
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.