Simulation Needs for Edge Related X propagation problems

[smeyer0028]

This is to amplify Andrew's answer to the X propagation discussion
and explains why we think only simulation can find gate level X's
handled incorrectly by normal Verilog semantics especially X propagation
problems that involve edges.

http://www.semiwiki.com/forum/conten...dangerous.html

There have been some recent posts about problems with the standard
Verilog simulation of unknown propagation semantics in RTL level Verilog.
Here is a quite common type of post from an engineer:

>> I've seen some non-intuitive behaviors specified by the Verilog standard
>> that, in some cases, contradict one's understanding of the 'x' semantics.
>>
>> As a result of these mismatched behaviors, many users will spend long hours
>> debugging 'x' problems in gate-level simulation that run extremely slowly.

>> It would be a nice feature if VCS/NC-Sim/Questa had a command-line flag that
>> causes them to simulate RTL 'x' scenarios in a way that better resembles a
>> gate-level situation (Design Compiler output), or better yet, equivalent
>> results to stressing '0' and '1' for every 'x'.

I am not sure if Semiwiki readers are aware of the fact that our
Tachyon DA CVC Verilog compiled simulator has a better and faster
implementation of X propagation semantics (+xprop option) than other
simulators.

CVC +xprop when run on pre-synthesis RTL designs can eliminate the need
for slow and difficult post synthesis gate level debugging without much
additional simulation time compared to our already fastest CVC full P1364
simulator.

Basically, our +xprop feature is much more pessimistic in producing
X's in RTL simulation so results match gate level behavior. In this
example assume cond cond='x':

if (cond) res=2'b00;
else res=2'b11;

Normal Verilog: res = 2'b11;
CVC with +xprop: res = 2'bxx;

There are even more subtle problems that CVC's X propagation algorithm
finds. For example assume sel is 3'bx0x:

case (sel)
3'b111: res = 3'b101;
3'b101: res = 3'b000;
3'b000: res = 3'b010;
endcase

Here because both cases 101 and 000 can potentially match, res will have
value 3'b0x0;

CVC with X-propagation can help find these and other unknown value related
bugs during RTL simulation that static formal tools can not find. Overhead
for +xprop for most designs is < 30%.

In addition to our normal +xprop option, CVC has some options that
will find and inject X's into simulation results for all X conditionals.
It is useful for design styles that do not allow unknowns at all. The full X
injection option has the problem that X's which are don't cares during
synthesis allow the synthesizer to potentially produce better gate level
implementations.

If any Semiwiki readers would do a comparison of CVC's +xprop results
versus other improved X Propagation tools, we would be all for it.

[paulki]

Im interested to benchmark CVC with Verdi.