EDA DesignLine Blog
Tell us What You Think
We want to know what you thought about this Discussion. Let us know by adding a comment.
Oski sponsors hardware model checking award
Brian Bailey
10/30/2012 12:03 PM EDT
A few days ago I received a press release from Oski Technology related to its sponsorship of the annual Hardware Model Checking Competition (HWMCC). After the challenge that they performed at DAC last year, and the lack of funding that happens in the Universities related to verification, I was interested to get more information about their attempts to raise interest levels and challenge the new generation of verification specialists. So, I talked to Vigyan Singhal, Oski Technology’s president and chief executive officer.
The 2012 Oski Deep Bounds Award went to Niklas Sörensson and Koen Claessen of Chalmers University from Gothenburg, Sweden.
Is this first year that this has been done?
Vigyan: Yes, this is the first year the Deep Bounds track has been added to HWMCC, at Oski's initiative. This track measures the effectiveness of Bounded Model Checking, the technology necessary for the most complex end-to-end formal verification problems. The previous tracks did not give any weight to these problems, the hardest, those that could not be completely solved.
Oski Technology wanted to encourage this track so that more complex designs can be solved automatically and directly by formal verification users, instead of using manual abstractions that can sometimes requires deep expertise.
How many entries were there?
Vigyan: A total of 11 model checking engines were submitted by 14 participants from six countries.
How do you judge something like this? What makes one entry better than another?
Vigyan: Participants submitted their engines to the organizing committee, consisting of Armin Biere (organizer of HWMCC 2012 and professor of computer science at Johannes Kepler University in Austria), Keijo Heljanko (professor at Aalto University's School of Science in Finland), Martina Seidl (professor at the Institute for Formal Models and Verification at Johannes Kepler University) and Siert Wieringa (researcher at Aalto University School of Science and Technology). The committee prepared 310 designs for the HWMCC competition. Of these, 85 designs were deemed to be the hardest. The Deep Bounds track was run on these 85 instances. The winner was determined by calculating which engine went the deepest on the hardest designs.
Are they developing tools or using tools?
Vigyan: Contestants are developing model checking proof engines used at the core of model checkers, including commercial formal verification tools. They were not using tools, but developing tools. However, commercial model checkers also need additional technologies, such as GUI, Verilog parser and waveform display technologies.
The press release said: Entrants were invited to solve benchmarks in the AIGER format. What is AIGER?
Vigyan: AIGER is a format used so that engine developers can focus on the core engine technology, and do not have to worry about building Verilog or SystemVerilog parsers. The name AIGER contains as one part the acronym AIG of And-Inverter Graphs (a commonly used data structure in model checking tools). It was first openly discussed at the Alpine Verification Meeting 2006 in Ascona, Switzerland, as a way to provide a simple, compact file format for the first HWMCC in 2007.
Can you tell me more about Niklas Sörensson and Koen Claessen, the winners of the award?
Vigyan: Niklas Sörensson was awarded a Ph.D. from Chalmers University in 2008, and was a post-doctoral researcher at Chalmers University until this year. He recently joined Mentor Graphics. Koen Claessen received a Ph.D. from Chalmers University in 2001, and is a professor at Chalmers University.
Does Chalmers have a formal verification program?
Vigyan: Yes, Chalmers University has a formal verification group, including professors Mary Sheeran and Koen Claessen. Many of its alumni have worked at EDA companies, including Cadence, Jasper, Mentor Graphics, Synopsys.
Thanks Vigyan and thank you for doing your bit to encourage verification in our colleges. I hope someone will do a similar program for other types of verification and to get the next generation of graduates believing that solving problems in verification is as important as doing design.
Related materials
The Oski 72 hour challenge
CEO and Professor Spotlight: Andreas Veneris
Brian Bailey – keeping you covered
If you found this article to be of interest, visit EDA Designline where you will find the latest and greatest design, technology, product, and news articles with regard to all aspects of Electronic Design Automation (EDA).
Also, you can obtain a highlights update delivered directly to your inbox by signing up for the EDA Designline weekly newsletter – just Click Here to request this newsletter using the Manage Newsletters tab (if you aren't already a member you'll be asked to register, but it's free and painless so don't let that stop you).
The 2012 Oski Deep Bounds Award went to Niklas Sörensson and Koen Claessen of Chalmers University from Gothenburg, Sweden.
Is this first year that this has been done?
Vigyan: Yes, this is the first year the Deep Bounds track has been added to HWMCC, at Oski's initiative. This track measures the effectiveness of Bounded Model Checking, the technology necessary for the most complex end-to-end formal verification problems. The previous tracks did not give any weight to these problems, the hardest, those that could not be completely solved.
Oski Technology wanted to encourage this track so that more complex designs can be solved automatically and directly by formal verification users, instead of using manual abstractions that can sometimes requires deep expertise.
How many entries were there?
Vigyan: A total of 11 model checking engines were submitted by 14 participants from six countries.
How do you judge something like this? What makes one entry better than another?
Vigyan: Participants submitted their engines to the organizing committee, consisting of Armin Biere (organizer of HWMCC 2012 and professor of computer science at Johannes Kepler University in Austria), Keijo Heljanko (professor at Aalto University's School of Science in Finland), Martina Seidl (professor at the Institute for Formal Models and Verification at Johannes Kepler University) and Siert Wieringa (researcher at Aalto University School of Science and Technology). The committee prepared 310 designs for the HWMCC competition. Of these, 85 designs were deemed to be the hardest. The Deep Bounds track was run on these 85 instances. The winner was determined by calculating which engine went the deepest on the hardest designs.
Are they developing tools or using tools?
Vigyan: Contestants are developing model checking proof engines used at the core of model checkers, including commercial formal verification tools. They were not using tools, but developing tools. However, commercial model checkers also need additional technologies, such as GUI, Verilog parser and waveform display technologies.
The press release said: Entrants were invited to solve benchmarks in the AIGER format. What is AIGER?
Vigyan: AIGER is a format used so that engine developers can focus on the core engine technology, and do not have to worry about building Verilog or SystemVerilog parsers. The name AIGER contains as one part the acronym AIG of And-Inverter Graphs (a commonly used data structure in model checking tools). It was first openly discussed at the Alpine Verification Meeting 2006 in Ascona, Switzerland, as a way to provide a simple, compact file format for the first HWMCC in 2007.
Can you tell me more about Niklas Sörensson and Koen Claessen, the winners of the award?
Vigyan: Niklas Sörensson was awarded a Ph.D. from Chalmers University in 2008, and was a post-doctoral researcher at Chalmers University until this year. He recently joined Mentor Graphics. Koen Claessen received a Ph.D. from Chalmers University in 2001, and is a professor at Chalmers University.
Does Chalmers have a formal verification program?
Vigyan: Yes, Chalmers University has a formal verification group, including professors Mary Sheeran and Koen Claessen. Many of its alumni have worked at EDA companies, including Cadence, Jasper, Mentor Graphics, Synopsys.
Thanks Vigyan and thank you for doing your bit to encourage verification in our colleges. I hope someone will do a similar program for other types of verification and to get the next generation of graduates believing that solving problems in verification is as important as doing design.
Related materials
The Oski 72 hour challenge
CEO and Professor Spotlight: Andreas Veneris
Brian Bailey – keeping you covered
If you found this article to be of interest, visit EDA Designline where you will find the latest and greatest design, technology, product, and news articles with regard to all aspects of Electronic Design Automation (EDA).
Also, you can obtain a highlights update delivered directly to your inbox by signing up for the EDA Designline weekly newsletter – just Click Here to request this newsletter using the Manage Newsletters tab (if you aren't already a member you'll be asked to register, but it's free and painless so don't let that stop you).
|
|
|
|
|
Navigate to related information