X-propagation and reset-like test

SystemVerilog
1

Hi

we are adding 2 types of checks:

  1. x-propagation
  2. reset tests (i.e. create reset at a random place and rerun test to see that nothing get stuck)

the assumption is that all/most deadlocks and problems will be detected in x-propagation
what do you think about added value of such reset tests ?
For deadlocks/overflow/… detection - is something beside x-prop is needed?
(i mean using simulation - formal usage has good potential to catch deadlocks/overflows/… but it has limitations especially if we want to test big design)

note: X-prop has some different models (vcs for example has tmerge and xmerge) - not sure it is easy to fully utilize tests in the different models

thanks,
N.

2

In reply to Noam Elbaum:

Simulation in Verilog/SystemVerilog is poor at handling X propagation and especially X re=convergence. Simulation x-prop models only take care of a few, localized cases.

You might want to take another look at formal applications once you realize that the performance advantage you though you had in simulation gets lost in all the random x-prop simulations you have to run in a slower x-prop mode.

Formal analysis is great at extracting FSM for deadlock/unreachable states with no user intervention. And liveness/safety assertions can provide design confidence you cannot get with simulations.