High-Risk Blocks Formal Sign-Off

Formal Verification of Software Configurable Silicon

Problem: Parallelism & “Superbugs”

The surge in parallelism and functional complexity has led to an increase in insidious bugs that are impossible to find pre-silicon using simulation or traditional formal methods. High-risk blocks with parallel structures, multiple power modes, concurrent processing, and/or multiple operational modes overwhelm simulation and lead to silicon bug escapes.

These blocks have too many combinations to test in simulation to completely cover all temporal relations between events. Additionally, finding one of these “superbugs” is a strong indicator that there are related bugs nearby, making it difficult to predict when all the bugs will be fixed, and the chip will be approved for tape-out.

Superbugs are always root-caused to concurrent logic blocks and never to sequential logic blocks. To restore chip-level, sign-off confidence we need a verification strategy that will predictably close all logic in “project time”:

  • Concurrent Logic: formal sign-off methods find all bugs, including bugs caused by parallelism, in these high-risk blocks.
  • Sequential Logic: advanced simulation methods can effectively close these blocks.

Oski’s High-Risk Block Formal Sign-off Services

Formal sign-off proves the absence of bugs. It is the only method that guarantees that all bugs have been found in your high-risk blocks before your schedule says it is time to tape-out.

We’ll find all the bugs in your high-risk blocks.

  • We rank your high-risk blocks by bug-escape risk.
  • You will not need to simulate the blocks that we formally sign-off.
  • If you modify your RTL, our follow-on proofs are also exhaustive.
Your chip-level coverage will be higher and ramp faster.

  • You will know there are no bugs remaining in your High-Risk Blocks.
  • If we start early, we can sign-off your high-risk blocks to be bug-free by mid-project.
  • Formally signing-off the concurrent logic blocks enables your verification team to focus on sequential logic blocks.
Your designers will spend less time on debug.

  • We find major bugs early, so your designers have the freedom to create a proper fix or even re-architect the design.
  • Fewer than 10% of bugs we report are false negatives.
  • It typically takes 5 to 30 minutes to root cause a bug with our concise counterexamples and analysis.

Susceptibility to Simulation Resistance by Application Domain

Below are examples of high-risk blocks by Application Domain that Oski has formally signed-off.

CPU

GPU / AI / ML

Networking

Ethernet

Wireless

CPU

  1. Instruction fetch queue
  2. OOO functions: register rename, reorder buffer and retirement
  3. Instruction scheduler
  4. Execution units
  5. Load-Store unit
  6. L2 cache
  7. Coherency manager

GPU / AI / ML

  1. Resource manager
  2. Instruction scheduler
  3. Execution units
  4. Load-Store unit
  5. L2 cache

Networking

  1. Forwarding engines
  2. Linked-list controllers
  3. Buffer managers
  4. Crossbar switches
  5. Packet parsers
  6. Quality of Service (QoS) units
  7. Framers

Ethernet

  1. Physical Layer
  2. Lane-to-Lane de-skew buffer
  3. Elasticity buffer
  4. Block aligner
  5. Link Training and Status State Machine (LTSSM)
  6. Data Link Layer
  7. Flow control credit counters
  8. Transaction Layer
  9. Packet encoder/decoder

Wireless

  1. Datapath controller
  2. Bypass cache and forwarding logic
  3. Demodulator Frontend
  4. MAC Protocol Control Unit (PCU)
  5. Packet parser
  6. Framer
  7. MAC DMA engine

Oski can provide a first-level analysis of how formal sign-off can dramatically improve your chip-level, tapeout confidence and where simulation will be sufficient.

Oski’s Engagement Process