by Jin Zhang, Senior Director of Marketing & GM Asia Pacific, and Vigyan Singhal, President & CEO, OSKI Technology
“By failing to prepare, you are preparing to fail”
“Productivity is never an accident. It is always the result of a commitment to excellence, intelligent planning, and focused effort”
Planning is key to success in any major endeavor, and the same is true for meaningful formal applications. End-to- End formal, with the goal of achieving formal sign-off, is a task that usually takes weeks if not months to complete, depending on the size and complexity of the design under test (DUT). Dedicating time and effort to planning is of utmost importance. While most formal engineers and their managers understand the need for formal planning, they do not know how to conduct thorough planning to arrive at a solid formal test plan for execution.
As the first step of any formal sign-off project that Oski performs for our customers, we routinely dedicate 2 weeks to craft the formal test plan, which includes the following key components:
- How to conduct formal verification on the design, how many formal testbenches we need to build to verify the whole DUT, or which areas of the design are not a good fit for formal
- What End-to-End checkers and corresponding constraints will be implemented
- How many cycles we need to target for the Required Proof Depth
- Where to use complexity solving techniques to overcome inherent design complexity
- How to measure formal progress to achieve sign-off
- How much time it will take to completely verify the design
The goals for creating the formal test plan are not only in creating a blueprint for execution, but also in aligning all the stakeholders on the achievable formal goals for the project. Sometimes a trade-off in scope, schedule and resources has to be made to fit in the realistic limitations. This is a decision that should be made upfront to avoid surprises down the road.
At Oski, we follow a systematic 3-stage approach. The IDENTIFY and EVALUATE stages aim at obtaining a deep understanding of the DUT. The PLAN stage combines both formal and design knowledge to create the final test plan.
This article aims to help formal engineers learn how to do proper formal test planning. Good formal test planning requires lots of formal verification experience, at Oski, a task conducted only by our project leads. However, we believe that by knowing what to do during formal planning, and practicing through real formal verification projects, one can acquire such skills.
FORMAL TEST PLANNING STAGE 1 – IDENTIFY
The goal of the IDENTIFY stage is to identify what design block(s) to verify using formal. This decision is based on several factors:
- What are the verification goals and areas of concern?
- What blocks are suitable for formal?
- How many formal engineers are available and what is their level of formal expertise?
The answers to these questions combined determine on which design blocks to apply formal in order to achieve the best return-on-investment (ROI). The process to arrive at these answers often requires discussion with design/ verification managers and project team leaders. Over the years we have heard many different goals shared by companies wanting to adopt formal:
- More and more, project teams want to shorten the project schedule by reducing their reliance on simulation. They understand applying formal early during RTL development can harden RTL sooner, save verification time at the sub-system or system level using simulation or emulation. Their goal is achieving formal sign-off on suitable blocks. This is the best adoption case because applying formal early results in the best verification ROI.
- In many instances, because bugs continue to be found close to or even after tapeout, formal is used to find missed corner case bugs, hence the formal goal is bug hunting.
- Sometimes, project teams have trouble reaching simulation coverage goals. Formal can discover unreachable targets, or generate input vectors to reach simulation cover points, and therefore the formal goal is coverage closure.
- There are also cases where project teams have specific needs in mind, such as verifying pre- and post- clock gating designs. In this case, some commercial formal apps will be useful.
Different verification goals translate to different strategy and require different levels of planning. For bug hunting, one only needs to focus on blocks or functionalities with the most issues, without having to worry about completely verifying the whole design using formal. On the other hand, achieving formal sign-off requires the most thorough planning. Spending insufficient time on planning may result in the ultimate goals not being reached.
Once the verification goals are aligned, we need to identify blocks suitable for formal. Contrary to common belief that only control types of blocks are good for formal, in reality data-transport blocks, where data is transported from inputs to outputs with simple or no modifications, are also good candidates. For example, some typical control and data-transport blocks could be arbiters of all kinds, interrupt controllers, power management units, tag generators, schedulers, bus bridges, memory controllers, DMA controllers and standard interfaces such as PCI Express, and USB. On the other hand, data-transform designs, where algorithmic options are often performed, are not good for formal property verification (also called model checking). Instead these should be verified using other techniques such as Sequential Equivalence Checking. To understand the functionality of different design blocks, block diagrams and design specs will be useful. Conversation with designers can also help get the high-level functionality of different design blocks for this assessment.
Not all blocks that are suitable for formal should be verified by formal. Again one needs to consider the ROI. If a block is a legacy design with minor changes and has gone through lots of verification, or if it is not a difficult design to verify with simulation (few corner cases and not many concurrent operations), it is obviously not the best use of formal resources. On the other hand, if the block is brand new, or is being developed as an IP to be used internally or externally with lots of parameters, then formal will bring better ROI.
Last, formal resources and expertise constraints limit what types of formal and how much can be done. End- to-End Formal requires a lot of formal expertise and can only be attempted by our engineers after going through several projects with mentors (usually takes about 2 years of full-time formal usage). On the other hand, writing local assertions to do bug hunting can be carried out by engineers with much less formal experience.
The output of the IDENTIFY stage is a list of good design blocks to apply formal verification on and the corresponding goals.
FORMAL TEST PLANNING STAGE 2 – EVALUATE
The goal of the EVALUATE stage is to finalize the list of formal testbenches for different design blocks, along with understanding of the possible formal verification challenges to overcome.
To achieve this goal, we need to carefully consider many factors, such as design interfaces, register transfer level (RTL) metrics and critical design functionalities. Knowledge of design interfaces is important to decide the best places to partition the formal testbenches. One consideration is whether the block interface is standard and well documented. Designers are usually very busy and are less willing to answer lots of questions about interface behaviors. So it is best to partition at the level where design interfaces are standard, or easy to follow. An ideal situation is when formal verification starts in parallel to RTL development so designers have the freedom of moving logic from one block to another to simplify the interfaces.
Next, we use formal tools to report the following RTL metrics: register counts, RTL lines of code (LOC), the number of inputs and outputs, and parameter variations.
These numbers further assist in deciding formal testbench boundaries and estimate the amount of effort it will take to formally verify each chosen block:
- A block with lots of inputs and outputs means more effort in modeling constraints. On the other hand, a block with large RTL LOC or register counts means more effort in modeling checkers and managing complexity. A balance needs to be made between simple interfaces vs. manageable block sizes for formal.
- People often ask what a good design size for formal is. While RTL LOC and register counts help guide the decision on formal testbench boundaries, there are no precise rules to say what the right size of block for formal is, as a small RTL block could be very complex.
A rule of thumb for formally manageable block is a block that can be designed by a single designer. Anything smaller will not bring the best ROI, and anything bigger will pose a challenge for formal tools.
- Understanding the impact of parameters may help reducing formal complexity. If design parameters can be reduced without reducing corner case coverage, formal testbench should use smaller parameters for better performance.
During the process of working with RTL, one also gains an understanding of the micro architecture characteristics of the design block to anticipate the kind of formal complexity and complexity resolution techniques one might use. This process also helps decide the Required Proof Depth.
At the end of this stage, there should be a mapping between each candidate design and one or more formal testbenches, along with a determination of who is responsible for developing which testbench. It is common that only a subset of the target blocks is chosen at the end of this process.
FORMAL TEST PLANNING STAGE 3 – PLAN
The goal of the PLAN stage is to put everything together and create the actual implementation plan for execution, as well as the estimated time for the formal project. With the understanding of design functionality, an English list of End-to-End and interface checkers and the corresponding constraints will be captured in the formal test plan, often in a word document.
It is worth noting that implementing formal End-to-End checkers often requires building reference models. As a matter of fact, 95% of the effort may be in writing the reference models in Verilog or SystemVerilog, with only 5% of the effort in writing the SystemVerilog Assertions. So one needs to factor the time it takes to write reference models when estimating the overall effort level. Also, internal assertions might be used during the project, but only when needed for debugging or helping End-to-End checkers reach closure. Therefore internal assertions are not included in the formal test plan.
Formal complexity discussion and resolution should be included in the formal test plan. Because each design is unique, often there is no existing solution to use. We need to estimate the effort in coming up with a solution as well as writing, verifying and using the solution. This is the most unpredictable part of the process. Often when we underestimated the effort level in our projects, it is when we didn’t fully comprehend the challenge involved in solving complexity. Careful consideration here will save surprises later.
Exact metrics to measure success need to be established. Once there is a total number of checkers and constraints to implement, a weekly tracking spreadsheet can be used to track the numbers of checkers and constraints written each week, their verification statuses, bugs found, and percentage towards completion. In recent years, formal tools have added formal coverage features, which can effectively measure how much the formal testbench is covering the DUT. This will be another useful metric to use to decide when a formal testbench is complete and formal sign-off has been reached.
The following list includes typical chapters in our formal test plan:
- Design overview
- Formal testbench overview
- End-to-End Checkers
- Interface checkers
- Required Proof Depth analysis
- Complexity analysis
- Metrics to measure formal sign-off
- Schedule estimation
The formal test plan is created for each block designated to have a separate formal testbench. This is a living document and may be updated during the verification process. For example, an End-to-End checker may be too complex, so needs to be split into two or more checkers, thus affecting the list in the document. At the end of the project, the actual formal testbench implementation should be consistent with the formal test plan. The formal test plan may serve as a user guide for future projects when the formal testbench is reused.
A REAL CASE STUDY
Often people underestimate the amount of time it takes to do formal sign-off projects. At DAC2014, we conducted a guessing game by proving the following information of a design that we verified before.
Reorders IP packets that can arrive out of order and dequeue them in order. When an exception occurs, the design flushes the IP packets for which exceptions has occurred. Design supports 36 different inputs that can send the data for one or more ports. Another interface provides dequeue requests for different ports. Design supports 48 different ports.
Design Interface Standard:
Packets arrive with valid signal. A request/grant mechanism for handling requests from 36 different sources; All 36 inputs are independent and can arrive concurrently. All 48 ports can be dequeued in parallel again using another request/grant mechanism. Micro Architecture Details:
Supports enqueue and dequeue for IP packets for 32 different input and 48 different ports respectively. 48 different queues used to store IP packets for different ports. A round robin arbiter resolves contention between enqueue requests from different source for the same port at the same cycle. RTL Stats:
RTL Line of code: 10830
Register count: 84,027
Inputs: 3,404 bits
Outputs: 9,137 bits
Clock domain: 1
Data latency: 6
Required Proof Depth: 28 cycles
When asked “How Long It Takes to Formally Verify This Design”, over 70% of respondents guessed in the 2-4 month range. In reality, we spent 5 months on the project with the following breakdown:
- Formal test planning: 0.5 months
- End-to-End Checker (including reference models): 1.5 months
- Constraints: 1 month
- Interface checkers and internal assertions: 1 month
- Abstraction Model: 0.5 months
- Iteration with designs on bug fixes: 0.5 months
As the breakdown shows, significant time is spent in formal testbench development. However once the block is completed verified with formal and achieved sign-off, the chance of missing a bug is very low. This level of confidence cannot be provided by simulation. If this design will be used by several projects, then the formal investment is well worth the effort.
Due to the complexity of formal sign-off projects, it is important to do thorough planning at the beginning so the formal testbench implementation can be done efficiently. This article provided an overview of the stages involved in formal test planning. Since this is a very important step, and one often ignored by project teams, we can’t emphasize enough the value of dedicating time to do formal test planning. Oski CEO, Vigyan Singhal will give a talk on this subject at Mentor Verification Academy on Wednesday June 10th, at 11am. It will be a good opportunity to learn more about the process and ask questions.
Back to Top