Posts Tagged ‘Vigyan Singhal’
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.
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…)
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.
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.
Saturday, June 6th, 2015
Oski Decoding Formal Events are usually hosted at the Computer History Museum in Mountain View and have attracted lots of formal enthusiasts in the bay area. Deep formal talks from Oski, lectures given by formal experts from different companies, good networking, cool gifts and museum tours have become the signature of these events that formal engineers look forward to, every quarter.
To reach out to formal enthusiasts around the world and create a bigger event than usual, the 2015 Q2 Decoding Formal event will be hosted at DAC. Our theme is proving completeness of End-to-End Formal for Sign-off.
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.