Frequently Asked Questions
Have questions about Oski’s Formal Verification Methodology, the difference between Model Checking (MC) and Sequential Equivalence Checking (SEC), or when to use formal? Check out the new Oski Frequently Asked Questions (FAQ) page, below.
Table of Contents
General
- What is Oski Technology?
- What is formal verification?
- What are different kinds of formal verification?
- What formal verification solutions does Oski provide?
- What is the difference between using EC tools like Formality (Synopsys) or Conformal (Cadence), and deploying Oski’s formal verification solutions?
- What is an Oski Abstraction Model?
- What is the advantage of using formal tools with Oski Abstraction Models? What is the cost to performance in using formal tools alone?
- Can Oski verify third party IP?
Business
- Does Oski sell formal verification tools?
- When is the best time to introduce formal?
- Does Oski work with formal tools from all EDA vendors?
- If we do not have any formal tool licenses, can Oski help?
- If we have the tools and FV resources, why do we need Oski?
- We’re not sure we can spare our designers. Does Oski need designer time?
Methodology
- What is the difference between Model Checking (MC) and Sequential Equivalence Checking (SEC)?
- Why and when does Oski use Model Checking (MC)?
- Why and when does Oski use sequential equivalency checking (SEC)?
- What is Oski’s End-to-End Formal verification methodology? And how does it differ from Local Formal Verification?
- How does End-to-End Formal verification use Abstraction Models to maximize coverage?
- How can we be confident in the coverage results for end-to-end formal? How are the these coverage results verified?
- What design information do we need to have on hand before we engage in formal testplanning stage for end-to-end formal with Oski?
- Does Oski provide formal verification for analog?
- What investment of time and effort is required to build a set of constraints?
- We are using formal, but have not seen tools converge. How do Abstraction Models improve convergence with formal?
Training
- If we use Oski’s formal verification methodology services, will we also have an opportunity to learn to apply formal in-house, on our own?
- Who can become an expert user in formal? What skills are required?
- Who can we contact for more information?
- What is Oski Technology? Oski Technology is the world’s first and only formal verification services company to be fully focused on formal verification methodology for the successful deployment of verification tools. With over twenty years in formal verification, Oski’s CEO Vigyan Singhal and the Oski Formal Verification team has spent years developing and perfecting a set of proprietary Oski Abstraction Models. These Abstraction Models and related methodology have redefined the traditional approach to simulation-based verification of highly complex SoC designs at leading semiconductor and IP companies. Leveraging these unique formal abstraction methods with off-the-shelf EDA tools, Oski delivers the highest coverage with the fastest time to tapeout, sometimes replacing and sometimes complimenting simulation.
- What is formal verification? Formal verification is an alternate method of RTL verification, as compared to RTL simulation. Depending on the design size, any formal tool can face the same known problem of tool complexity, due to state space explosion of the reachable state space. However, a careful use of decomposition and abstractions can deliver sufficient formal verification coverage for End-to-End Formal Verification of large and complex designs. In particular, when Oski’s Abstraction Models are deployed in conjunction with formal tools, formal is known to provide higher coverage and faster verification schedule, on even the most complex designs.
- What formal verification solutions does Oski provide? Oski’s methodology and Oski Abstraction Models allow off-the-shelf EDA tools to scale for complex designs. Formal can be integrated with traditional simulation-based and coverage-driven flows at each stage of the verification process, reducing schedule and increasing coverage for better overall return on effort and a measurable productivity advantage.
- What is the difference between using EC tools like Formality (Synopsys) or Conformal (Cadence), and deploying Oski’s formal verification solutions? Formality and Conformal are Logic Equivalency Checking (EC) tools used to compare the equivalence of two different RTL or gate-level designs. These tools do not prove the correctness of RTL designs with respect to a functional specification. In contrast, Oski’s formal verification methodology complements or replaces simulation to prove correctness of RTL designs, so that formal can be properly integrated with traditional simulation-based and coverage-driven flows.
- What is an Oski Abstraction Model? An Oski Abstraction Model is a custom model (designed in Verilog, SystemVerilog and SVA) that abstracts certain implementation details from a given design. Abstraction Models are necessary to overcome the state space explosion problem, common with formal verification tools. Such models can reduce the formal tool runtimes many orders of magnitude, and previously intractable problems can be solvable. One published case study shows End-to-End Formal running on a design with more than a million flops in the cone-of-influence. Even though these models simplify design behaviors, they always add more behaviors to the design and do not reduce behavior. Thus, they do not cause any false positive results. Moreover, the correctness of such Abstraction Models can be separately formally verified through assume-guarantee methods.
- What is the advantage of using formal tools with Oski Abstraction Models? What is the cost to performance in using formal tools alone? Using Oski’s Abstraction Models, formal runtimes can be thousands of times faster than using formal without abstractions. Without Oski’s formal verification methodology and Oski Abstraction Models, the use of formal tools and techniques often lead to schedule delays and generate a low return on effort for complex designs. Abstraction techniques are used to reduce the state space of the design so that the formal verification tools can solve a computationally easier problem.
- Can Oski verify third party IP? Yes. Oski often formally verifies internally developed IP or licensed 3rd party IP. IPs are typically well-suited for formal verification. One well-known challenge for IP verification is the configuration explosion problem — through parameters, configuration registers, or ifdef’s, one IP design can be the source of hundreds of generated RTL designs. This configuration explosion can be nicely solved through a scalable formal verification methodology.
- Does Oski sell formal verification tools? No, Oski does not sell any formal verification tools. We license tools from vendors such as Cadence, Mentor Graphics, Synopsys and OneSpin. Our customers also typically have their own licenses for these tools.
- Does Oski work with formal tools from all EDA vendors? Yes. Oski’s solutions and Abstraction Models are effective with all formal tools — and necessary for the effective use of any and all formal tools on the market today. Oski supports all off-the-shelf EDA tools, and proprietary EDA tools. Oski has partnerships with Cadence, Mentor Graphics, Synopsys and OneSpin.
- If we do not have any formal tool licenses, can Oski help? Oski has strong ties to the R&D departments of leading EDA vendors, and agreements with some EDA vendors that allow us to use our formal tool licenses for building and delivering early-stage formal verification solutions. If you want to deploy formal verification internally in your company in the long-term, you will eventually have to buy licenses either from the vendor, or OEM from Oski.
- If we have the tools and FV resources, why do we need Oski? Even if you have the tools and FV resources to achieve end-to-end formal verification, there is significant risk of state-space explosion resulting in poor convergence for medium or large-sized designs. Oski Abstraction Models enable formal tools achieve unprecedented convergence by transforming the problem, allowing formal tools to analyze an alternate view of the design, and run thousands of times faster, resulting in convergence on end-to-end verification of designs as large as millions of state bits in the cone-of-influence of the verification problem.
- We’re not sure we can spare our designers. Does Oski need designer time? Oski can work without dedicated time from your designers. Oski works with customers just before tapeout to offload a verification long pole, often with very limited specifications, and using formal coverage methodology to derive the design behavior. If necessary, we start work with just the RTL and existing simulation waves, before iterating with the design or verification team.Table of Contents
- What is the difference between Model Checking (MC) and Sequential Equivalence Checking (SEC)? RTL-vs-C Sequential Equivalence Checking (SEC) can be used to formally compare RTL vs a C reference model. Model Checking (MC) is used to verify designs against a set of properties (or checkers).
- Why and when does Oski use Model Checking (MC)? Formal Model Checking (MC) is best applied on control or data transport, and multiple, concurrent streams that are difficult to completely verify using simulation. For example, arbiters of many kinds, on-chip bus bridges, power management units, DMA controllers, host bus interface units, schedulers, interrupt controllers, memory controllers, standard interfaces (e.g. PCI Express, USB).
- Why and when does Oski use sequential equivalency checking (SEC)? Sequential Equivalence Checking (SEC) is best applied on data transform designs, that contain sequential, math operations on input data objects or packets. SEC can be used to formally verify RTL against a reference model. Such a comparison can be used for multiple possible applications: e.g., comparing the RTL against a reference C model; comparing an RTL with clock gating against one without; proving the correctness of complex bypass logic using reference traffic that does not exercise the bypass. For example, for floating point units, graphics shading units, convolution units, MPEG decoders, classification search algorithms and instruction decoders.
- What is Oski’s End-to-End Formal verification methodology? And how does it differ from Local Formal Verification? Oski’s End-to-End Formal uses formal to verify most or all the functionality of a design, and replaces simulation at that level. End-to-End Formal verifies the correctness of RTL design behavior from the inputs at one interface of the design to the outputs at another interface of the design. This is different from verifying local RTL assertions (typically embedded in the RTL), or interface protocol checks at one interface of the design. Both styles of formal are useful, and required. End-to-end Formal typically requires a wider set of abstraction techniques than local formal verification. Local Formal Verification can often be effective for bug hunting, but does not reduce simulation effort or increase design verification coverage.
- How does End-to-End Formal verification use Abstraction Models to maximize coverage? With End-to-End Formal verification, formal verifies most or all the functionality of a design, and replaces simulation at that level; simulation may still be used at a higher chip-level, or system-level verification. For formal verification to become a part of verification signoff, the flow must deliver quantitative coverage results that measure the quality of the formal verification work. Such results should also be aligned and integrated with the simulation-based coverage measurements used in the signoff flows. Coverage results use exactly the same metrics as a simulation-based coverage flow, allowing for an easy integration of all coverage results.
- How can we be confident in the coverage results for end-to-end formal? How are the these coverage results verified? For many of Oski’s designs, formal has been used to find all bugs in a design, and has replaced simulation at that design-level. Simulation was still run at higher levels, e.g. at full-chip level, or system-level. Once Oski formal verification methodology is applied, formal code coverage can be measured to quantifiably complement simulation results, and integrate formal coverage metrics in an overall chip-level simulation and methodology.
- What design information do we need to have on hand before we engage in formal testplanning stage for end-to-end formal with Oski? A functional requirement specification is needed to understand the desired end-to-end behavior. If the RTL already exists, it is useful to pre-process the RTL with the formal tools to understand design details, and estmate complexity. Also, if simulation waveforms are available, they help in understanding the end-to-end functionality, faster.
- Does Oski provide formal verification for analog? No, Oski does not provide formal verification methodology to verify pure analog design.
- What investment of time and effort is required to build a set of constraints? Crafting a set of constraints requires effort and time, depending on the design and its interfaces with its neighboring designs. Constraints are often built interactively, on an as-needed basis. An alternative approach is to implement all possible known constraints up-front. In using this approach, it is important to be mindful of (a) over-constraints; and (b) adding too much complexity, which interferes with the proofs.
- We are using formal, but have not seen tools converge. How do Abstraction Models improve convergence with formal? The major challenge to achieving convergence with formal is a state-space explosion problem. Abstraction Models are developed precisely to address this formal convergence problem, by allowing off-the-shelf EDA tools to scale for complex designs. Furthermore, formal can be integrated with traditional simulation-based and coverage-driven flows at each stage of the verification process, reducing schedule and increasing coverage for better overall return on effort and a measurable productivity advantage.
- If we use Oski’s formal verification methodology services, will we also have an opportunity to learn to apply formal in-house, on our own? Yes. An important part of Oski’s service offering is to provide guidance in better understanding how to apply formal in your design environment, so you can make informed choices about how best to allocate design and verification resources. Knowledge of what is possible with formal verification, including how to identify which blocks are the best candidates for formal, enables you to better plan and execute verification strategy, resulting in improved coverage and faster schedule, and creates an opportunity for deepened focus on design.
- Who can become an expert user in formal? What skills are required? A PhD in formal is required to build tools, but you don’t need a PhD in formal to be successful with formal. Formal requires good problem-solving skills and the implementation of sophisticated methods and abstractions. These skills are more important than training or education, as formal verification requires so much white-box debugging. Formal verification and simulation require different kinds of solutions to overcome their respective convergence problems; to become an expert in formal, it is best to focus on formal on an ongoing basis.
- Who can we contact for more information? Please send email to info@oskitech.com or call +1 (408) 216-7728.