The Dangers of Living with an X (bugs hidden in your Verilog)
The semantics of X in Verilog RTL are extremely dangerous as RTL bugs can be masked, allowing RTL simulations to incorrectly pass where netlist simulations can fail. Such X-bugs are often missed because formal equivalence checkers are configured to ignore them, which is a particular concern given that equivalence checking is fast replacing netlist simulations. This paper gives examples of such problems in order to raise awareness of X issues in many different parts of the design flow, which are often poorly understood by RTL designers and EDA vendors alike. It gives practical advice on how to overcome X issues in new designs (including good coding styles) and techniques to investigate them in existing designs (including automated formal proofs). New terminology is introduced to differentiate subtle interpretations of X by EDA tools, along with recommendations to avoid problems. In particular, this paper describes how to change the default settings of equivalence checkers to find hidden bugs (that are otherwise far too sneaky to detect). In short, if you are using EDA tools for simulation, codecoverage, synthesis or equivalence checking, you must be aware of the problems and solutions described in this paper.
This document is only available in a PDF version. Click Download PDF to view. Download the PDF from the menu on the right.