INTRODUCTION
Since the advent of formal techniques, the application of formal analysis has helped designers achieve more in-depth analysis and coverage of functional verification activities in general. However what has spurred the growth and popularity of such techniques has been specific and targeted applications of formal analysis.
Functional verification is often focused on verification of the logical functions of the design. An overlooked area closely related to functional verification is proper implementation of the logic. In recent years, requirements for better power performance has brought the power implementation aspect of design more and more into the functional verification side, as design functionality became more dependent on new structures designed for power savings.
Similarly, on the timing side the increased complexity of implementation, number of clocks, and clock complexity, as well as greater challenges for closing timing requires a closer look at the verification of the functional aspects of the design early on. The relationship between the functional and timing side of equations in clock-domain crossing verification requires a close analysis of timing in order to gain accuracy and efficiency on the functional side.
Much of the timing information in the front-end design stage is not generally used during functional verification. This information, however, can provide a great deal of guidance and initial seeds for many downstream steps in the chip design process, including activities related to functional verification.
 |
Figure 1:
In this article we will examine several examples where the functional verification tasks can benefit from timing information often readily available in the design.
CLOCK-DOMAIN CROSSING ANALYSIS MADE EASY
Clock-domain crossing verification requires a great deal of knowledge about the clocks and resets, including clock relations and modes. Incomplete or incorrect information used at set up will lead to a great deal of wasted time and very poor results when performing CDC analysis. Generally, most of the time involved in CDC analysis is spent on understanding and analyzing the proper clocking and clock relations and how one can identify the design operation in a specific design mode. As much as 80% of the CDC effort is in set up in order to get good results.
Excellicon tools properly extract timing constraints from the HDL itself. This not only provides a true and accurate representation of the circuit description of the HDL but also provides information which is often hard to deduce based solely on design knowledge; such as clock relations or how to put the design in a certain mode of operation.
In order to extract the right information the design needs to be formally traversed backward in order to extract clocks, clock relations, and mode information from the design.
 |
Figure 2:
By traversing the design backward through the clock paths combined with proper formal analysis, all clock information — including clock relations — are derived from the HDL. The formal analysis is necessary to resolve the paths, and it helps in analyzing the design so that proper clock and control signals are identified. Typically this is a monumental task to perform manually, or even through tracing clocks via traditional tools, but thanks to automation and selection of various detection algorithms using targeted formal analysis techniques, proper signals can be identified and clocks and control signals can be categorized separately so that a designer can analyze and assign proper attributes to them.
 |
Figure 3:
Excellicon's Constraints Manager requires only HDL files as input. The tool then extracts the correct clock and clock information right from the design itself. This not only reduces the work required to analyze and extract the necessary information, but also saves a great deal of time. What may take a week or more of designer time to understand and extract manually is done in minutes by Constraints Manager.
However, the clocking information isolated to a single layer of hierarchy has limited use and is usually missing a great deal of information about the clock scheme of the design because clocks often converge at various hierarchy layers. In order to completely understand what is going on, all controls, clocks, and clock relations need to be analyzed in the context of the hierarchical design. The clocks have to be formally traversed up and down through all layers of the hierarchy, so the proper understanding of the connectivity and functionality of the clocks are quantitatively derived from the design.
 |
Figure 4:
Once Constraints Manager extracts this information, the user has a great deal of information needed for analyzing the clock-domain crossings using Questa®. Automating the initial set up process will only enhance the accuracy and speed of analysis.
Functional verification of CDC is often incomplete because of challenges with set up and the time it takes to perform such analysis. Often a designer validates the CDC cases for only the functional mode of the design, sacrificing other modes due to design schedule constraints. Combining the extraction power of Excellicon with in-depth analysis capability of Questa® CDC enables the designer to perform even more in-depth analysis of CDC. Even a multi-mode CDC analysis, which has been considered very expensive in terms of set up and analysis, can be achieved with the auto-extraction of modes for the entire design through every layer of hierarchy. The ability to extract such information allows CDC analysis for any mode and at any level of hierarchy with very little effort since the most expensive part of the CDC analysis — the set up — is now reduced to minutes.
VERIFYING TIMING EXCEPTIONS FORMALLY AND FUNCTIONALLY
Timing exceptions are often necessary to clarify the design behavior when performing timing closure during the implementation of the design. The back-end designers are often challenged to identify the proper design function in order to correctly access the circuit behavior. The issues are often resolved through back and forth discussion with logic designers who are knowledgeable about the design requirements and their intent when designing the circuit. Use of exceptions is a method to clarify the designer intent and/or prevent the timing tools from analyzing unnecessary paths in order to meet design timing.
This is another example where the timing information (timing constraints) can help to improve the functional quality of the design and reduce design uncertainty through identification of areas prone to timing violations, or identification of design structures either where greater clarity is necessary to describe the behavior of the design or where redesign is needed to define the same functionality. Designs analyzed for proper functionality with respect to timing will be implemented much faster and reduce iteration between the front and back end.
If at all possible the best design practice is to minimize (or avoid) definition of timing exceptions all together, which often provide a great deal of headache and complexity for back-end design teams. Once the design is analyzed for identification of timing exceptions, the functional verification team can determine the implementation complexity with the respective teams and together plan to alleviate such complexities. So if it is possible to design without timing exceptions, or at least reduce them to the absolute necessity, the implementation team will be able to close timing much more efficiently.
Verification of exceptions is not always possible through formal means. In order to fully understand and analyze timing exceptions and their impact on design metrics, such as area and power, a combination of tools such as Excellicon formal engines along with the Questa series of tools must be used to achieve full validation of exceptions, design intent, or structural exceptions.
Lets understand what the functional analysis of timing exceptions can buy during the verification stage of the design. There are two types of exceptions:
- Data Exceptions
- Clock to Clock Exceptions (often performed as part of CDC analysis)
Let's first go through various types of these exceptions, which are essential to correct operation of the circuit, pictured in Figure 5.
 |
Figure 5:
Generally formal analysis is used to verify the structural type of exceptions. However it is important for any tool to be able to bound the formal analysis extent as the cone of logic being analyzed can quickly grow beyond the capacity of the tools.
In the first example, below in Figure 6, there is no possibility for the indicated path to be active, hence the path is said to be False. On the right, the FSM determines the number of cycles necessary for data to be marked valid once launched from the starting point and captured at the end point. Formal analysis is necessary in order to determine the proper functionality of the FSM.
 |
Figure 6:
In analyzing FSM, care must be taken as to what is being analyzed and what information must be provided to formal solvers so that the correct design functionality is analyzed. For example, a formal proof defined as equations after formal analysis of the FSM only validates the FSM functionality as the formal engines operate on the FSM and fails to properly determine the functional operation of the data portion of the design, as shown in Figure 7 below. In order to perform proper functional analysis, the SVA must be completely independent of the FSM and generated as stimuli; otherwise the formal analysis and any associated SVAs represent only validation of FSM functionality, not the proper functionality of the data path.
 |
Figure 7:
By contrast, timing intent exceptions need to be properly defined to describe what the designer intends for circuit operation. In the very simple example below, formal analysis will not provide any useful information other than what is already available to the designer. However, a proper SVA generation along with simulation of such SVA will allow for complete behavior analysis of the circuit and proper definition of exceptions. In this very simple example, false or multi-cycle paths can be applied depending on the designer intent between clk_a and clk_b
 |
Figure 8:
The Excellicon ConCert product is capable of recognizing and extracting various cases of design-intent. Excellicon is capable of recognizing and validating the exceptions; however the designer may need to see the impact of such exceptions in the context of the design. Generation of SVA simplifies the verification and validity of such exceptions. The connection to Questa is made available through generation of SVAs. Such SVAs are made available to Questa for simulation in the context of the surrounding circuitry.
 |
Figure 9:
PROMOTION AND DEMOTION OF TIMING INFORMATION FOR DEEPRE FUNCTIONAL VALIDATION
The clock and mode formal extraction capability of Constraints Manager was briefly outlined in the first section of this article. It was also mentioned that the clock extraction must be performed in the context of the design hierarchy.
The promotion and demotion of timing information is essential to the full understanding of clocks, which are essential to full and complete functional analysis of the design. Depending on design methodology and design team approach, the timing information is either defined (or available) at the top or bottom layers of hierarchy. Whether the design approach is top down or bottom up, much of the timing, control, and clocking information needs to be properly propagated in order to gain full understanding of the control and clocking of the design.
Once this information is correctly extracted and made available for each layer of hierarchy such information can be used for functional and full verification of the appropriate layer of hierarchy. The possibility of leveraging timing information to aide and guide the functional verification necessitates correct and accurate promotion and demotion of timing information from various layers of hierarchy up or down the hierarchy. In order to identify and deduce correct behavior of all clock relations, Constraints Manager and Constraints Certifier tools perform promotion and demotion of constraints respectively.
As shown in Figure 10 below, Constraints Manager is capable of promotion and demotion of timing information via one of three techniques.
 |
Figure 10:
In each scenario, proper techniques are used to promote all timing and control information to the next layers of hierarchy. The details of each technique are available from Excellicon.
Demotion performed by Constraints Certifier preserves the original constraints files while ensuring continuity of the clocking and control structures for analysis at any layer of hierarchy. Unlike traditional demotion of timing information, which is achieved through manipulation of hierarchy delimiters, Excellicon achieves demotion partially through formal means to ensure complete and validated representation of the timing information for each layer of hierarchy. The clock demotion is responsible for demotion of all timing information to lower layers of hierarchy. All clocks, clock groups, exceptions, control and case analysis information, I/O delays, and DRCs are demoted automatically.
CONCLUSION
Timing information traditionally is attributed to the implementation side of the design process. However the need for more communication throughout the design flow and tackling the complexity of verification tasks can greatly benefit from information being readily available from the timing side of the equation.
The timing information derived from the design not only ensures that the timing information used for implementation is in lock step with the design but also helps the verification effort tremendously by providing the necessary information to set up the verification tools properly. Additionally, the added automation will help to reduce the amount of manual work performed by designers, which has to be done in order to gather and feed initial information to the tools used during functional verification.
In a typical design flow, the timing information is not complete and does not contain the necessary information for designers to use during functional verification. However Excellicon enables such a possibility through extraction of relevant information and by validating them formally or through the Questa tool set before they are made available for use in verification and downstream design tools.
Excellicon provides the seed input and much needed information to perform more in-depth analysis of design functionality and quality of results. By extracting control and clocking information from the actual HDL code, verification engineers can ensure proper representation of the timing information for each layer of hierarchy.
Back to Top
