Fujitsu: Efficient Static Verification Sign-off for High-value Failure Mode

Executive Summary: DAC 2019 presentation by Atsunori Machida, Fujitsu Kyushu Network Technologies

Ascent AutoFormal
Meridian CDC

Case Study Presentation Overview

Atsunori Machida, Fujitsu Kyushu Network Technologies, presented a case study on Fujitsu’s static verification sign-off methodology utilizing Real Intent tools.

Machida-san presented results that include a 30% reduction in simulation time from using Ascent AutoFormal, along with weeks of debug time savings from Meridian CDC.

Fujitsu Kyushu Network Technologies Background

Fujitsu Kyushu Network Technologies is a Fujitsu subsidiary in Japan with about 900 people.

The company does research and development of hardware, firmware, and software. Their focus is mainly networks, and their core technology is network signal processing with video voice AI, along with IoT, AI, automotive and medical.

Atsunori Machida, Fujitsu’s speaker on this topic at the Design Automation Conference, is an ASIC and FPGA project manager for those applications.

SoC RTL Verification Requires Static Analysis

Fujitsu uses a static approach due to the large and complex SoC logic scale.

With hundreds of IPs and hundreds of clock domains, a huge amount of verification is needed. Additionally, the complexity creates a risk of missing bugs during the design process.

Fujitsu determined that a static approach was essential to improving quality and finding specific failure types early.

SoC Static Verification Challenges

Early RTL sign-off using formal verification requires running more than 100,000 checks. Further, failure symptoms and root causes are mixed, so it is difficult to find the real root cause manually.

Additionally, Fujitsu saw challenges with clock domain crossing set up, due to having 100s of clock domains and the CDC tools requiring specific knowledge and skills to achieve precise analysis.

If a designer fixes the wrong thing — i.e. the symptom and not the root cause — it can create excessive design iterations. The upshot is bugs can be missed even with a static approach. Thus, Fujitsu said they needed an effective static approach to solve these problems.

Static Verification

Efficient Static Sign-Off Requires Tools & Methodology

Fujitsu’s goal was to introduce effective static verification tools while establishing a systematic method.

To achieve this, they required tool set up guidelines and prioritization of the failures (to focus their debug effort).

Fujitsu determined that Real Intent’s static verification tools — Ascent AutoFormal for automated formal verification and Meridian CDC for CDC checking, had functions for both setting up the checks and prioritizing the failures.

Static Tools — Key Functionality

Fujitsu evaluated the usability and efficiency of the two Real Intent tools in a trial project case study. They determined that the tool organization of relevant information made debug easier. The examples they gave are listed below.

  • The setup check results are listed here as environmental information.
  • The bug failures are listed & well-categorized.
  • A ‘big picture’ overview of failures & warnings in the design, which helps with debug.
  • Multiple views of the failures, such as schematic view, source view and waveform view.
  • The causation tree window was important for formal verification because it enabled them to quickly identify the root cause.

Fujitsu indicated that Real Intent’s root-cause priority listing (primary secondary categorization) and well-organized GUI reporting saved them design debug iterations.

RTL Verification

Automatic RTL Verification Results: 30% Reduction in Simulation Time

Fujitsu was able to achieve efficient RTL sign off with static tools.

First, they were able to complete whole chip analysis with Real Intent AutoFormal. Fujitsu compared their experience with another tool they also tried, which they said gave up and “exploded”.  This is because Real Intent’s static tool engines are customized for specific failure modes like AutoFormal and CDC.

Second, Fujitsu performed focused checks for behavioral control, FSMs and tristate drivers, and were able to find critical deadlocks in FSM.

AutoFormal enabled a 30 percent reduction in logic simulation time. This simulation reduction was based on AutoFormal’s ability to identify the root cause error as a primary failure, with other violations detected as warnings.

Fujitsu compared this root cause analysis with another tool. For FSM checks, AutoFormal reported 1 primary error and 9 secondary warnings, while the other tool just presented all 10 as