close By using this website, you agree to the use of cookies. Detailed information on the use of cookies on this website can be obtained on OneSpin's Privacy Policy. At this point you may also object to the use of cookies and adjust the browser settings accordingly.

ASIC synthesis verification from RTL code to final netlist

Systematic design errors, introduced by automated design refinement tools, such as ASIC synthesis, can be hard to detect, and damaging if they make it into the final device. Formal Equivalency Checking (EC) has become a standard part of the ASIC development flow, replacing almost all gate level simulation with a rigorous consistency check between pre- and post-synthesized code. 

OneSpin 360 EC-ASIC excels by automated state and phase mapping, automatic handling of sequential optimizations such as clock gating and pipeline retiming, and more, leveraging decade-long technology development and field use. 

Highlights

  • Exhaustively proves that design functionality is maintained through all implementation steps
  • Slashes verification time and effort by automated state and phase mapping
  • Significantly reduces debug time by precise location of bug observability points
  • Detects more synthesis bugs and synthesis/simulation mismatches than conventional equivalence checkers
  • Uses an extensive set of fully automatic design consistency checks to rapidly detect common coding errors
  • Leverages decade-long technology development and field use

Fast time to results

The OneSpin® 360 EC-ASIC Equivalence Checker thoroughly proves, without simulation, that design functionality is maintained through all implementation phases of a design, such as design revisions, synthesis and optimizations, made from RTL to the final netlist – RTL-RTL, RTL-gate and gate-gate – in ASIC/SoC designs.

The tool fully automates state and phase mapping via proof-based sequential analysis. A design conditioning component and highly accurate design modeling detect synthesis bugs, synthesis/simulation mismatches and RTL coding bugs that often escape conventional equivalence checking. 

360 EC delivers dependable results because it operates completely independently of any synthesis tool, requiring no special synthesis "side files" to handle crucial phases of the equivalence checking flow, such as state mapping, datapath analysis, and ECO verification. 

Automated State Mapping

360 EC-ASIC achieves fast time to results by using highly automated proof-based sequential analysis to accelerate the mapping of state-holding design elements necessary to capture combinational logic behavior across latch boundaries. This full semantic analysis produces "right first time and all the time" results, eliminating the manual, time-consuming, error-prone iterations generally necessary when using tools that employ name-based mapping routines. The same analysis also automatically and reliably generates the associated phase mapping of sequential elements.

Automated Debug

OneSpin 360™ EC-ASIC significantly simplifies and speeds debug, using a proof-based analysis and diagnosis capability that locates bug observability points with pinpoint accuracy.

Rapid cross-referencing between the RTL and the gate level netlist then minimizes the back-tracing necessary to locate the bug itself. The 360 EC-ASIC's debug capabilities facilitate a systematic and well-structured debug approach, including value annotation to source code as well as full cross-highlighting between source browser, schematic engine and hierarchy browser, with driver and load tracing.

Comprehensive Bug Detection

The 360 EC-ASIC's accurate modeling and sequential analysis detect synthesis bugs, synthesis/simulation mismatches and RTL coding bugs, including the following checks:

  • Synthesis full_case
  • Synthesis parallel_case
  • Bus contention
  • Bus floating
  • Division by zero
  • Negative divisor, exponent or remainder
  • Don't care and X assignment
  • Read/write, write/write race conditions
  • Function without return
  • Array boundaries
  • Range overflow
  • Stuck-at
  • Initialization
  • Dead code
  • User defined

The tool adheres to either simulation or synthesis semantics, and can be configured to obey VHDL's 9-valued and Verilog's 4-valued semantics. It supports advanced, configurable controllability and observability "don't care" handling in RTL-RTL and RTL-gate comparisons.

Example Projects

For example, the 360 EC-ASIC found a synthesis bug for a baseband chip resulting from a "full_case" directive, that is – an incorrect or illegal synthesis tool constraint – which would have necessitated a design respin. Other tools may have given an imprecise warning of a problem, or missed the bug altogether. 

In another setting, 360 EC-ASIC's precise "don't care" handling enabled it to detect a synthesis/simulation mismatch in a commercial microprocessor IP design. The IP vendor removed don't care assignments, essentially changing the entire don't care handling strategy.

A leading semi-conductor company developed new peripherals and formally verified them using the true functional sign-off methodology of 360 MV. These peripherals have been integrated into 2 ASICs – each of 4 million gates – constituting the central components of a large multiprocessor system. Afterwards, 360 EC-ASIC has been employed to preserve the achieved extreme level of quality through subsequent implementation steps. These ASICs worked right the first time, met an ambitious project schedule, and were critical for the business success of a large wireless communication systems company.

Feature Summary

  • Requires no change to the design team's existing design flow
  • Significantly eases chip level simulation by ensuring equivalence between implementation levels
  • Deploys multi-threaded proof engines
  • Verifies multimillion gate designs
  • Handles large multipliers, operator merging and resource sharing with datapath analysis capability
  • Supports low-power implementations and clock gating
  • Focuses debug with logic cone extraction and highlighting
  • Avoids false negatives associated with library cells by qualifying cell libraries with sequential checking
  • Supported design languages: Verilog, SystemVerilog, VHDL, EDIF, Liberty and mixed languages
  • Supported computer platforms: Linux, Solaris

Get in touch!

Thoroughly verify ASIC synthesis from RTL code to final netlist and try 360 EC-ASIC now!

» Contact