The use of this site and the content contained therein is governed by the Terms of Use. When you use this site you acknowledge that you have read the Terms of Use and that you accept and will be bound by the terms hereof and such terms as may be modified from time to time.
All text, graphics, audio, design and other works on the site are the copyrighted works of nasscom unless otherwise indicated. All rights reserved.
Content on the site is for personal use only and may be downloaded provided the material is kept intact and there is no violation of the copyrights, trademarks, and other proprietary rights. Any alteration of the material or use of the material contained in the site for any other purpose is a violation of the copyright of nasscom and / or its affiliates or associates or of its third-party information providers. This material cannot be copied, reproduced, republished, uploaded, posted, transmitted or distributed in any way for non-personal use without obtaining the prior permission from nasscom.
The nasscom Members login is for the reference of only registered nasscom Member Companies.
nasscom reserves the right to modify the terms of use of any service without any liability. nasscom reserves the right to take all measures necessary to prevent access to any service or termination of service if the terms of use are not complied with or are contravened or there is any violation of copyright, trademark or other proprietary right.
From time to time nasscom may supplement these terms of use with additional terms pertaining to specific content (additional terms). Such additional terms are hereby incorporated by reference into these Terms of Use.
Disclaimer
The Company information provided on the nasscom web site is as per data collected by companies. nasscom is not liable on the authenticity of such data.
nasscom has exercised due diligence in checking the correctness and authenticity of the information contained in the site, but nasscom or any of its affiliates or associates or employees shall not be in any way responsible for any loss or damage that may arise to any person from any inadvertent error in the information contained in this site. The information from or through this site is provided "as is" and all warranties express or implied of any kind, regarding any matter pertaining to any service or channel, including without limitation the implied warranties of merchantability, fitness for a particular purpose, and non-infringement are disclaimed. nasscom and its affiliates and associates shall not be liable, at any time, for any failure of performance, error, omission, interruption, deletion, defect, delay in operation or transmission, computer virus, communications line failure, theft or destruction or unauthorised access to, alteration of, or use of information contained on the site. No representations, warranties or guarantees whatsoever are made as to the accuracy, adequacy, reliability, completeness, suitability or applicability of the information to a particular situation.
nasscom or its affiliates or associates or its employees do not provide any judgments or warranty in respect of the authenticity or correctness of the content of other services or sites to which links are provided. A link to another service or site is not an endorsement of any products or services on such site or the site.
The content provided is for information purposes alone and does not substitute for specific advice whether investment, legal, taxation or otherwise. nasscom disclaims all liability for damages caused by use of content on the site.
All responsibility and liability for any damages caused by downloading of any data is disclaimed.
nasscom reserves the right to modify, suspend / cancel, or discontinue any or all sections, or service at any time without notice.
For any grievances under the Information Technology Act 2000, please get in touch with Grievance Officer, Mr. Anirban Mandal at data-query@nasscom.in.
As design complexity is increasing, the goal of 100% functional coverage becomes harder to achieve even after using constrained random stimulus and directed scenarios, therefore there is a need to adopt new methods of validation.
The verification engineering team tries to break down the RTL design into pieces and analyse them – independently and then in sync. This takes time! Design verification takes almost 80% of the overall time spent on chip development and verification engineers lose hair, sleep, peace, patience and weekends on tight deadlines to deliver the quality of verification.
Each miss from the verification team can cost a potential revenue loss of millions. The bugs can result in rolling back all the produced silicon from the market. One example was when Samsung rolled back its Galaxy Note 7. Turns out the device was failing due to battery short circuit, which was missed during the verification of the design. RTL designing and verification is a tricky task because we can’t give an update or version upgrade like what happens in the software industry and we can’t translate our design to silicon for each update in design. Hence, we need to verify and thoroughly analyse the design before actually sending the design to foundry. As we can rightly guess, this is a very expensive process both in terms of time and money.
Fig 1
The figure above shows how the delay in the making of a chip affects the cost. This shows that as many bugs as possible needs to be removed in the early stages and new design errors should not be introduced while refining the design.
Introduction to Formal Verification
Formal verification uses mathematical models/methods to prove or disprove the correctness of the system’s design with respect to formal specifications expressed as properties to verify the design thoroughly. It covers all the possible values a design variable can take and hence generating all the possible scenarios and stimulus for the design. We can theoretically achieve 100% coverage, which is a huge boost to the confidence of the design.
Formal verification is a technique used in different stages in ASIC project life cycle like front end verification, Logic Synthesis, Post Routing Checks and also for ECOs. But when we delve deeper, the formal verification used for verifying RTLs is entirely different from others.
Fig 2
Formal Verification Techniques:
The following figure illustrates the various formal verification techniques:
Fig 3
What is Formal Property Verification (FPV)?
What is formal property verification? A natural language such as English allows us to interpret the term formal property verification in two ways, namely:
Verification of formal properties, or
Formal methods for property verification(widely used interpretation by formal engineers)
FPV is the simplest form of formal verification; it is a method to prove the correctness of a design or show root cause of an error by rigorous mathematical procedures. This does not mean that the user must be a mathematician. It does not require test benches or stimuli and turnaround time is very less.
How FPV is Done?
In practice, there are two ways in which property verification is done today. These are static Assertion-based Verification (ABV) and dynamic Assertion-based Verification (ABV). In both forms, formal properties specify the correct requirements of the design, and the goal is to check whether a given implementation satisfies the properties. Static ABV techniques formally verify whether all possible behaviors of the design satisfy the given properties. Dynamic ABV is a simulation-based approach, where the properties are checked over a simulation run – the verification is thereby confined to only those behaviors that are encountered during the simulation.
Property checking can be done by using either using property languages (for example, ITL Interval Language) or Assertion languages (SVA, PSL, etc.). SVA is the assertions subset of the System Verilog language. Assertions or properties are primarily used to validate the behavior of a design and can be checked statically by property checker tool and proves whether or not a design meets its specifications. A holding SVA/ITL/PSL means that the assertion/property has been formally and exhaustively checked and it holds in all possible traces of the design. A failing SVA/ITL/PSL means that a counterexample was found that represents a violation of the intended design behavior.
Fig 4: High level Architecture view for formal property verification
Formal verification tool automatically uses its magic to generate the stimulus and implicitly covers all the cases. The only requirement of Formal tool is to give it the RTL design and a formal description of the specifications in form of PROPERTIES for covering all the input and output combinations exhaustively. Basically Formal Verification works on the principle of “failing to fail” to prove the design’s correctness. It generates all the possible stimulus and tries to fail our check. When it fails to fail – it states our design is correct else it stop immediately once a failure is found.
Let’s understand this through an example: We need to verify a DUT. We have two options:
We can generate possible input and output combinations on our own and write very specific test patterns to validate that the input we provided generates the expected output. This is known as Directed Testing of the design of Directed Verification. We use SV, UVM test-benches to write specific testcases to check the DUT.
The other option is – a tool generates all the possible inputs possible for our design and we only describe the behavior or relationship of input with the output. This description of behavior is done using SVA(system Verilog Assertions).
What type of designs can be easily verified using FPV?
Fig 5
Key Differences between Simulation and Formal:
Fig 6
What are Formal Engines?
Just like the engines of a car or any other vehicle. Formal engine is the actual heart and soul of the Formal Tool. It is the driving force. It determines how exhaustively the tool is verifying. It contains the algorithm which mathematically proves the correctness of our design.
Fig 7: Graphical representation of various engine’s performance
What are the EDA tools and supported apps available?
There are many tools in the industry which uses formal methodology to achieve a particular purpose.
Synopsys: Synopsys provides VC Formal tool which covers a wide range of formal applications such as assertion-based verification, connectivity verification, sequential verification, etc. There is VC LP which is mainly used to verify formally the low poour design intent.
Siemens/Mentor Graphics: Siemens/Mentor Graphics Questa tool also provides formal verification specific applications such as Questa Connectivity check, Questa post silicon debug, Questa property check, Questa Register check, etc.
JasperGold from Cadence: Cadence JasperGold tool supports many ‘Apps’ through which certain formal verification tasks can be performed very easily. Along with that, for standard interfaces, assertions/properties can be generated automatically or readily available as Assertion Based Verification IPs (ABVIP).
Formal Property Verification (FPV)
Unreachability Analysis (UNR)
Pin connectivity verification (CONN)
Configuration register verification (CSR)
AMBA Interface protocol compliance verification using ABVIPs (FPV)
Formal Coverage (COV)
Formal Superlint/ Auto Formal Lint (AFL)
Sequential RTL equivalence (SEC)
Security Path Verification (SPV)
Functional Safety Verification (FSV)
Fig 8: View of Supported JasperGold apps
FPV Flow, Environment and Setup
Formal verification tools try to prove design correctness by analysing the space of possible behaviors of a design with static analysis algorithms, without simulating the design behavior over time. Therefore, formal techniques do not need a traditional testbench with dynamic tests/stimuli. Before starting formal verification, we must specify design intent, usually in the form of properties or assertions. This gives the tool a formal basis to reason about the design, and to identify violations that signify problems or bugs.
Formal tool doesn’t require a big SV/UVM based testbench. The tool creates a mathematical model for both the design and the specified assertions and try to prove one model against the other. In the process, it automatically checks whether the defined assertion is valid for all the legal possible stimuli defined by the set of user constraints.
Formal tool requires the clocks and resets to be specified before the actual formal analysis/verification begins. Formal tool can infer clocks based on how they are used in the design. But specifying clocks explicitly would help the tool analyse the sequential behavior of the design accurately. Also specifying the reset would help the tool apply reset for a few cycles and reset the design to a known state. And the other way of getting to a known state is to load waveforms from the simulation. This would help in reducing the non-deterministic values on non-resettable flops for formal analysis. More the non-deterministic values, the formal analysis would be more pessimistic. It would be good to reduce the state space by initializing the design using waveforms.
Sometimes we may need control over the state space. Legalize our state space by specifying constraints. Constraints direct the formal tool to choose values that follow the constraints. If we don’t specify the constraints, tool tries to mathematically prove the assertion for all the possible stimuli which may not be the desired behavior.
Formal verification tools ensure faster run times for comparatively small designs. However, adding assertions can take some time before doing actual verification. Also, time taken for establishing a given proof (assertions) can increase exponentially with the size of the design under consideration. We can direct the tool on what engine it should use and how much time it needs to spend on proving assertions, etc.
FPV Flow and Setup
Fig 9: High Level Flowchart for formal property verificationFig 10
Sample TCL File
Fig 11
Advantages of FPV over Simulation approach
Verification is mostly fully automatic except for initial set-up, property coding
Verification can be started as soon as RTL is ready. It need not wait for the readiness of complete RTL. It can start the analysis even with basic functionalities:
Reset Analysis
Sanity checks, etc.
As testbench is not required, stimulus generation will be automatically managed by the FA tool with or without constraints around it
The prove will be extremely fast compared to dynamic simulations.
Simulations usually takes more time to detect the corner cases, FSM deadlock conditions. Sometimes it need additional metrics (coverage data) to identify the corners. But FA tool can easily find and reach those cases in quick time (fraction of minutes)
Both black box and white box approach can be used
There is no specific testbench required to drive stimulus to the DUT. Thus, formal can be applied to the designs in very early phases of the project.
Gives a higher level of confidence than simulation alone. Formal should be considered as complementary to simulation rather than replacing simulations entirely.
Can replace millions of simulation cycles.
Allows a more concrete mapping of specifications/design-intent to the actual design.
Limitations of Formal Verification:
Even though formal verification has many advantages it does have certain disadvantages:
As the design size grows, the state-space increases exponentially. So, when compared to a design with 2048 flops, a design with 2049 flops will have an exponential increase in the state space. Hence as the design size increases, quickly we reach an upper limit where the machine cannot handle the size of the design or the time taken to explore the state space starts to reach a point of diminishing returns. This is called the problem of state-space explosion.
FA is not suitable for data paths functions except for simple functions. This is true especially for algorithmic blocks
FA is good for verifying a system but not for validating the system (As Validation usually can be done only dynamically and formal verification is a static process).
FA can only handle RTL logic. Any analog block will get black boxed or can be removed from the DUT during FA
That the contents of third-party articles/blogs published here on the website, and the interpretation of all information in the article/blogs such as data, maps, numbers, opinions etc. displayed in the article/blogs and views or the opinions expressed within the content are solely of the author's; and do not reflect the opinions and beliefs of NASSCOM or its affiliates in any manner. NASSCOM does not take any liability w.r.t. content in any manner and will not be liable in any manner whatsoever for any kind of liability arising out of any act, error or omission. The contents of third-party article/blogs published, are provided solely as convenience; and the presence of these articles/blogs should not, under any circumstances, be considered as an endorsement of the contents by NASSCOM in any manner; and if you chose to access these articles/blogs , you do so at your own risk.
As India embraces the digital age, Insurtech is emerging as the catalyst that transforms the insurance landscape. The government's strategic initiatives, coupled with regulatory foresight, are not just clearing the path for insurtech innovators but…
From the beginning of computing, enterprise workloads found their home on-premises. Servers were racked diligently within secure data centres, processing vital business data. Then, the cloud emerged, painting a captivating picture of scalability and…
In the rapidly growing technology world, enterprises are readily looking to enhance their businesses in innovative ways to deliver seamless Customer Experiences (CX). The advent of cutting-edge technologies such as Generative AI (GenAI) is set to…
Rapid Urbanization, Digitalization, and increasing demand for Smart Cities have transformed Elevators into a platform of many opportunities. Research estimates that the Global Elevators and Escalators Market will grow at a CAGR of 6.3% from 2022 to…
The Mars Climate Orbiter: In 1999, the Mars Climate Orbiter failed to enter its intended orbit around Mars and was destroyed upon entering the Martian atmosphere. The failure was caused by a software error that used the wrong units of…
Integration of AI and Real-World Evidence (RWE): We foresee a significant leap in the integration of AI with Real-World Evidence (RWE) in the pharmaceutical industry. This convergence will enhance clinical trial design, optimize patient recruitment…
