Verilog X-Bugs: simulation/coverage vs formal verification

MikeTurpin

I'd like to raise awareness of problems with X-semantics in Verilog, and begin a discussion here about how this affects validation. The problems include:

1) RTL simulation can optimistically pass tests that could fail netlist sims
2) Code-coverage results can be both optimistic (i.e. claims branch is covered when it's unreachable) and pessimistic results
3) Formal equivalence checkers are not usually set up to detect X-bugs
4) Formal property checking gives more accurate results than RTL sims (e.g. might fail a property that would optimistically pass RTL sims)

I presented a paper on these issues at Boston SNUG 2003, which won the Technical Committee award. It can be found on SolveNET and also at:

http://www.arm.com/pdfs/Verilog_X_Bugs.pdf

In addition to highlighting the problems, my paper also gives some solutions - often involving the use of formal verification.

I'd be interested in other people's experience of Verilog X semantics causing verification problems, and on the propsed coding rules in the paper (particularly the recommendation to not use if-statements in combinatorial logic).

alain · Junior Joined: Jan 11, 2004 Posts: 5

JZook · Posted: Mon Jan 12, 2004 5:44 pm **Post subject:**

Because of this paper and others, and our own experience, we no longer trust X's in RTL simulations.
For reset testing, we wrote a perl script to parse the Verilog RTL files (just one module per file allowed) and add an initial block where all reg's are assigned a random value. The perl script took a couple man-weeks to perfect (because our designers aren't real consistent in how they declare their reg's), but it runs plenty fast, and the initial blocks do not noticeably slow down the simulations.

I have heard other people (Duane Galbi in a SNUG a couple years ago, for example) say they did something similar through the PLI, which would probably be harder to get right, but has the advantage of not modifying the RTL.
_________________
John Zook
Senior Verification Engineer
Tilera Corporation

jeffli · Senior Joined: Jan 09, 2004 Posts: 32

You can also get X values in Verilog from Z values. Most gates and expressions in Verilog generate X if any input is Z. Z values can be from explicit Z in constants, certain Verilog gates or undriven nets. These Z values can cause possible X-bugs though it is probably not as likely as the others.

MikeTurpin · Posted: Tue Jan 13, 2004 2:17 pm **Post subject:**

I was hoping for a reaction to my "avoid if statements" rule, it's also proved controversial at ARM. I agree completely with the comments:

a) if statements are more readable
b) don't use nested ternary ?'s

For (a), if-statements may be intuitive and easily understood by engineers but are dangerous as EDA tools often take a different interpretation of the semantics.

For (b), why not rewrite nested if statements as a case statement (or possibly casez) as this is priority encoded? I've now rewritten several nested if statements as case (sometimes with single ?'s in the assignments) and this can be more readable (or easier to spot problems/redundancies).

My RTL coding rule is meant as "avoid using if's" but if you do use them you need to:

- be aware of the issues
- reset all DFFs
- add X-checking assertions
- run automatic formal proofs

So, if-statements could mean a whole bunch more work. If you have a control block, then all DFFs should be reset and you could have X-checking assertions on the I/O to protect any if-statements.

Not all X's are evil though - some are good (X-propagation is better than optimistic termination). I think that mcurry's code could have a following case default (providing that all 2-state values of "blah" are covered by a case-item) so that X's can be trapped by the default and propagated onto each output. This could still be concise and achieve the desired effect of not having to specify every output on every case-item.

You can also do the all X's -> 1's, 0's or random by using initreg in VCS.

MikeTurpin · Posted: Wed Jan 14, 2004 11:48 am **Post subject:**

srini

MikeTurpin

Hi Srinivasan,