25 - 26 September, 2019

Radisson Blu Bengaluru

Bangalore, India

Event Details

MP Associates, Inc.
THURSDAY September 26, 11:30am - 1:00pm | Robusta
Formal Verification
Girish Marudwar - Synopsys, Inc.
Formal Verification (FV) technology and methodology has come long way and has become main stay along with simulations. With advent of multiple apps, we see many engineering teams have adopted formal verification and achieved shift left in their verification cycles. In pursuit of shifting left further, experts are innovating new ways to apply FV to non-conventional problems. In this first session on Formal Verification these innovations will show you that there is lot of potential in FV technology which is still out there to be unearthed and get benefited

1.1Step-Up Your Register Access Verification
Even small IPs have dozens of control & status registers, many with complex access policies. Additionally, verifying a retention registers’ robustness early-on can save many simulation cycles down-the-road. While simulations leveraging UVM_REG can exercise the primary use cases, numerous corner-cases are left uncovered, creating the risk of show stopper bugs going undetected. In short, a formal-based solution is needed to ensure exhaustive coverage of the state space. Hence, in this paper we will show how we replaced our simulation-based flow with an automated formal-based flow to reduce our setup and run time from weeks down to minutes, simultaneously enjoying exhaustive results.
 Speaker: Nisha Kadhirvelu - Cypress Semiconductor Technology India Pvt Ltd
 Authors: Nisha Kadhirvelu - Cypress Semiconductor Technology India Pvt Ltd
Sundar Krishnakumar - Cypress Semiconductor Technology India Pvt Ltd
Rimpy Chugh - Mentor Graphics (India) Pvt. Ltd.
Wesley Park - Mentor, A Siemens Business
1.2Bringing DataPath Formal to Designers’ Footsteps
Aggressive demands in the Graphics Industry force the need for a shift left approach on all the aspects of design life cycle. This compels the designers to adopt better arithmetic implementations and also optimize the design to gain better power and performance. Such changes often have a short time to market schedule and hence, need to be quickly validated. In Intel Graphics, we have been successful in completely validating complex data path designs by functionally validating the algorithmic specifications (specs) in a high level language (C/C++), also known as System Level Model (SLM) against the RTL implementation in a Formal Verification (FV) tool. We propose extending DataPath FV to include three comparatively low effort and high ROI methodologies: Design Exercise, RTL-RTL and Corroborating C Specification model. We share success stories where these methodologies helped in proliferating FV within Intel Graphics and have helped to quickly validate new feature changes.
 Speaker: Achutha Kiran Kumar V. Madhunapantula - Intel Corp.
 Authors: Achutha Kiran Kumar V. Madhunapantula - Intel Corp.
Disha Puri - Intel Corp.
Shriya Dharade - Intel Corp.
1.3Formal for Adjacencies: Expanding the Scope of Formal Verification
ABSTRACT Introduction Pre-silicon simulation/emulation based dynamic validation (DV) has advanced by leaps and bounds to verify the latest complex hardware designs with decent confidence. However, the union of all these technologies would still leave some holes that get exposed as bugs on the silicon that motivates the designers to explore alternate methodologies to gain higher confidence. Formal Verification (FV) is one powerful validation technique that mathematically proves design correctness, rather than simulating specific test cases, and has been growing in popularity across the industry. Traditionally, FV has been found useful applications in the areas such as algorithmic circuit verification, complex control path verification, connectivity checks etc. There are many other areas where application of FV has been limited or completely non-existent since these are considered not suited for FV. In our paper, we present our experience in application of FV in some of these non-traditional areas. Post-Silicon FV In the current design environment, even after running many cycles of verification both at simulation and emulation, there are critical bug escapes which are found post-silicon. These bugs are often hard to root-cause at the chip level since not all RTL signals are available for debug. A RTL bug which is found post-silicon is required to be root caused and fixed correctly at the RTL level. The current techniques which are being used, although help in localizing a problem, takes time to arrive at the root cause to a particular unit or a functional block (FUB). Some of the critical bugs could delay the PRQ of the product and hence causing a huge financial loss to the company. The key requirement for curtailing the compute resources would be exhaustive verification methods and expeditious debug time. Formal property Verification (FPV) exhaustively verifies a given design against a specification coded as properties. The FPV environment uses mathematical techniques to verify the assertions, given a set of constraints (assumptions). A passing proof indicates that all possible behaviors were exhaustively verified and the design adheres to the given specifications. Here, we describe the FPV methodology which was incorporated to resolve the post-silicon bugs on multiple units therewith not only reducing the time for debug but also proving that the RTL fix provided was correct. Although application of FV in post-silicon debugs is nothing new [6], we are presenting an optimised methodology which would help in catching bugs faster. Non-Conventional Applications using Formal: The basic theory behind the RTL-RTL is that when we inject two functionally equivalent RTL models with same inputs, we expect the outputs to remain the same. The tool requires us to give two RTL models. If the input names are same, then it drives the same values on both the models and an assertion is added at the output to check for equivalence. This methodology has found widespread applications in areas such as clock gating verification, timing fixes [5] etc. We employed this methodology to attune to our validation environment which lead us to the application of sequential equivalence checking in new areas. • Hierarchical RTL-RTL for SoC designs and derivative products: When there are multiple derivative projects forked off from a parent project, there is a need to validate if the feature has unintended changes in the forked off projects. To ensure the correctness of the change, many tests are run which has an added impact on the compute cost on each test. This effort could be greatly reduced if we have equivalence checked from the top level to the design till the leaf level of two projects. Conventional RTL –RTL would hit convergence issues if the design size is more than 5 million. We worked with vendor to enhance the equivalence check capabilities at chip level to automatically partition the design depending on the hierarchy defined at the chip level till the leaf level units. This compares the two designs till the leaf level and equivalence is proven. We have enhanced further to compare the partition if there is a change in the name of the partition with the lower level units being the same. This has helped us to achieve the results nearly 50X faster to current validation environment. •SCHMOO RTL-RTL: Intel GPU (GT) has media capabilities which handle video encoding, decoding and transcoding process. The traditional way of validating media hardware algorithms is using a golden C model as reference and control logic in these blocks is validated using testbench techniques to create different timing scenarios. In any VLSI design it is hard to expose some of the control logic bugs using traditional techniques as we are limited by either test content, testbench infrastructure or coverage and these bugs end up showing in silicon, which is very expensive. We use the terminology schmoo to refer to different interface delays and backpressures created in testbench to the DUT. The problem with the existing methodology is due to the vast amount of variable delays that can happen and that cannot be generated and tested in the lifetime of a product. This leads to a lot of silicon escapes which leads to a higher TTM. So, we explored an already established RTL-RTL methodology and adapted it to suit the validation requirements. In order to enable the requirement for control logic verification, we used FIFO’s at the input and output to enable the variable latency RTL-RTL. •Connectivity Verification Formal Connectivity verifies RTL connections at the block, unit, and chip level for IP integration. It takes connectivity specification as input, automatically generate properties for each connection specified in the specification and exhaustively verifies connectivity. Here, we discuss the innovative application of connectivity verification which is beyond the normal SOC connectivity verification. Using normal SoC connectivity verification flow at top level, a lot of the debug time is wasted in debugging the failures related to errors in connection misses. We extracted the reverse connectivity from monitors connected at leaf levels and translated these connections to top level and verified thereby reducing down the connectivity debug time to less than 1% of debug time. Thus proving to be a typical example of shift left in validation cycle. By using this application, we have found very critical bugs in the connectivity which were difficult to be found in traditional connectivity check methods. RESULTS: With the application of the methodologies explained above , we have achieved encouraging results in the reduction of verification time in each application. Post Silicon FV : We found that time taken to debug post silicon issues using traditional methodology and the verify the fixes has reduced from 80% to 20% with FV methodology. Hierarchical RTL –RTL : With the FV methodology the reduction in time taken to expose the failures for the whole design is reduced from 94% to 6% . Schmoo RTL –RTL : We noted a reduction of time taken to expose ~95% of the control bugs using the FV methodology is from 84% to 14%. Connectivity Verification : Using conventional method of connectivity verification most of the debug time was spent in verifying the connectivity misses. With the FV methodology, we could achieve a reduction in the time taken to expose and debug the failures from 75% to 25% . References: [1] C. Pixley, "A theory and implementation of sequential hardware equivalence", IEEE Transactions on Computer-Aided Design, Dec. 1992, pp. 1469-1478. [2] Z. Khasidashvili, M. Skaba, D. Kaiss and Z. Hanna, "Theoretical Framework for Compositional Sequential Hardware Equivalence in Presence of Design Constraints", ICCAD 2004, pp. 58-65. [3] “Formal Verification: An Essential Toolkit for Modern VLSI Design” by Erik Seligman, Tom Schubert, M V Achutha Kiran Kumar, Elsevier Publications, 2016. [5] M AchuthaKiranKumar V, Aarti Gupta, Bindumadhava S S, "RTL2RTL Formal Equivalence: Boosting the Design Confidence" DVCon 2014. [6] Aditi, Laurent et al., In case of emergency, call 1-800-FORMAL, JUG 2018
 Speaker: Achutha Kiran Kumar V. Madhunapantula - Intel Corp.
 Authors: Achutha Kiran Kumar V. Madhunapantula - Intel Corp.
Bindumadhava S. Singanamalli - Intel Corp.
Vichal Verma - Intel Technology India Pvt. Ltd
Savitha Manojna - Intel Technology India Pvt. Ltd