A Recap of Formal Verification Use Cases from Verification Day 2020
Like most industry events this year, we shifted our Formal Special Interest Group event to virtual and joined forces with Synopsys’ static and low power teams to host a combined event, Verification Day. For this virtual event we had the advantage of reaching out to customers across geographies and time zones which reflected in the highest attendance ever, attendance increased by 3X compared to the last year.
As part of formal verification track, we had good mix of Synopsys and customer presentations. Sean Safarpour kickstarted the track describing how increasing verification complexity demands formal to be included as part of verification flows. He talked about how customers had been using formal apps to address a variety of verification problems ranging from fastest coverage closure to formal signoff for control intensive and data path blocks.
Lijun Li, a presenter from a semiconductor vendor, talked about how data path verification is a “must have” for his team and how formal has been used for years. Data path verification flow has been put in place to be used by designers and no special skill is required to use this mandated flow. He also shared details on what it takes to formally signoff these math intensive datapath design structures.
Ipshita Tripathi from Qualcomm discussed how her team has been climbing the formal deployment pyramid. She covered a range of uses, from using formal Apps as needed to training team members to make use of as many as Apps as possible including formal signoff. This presentation can be a blueprint for any verification team planning to deploy formal as essential part of the verification flow.
Luv Sampath from Qualcomm presented on how formal can help with the development of the most optimum functional coverage models (using reachability analysis). This is a unique way to show how to approach functional coverage, not only for formal analysis, but also for its usage and closure in simulation environment.
Arun Singh from Samsung had an interesting take on how the combination of sequential equivalence and transactional equivalence can be used to verify the impact of clock gating logic on functionality of the design. Typically, sequential equivalence works very well to address this verification problem, but in some special circumstances transactional equivalence (which is also used for data path verification) can help reduce the users’ effort.
Finally, Iain Singleton and Paul Stravers from Synopsys shared their experiences on how they used formal to find bugs and signoff the block without running a single cycle of simulation at block level. This presentation also had details on how designers find it much more productive to debug in a formal setup where turn around time is much smaller and debug trace is much shorter.
Overall, it was a very productive virtual conference and you can access the recorded proceedings HERE.
Stay safe and stay healthy!
