Ad-hoc translations to close verilog semantics gap

This paper describes rules to transform Verilog HDL source code in order to propagate X-values on RTL models in a more realistic way, and to check for potential differences of RTL simulation results against expected silicon implementation behavior. By running X-propagation simulations in parallel to usual RTL simulation and debugging, RTL design bugs previously detected in gate-level simulations can be detected earlier now. A prototypical tool automatically implements the proposed transformation rules. Experimental results on two industrial hardware designs validate the usefulness of our approach and justify its application in everyday use.