Avery Design, A leading Verification IP and X-Verification EDA tool provide a new tool to complete the
offering. Today you may use Avery’s EDA tools for X-Verification at RTL Level as well as at Gate Level

SymXprop – Semi-Formal RTL XAnalysis

Design practices involving partial reset, uninitialized memories, clock and power gating as well as
regular RTL coding bugs expose SystemVerilog’s inaccurate RTL X handling semantics by creating

Xoptimism and X-pessimism issues in RTL simulations. This often results in needing to expend extra
engineering time to effectively debug and fix real bugs or work around false positives. SymXprop
analyzes X propagations in RTL simulations for combinatorial and sequential X inaccuracies using
patent pending hybrid formal analysis and automatically eliminates these X inaccuracies in RTL
simulations.
Highlights

  • Analysis modes for X-optimism and X-pessimism
  • Analyze one or multiple submodules displaying X issues
  • Scalable to large designs with built-in distributed parallel processing
  • Supports VCS, Xcelium, and Questa simulators

Run RTL Simulations Free of All X Inaccuracies

SymXprop uses symbolic simulation and formal methods running in lock-step with logic simulation to
provide a dynamic, high accuracy X resolution function eliminating X-optimism or X-pessimism for the
true hardware accurate logic simulation. Both combinatorial and sequential analysis is performed
catching and resolving X-pessimism caused by re-convergent sequential paths that may take many
clock cycles to express.
Setup involves adding SymXprop APIs to the testbench to identify which submodules of the design to
perform the analysis on and when to start or stop analysis. During RTL simulation, SymXprop gets
called when a new X presents itself. SymXprop treats the X as a symbolic variable and then performs
symbolic simulation and a formal proof to determine whether there is X-optimism or X-pessimism and
then resolves the true hardware accurate simulation value for logic simulation to proceed with.
SymXprop utilizes Avery’s SymFormal, symbolic simulator and formal engine infrastructure, which
supports distributed processing for improved runtime performance.
Overall when using SymXprop only real X’s remain and can be more confidently dealt with as either
design bugs due to their presenting unacceptable non-determinism in the design function or as
acceptable don’t cares.

Contact us for more information

want to know more?
contact us now

Subscribe to
Newsletter