Decoding Formal 
Dr. Jin Zhang
Jin Zhang has over 15 years of experience working in EDA, driving the effort of bringing new products and services to market. At Oski Technology, she is responsible for Oski’s overall marketing strategy as well as business development in Asia Pacific. Prior to that, she was the General Manager at … More » Sponsoring Technical Advancement in Formal VerificationAugust 13th, 2014 by Dr. Jin Zhang
The Hardware Model Checking Competition (HWMCC) was conceived at CAV (Computer-Aided Verification) 2006 and first launched at CAV 2007. The goals were to encourage technical advancement of model checking algorithms and thereby their deployment in the industry to promote formal adoption for hardware design verification. Throughout the years, several competition tracks have been added – Single Safety Property Track, Multiple Safety Property Track, Liveness Track, and Deep Bound Track. The competition has been co-hosted at CAV and FMCAD (Formal Methods in Computer–Aided Design) at various international locations such as Berlin Germany, Princeton NJ, Portland OR, Edinburgh UK, Austin TX, and Cambridge UK. This year, HWMCC 2014 CAV Edition was co-hosted at FLoC Olympic Games 2014 in Vienna, Austria. The event was organized by Armin Biere from Johannes Kepler University, Austria and Keijo Heljanko from Aalto University, Finland. The pictures below show the first-prize winners of each track.
Oski Technology has been a key sponsor for these events over the years. Oski proposed the addition of Deep Bound Track in 2011 to sponsor research in formal verification in order to reach deeper proof bound. As a formal verification service provider, Oski depends on the underlying formal tools (commercial tools from all major vendors) to complete formal verification and sign-off of key design blocks. In order to achieve formal sign-off, end-to-end checkers have to be verified to ensure complete functional coverage on DUT (Design Under Test). However, formal tools often return with bounded proof status due to the complexity of formal and DUT. In all of our projects, we need to qualify the bounded results to make sure sufficient proof depth is achieved using various techniques such as abstraction models. As a result, if a formal tool can reach deeper into the search space, it can speed up verification and achieve formal closure much quicker and easier. Our sponsorship of the Deep Bound Track has resulted in the advancement of the state-of-art in model checking algorithms and its subsequent adoption by commercial formal tools to improve tool performance and capacity. Congratulations to all the winners of all the tracks! We are proud of the work conducted in academia and industry to continue advancing formal verification technology to benefit the semiconductor community.
The Award MedalTags: Aalto University, CAV, Deep Bound Track, FLoC Olympic Games, HWMCC, Johannes Kepler University Category: Blog |
|
|
|||||
|
|
|||||
|
|||||
