The verification of all configurations (reaching in millions) of an (silicon) IP is a challenge. I have experienced this problem first-hand both from the vendor side as an embedded SRAM (eSRAM) compiler designer, and from the customer side, as an architect of a wireless SoC using 3rd party IPs.

When I was eSRAM compiler designer, eSRAM used to support hundreds of thousands of configurations based on address widths, data widths, data masking, low power features, etc. In order to meet performance for different configurations, I sometimes designed different internal architectures of eSRAMs for different configurations. Due to the large number of configurations, verification is performed only on the configurations where the designer identifies the greatest need, for example when there is an architecture change either in the design or layout. Though this approach may appear to be comprehensive, I have seen silicon failures because the configurations picked for silicon had not been verified. The failures were due either to design modeling error or layout programming error. These failures could have been caught at the verification stage, if all configurations of eSRAMs were verified. However using simulation as the sole verification technology, verifying all configurations was simply not possible.

When I started building a wireless SoC (for transferring video real time), my team developed baseband (BB) and medium access control (MAC). For the rest of IPs, we decided to source from external 3rd party IP vendors, thinking that it would save us time and money since the IPs would be mature, in another word, completely verified. I needed some specific cuts of eSRAMS and a specific configuration of flash memory controller for my SoC and contacted 3rd party IP and library vendors for the same. When I asked the vendors about the maturity level of their IPs, they ensured me that their IPs are “Silicon Proven” and hence I should not worry. My experiences as an eSRAM designer have taught me that “Silicon Proven” configurable IPs may not mean that my specific eSRAM cuts and flash controller configuration were verified on silicon. So, I inquired if our particular requirements were proven on silicon. Not surprisingly the answer was negative. When I asked the IP vendor if we could get the testbench of the flash memory controller so we could verify our specific configuration, he pointed me to a verification IP (VIP) company. We were paying for an IP that was not fully verified. Moreover we had to pay for a VIP to verify that unverified IP (what a shame!).

I wondered if this this challenge was faced by every designer using 3rd party IP, and if there might be a better solution. Enter Oski Technology.

These days I work with Oski Technology where I deploy formal verification for verifying complex blocks of SoC and vendor IPs, and I no longer worry about missing corner case bugs. Formal tools explore all possible (legal with constraints) inputs for the design under test (DUT) and are hence able to find all corner case bugs. Moreover, by using end-to-end checkers, we verify the end-to-end functionality of the design. This means that even if the internal design architecture is changed, there is no need to change my verification setup for verifying DUT (awesome!).

Recently, Oski formally verified all possible configuration of a configurable IP (over 1 million combinations) using just one (yes, just one) formal testbench. The testbench is written in way that IP customers can use the formal testbench as VIP to verify the specific configuration in use so they can be fully confident that the IP will not fail in silicon.

The benefits of formal verification for IP vendors and their customers are summarized below:

1. For IP vendors, “Formally Certified” IP is better than so called “Silicon Proven” IP, as all configurations are verified formally (no corner case bugs!). This can be an competitive edge for the IP vendors
2. By using end-to-end checkers in formal verification, there is no need to change the testbench even if internal design architecture is changed, saving time and effort
3. For IP customers, the formal testbench (formal VIP) can be used to further ensure the specific configurations in use do not cause any integration issues with the rest of the SoC.

Given these benefits, why aren’t all IP vendors using formal technology to verify their IPs? We will discuss this question and Oski’s approach in future blog posts, so stay tuned!