Achieve End-to-End FormalTM verification and
complete coverage with Oski Formal
Methodology and Abstraction ModelsTM!
Regardless of application, the logic of a design block falls into one of the three categories:
Different types of designs are suitable for different verification strategies. For example control intensive logic and data transport logic are good candidates for model checking (MC), whereas data transform logic is a good candidate for sequential equivalence checking (SEC). It is important to spend time on formal test planning so that the correct technology is deployed to verify the right block, so as to reduce overall verification cost and effort.
Oski has used formal technologies to verify all kinds of designs, as demonstrated by the diversity of our customer list. Contact us to find out what further can be done to verify your design.
Many blocks in a CPU design are good candidates for formal verification. Below is a block diagram of ARM Cortex-A15 processor, used only as an illustration. The blocks highlighted in yellow are suitable blocks for formal verification.
Some example properties that can be verified using formal verification include:
These properties are hard to verify with simulation, but formal technology that uses symbolic representation and Oski Abstraction Models can catch many corner case bugs. Some example bugs that are discovered include:
Modern processor designs include many CPU cores, so it is even more important to use formal technology to exhaustively verify these CPU sub-blocks to minimize the verification effort at the top level, thereby reducing verification cost and shortening time to market. Oski can assist you with the complex tasks of processor verification using formal technology and Oski Abstraction Models.
Most SoC designs today consist of ARM processors, internal and/or 3rd party IPs and are based on standard or custom bus interfaces. Many blocks in such SoC are good candidates for formal verification to replace simulation when doing functional verification.
The following diagram shows a conceptual SoC: the blocks in yellow and orange can be verified using model checking (MC) or sequential equivalence checking (SEC). For example, in a wireless subsystem consisting of MAC (Media Access Control), BB (Base Band) and radio (RF) blocks, the MAC can be verified using model checking, the BB can be verified using sequential equivalence checking by comparing RTL with the C reference model, and the RF should use the traditional simulation for verification. The whole wireless subsystem should still be verified using simulation, however with the verification effort spent in formally verifying MAC and BB, the effort and time it takes to simulate the whole wireless subsystem would be significantly reduced.
Oski has performed many projects on SoC verification and can assist you in identifying the best blocks for formal technology so you get the best verification ROI, taking advantage of the strength of both formal and simulation in your verification flow.
IPs are major building blocks of today’s SoCs. Most IPs today are highly configurable to satisfy the different needs and requirements of IP consumers. For example, a DDR memory controller can have the following configurations:
Taken together, a DDR memory controller could offer more than 1 million different configurations, impossible for IP providers to verify all the configurations using simulation. By the same token, IP consumers can never be sure the configuration they have in use are thoroughly verified by the IP provider.
The solution to the problem consists of two parts:
Oski can assist IP providers (external 3rd party or company internal group) to formally verify highly configurable IPs. “Oski Certified” IP means quality IP, a competitive advantage for IP providers.
Most DSP designs are “data transform” designs that change the value of the data based on certain functionality, such as convolution, FFT, and inverse quantization. Often DSP designs start with a C reference model and the RTL model can be manually written based on the high level spec or automatically generated using high level synthesis tools. For these types of designs, sequential equivalence checking that compares the RTL with the golden C reference model can offer the formal confidence that the RTL design is correct to the spec. Unlike combined equivalence checking tools that are easier to use and debug, sequential equivalence checking often requires constraints and Abstraction Models in order to converge.Oski can assist you in applying the SEC tools effectively for your DSP designs.