Symbolic simulation is a formal verification technique that adds thecapabilities of symbolic methods to conventional simulation methodologies. In symbolic simulation, for each input, a symbolic variable is introduced that represents all values that this input may take. The symbolic simulator then computes symbolic expressions for each output in terms of the input variables. These expressions implicitly represent the values of the outputs for all possible input assignments.

This paper presents methods that enable symbolic simulation of thecomplete set of Verilog HDL constructs including delays and events. Thekey contribution of this work is that it shows that a symbolic simulator with complete Verilog IEEE 1364-1995 semantics is feasible, and that all language constructs can be simulated symbolically.

The paper starts with a discussion about problems with existing symbolic simulator tools, especially in dealing with design testbenches. Related work is thoroughly surveyed to show the contribution of the work. Principles of symbolic RTL simulation are explained in an interesting tutorial style that demonstrates the challenges of symbolic simulation at the RT-level, especially if delay- and event-control is involved.

The paper proposes the event accumulation mechanism as a means to reduce the average complexity of event driven simulation. The technique introduced combines execution paths that were split due to unbalanced delays or events. This approach has the advantage of allowing testbench simulation with minor changes. Possible problems of the proposed approach are also discussed and handled.

This paper will be interesting for researchers, especially graduatestudents, working in VLSI simulation and formal verification and CAD tool design. The discussion about the implemented simulator and the experimental results are very informative.