A Scalable Symbolic Simulator for Verilog RTL

Symbolic simulation is an important technique used informal property verification and test generation for digital circuits. Existing symbolic simulators predominantly operate at the gate level, reasoning about individual bits and signals. As a result, their performance does not scale well to large circuits like microprocessors. Word-level symbolic simulators address this problem to some extent, but present other challenges, such as fixpoint detection when simulating multiple modules that mutually trigger each other. In this paper, we present some exploratory ideas for performing word-level symbolic simulation over a Verilog RTL description of a circuit. We outline the basic technique of simulation and of handling fixpoints, discuss issues faced in our approach and present solution techniques to counter these issues. We also present initial experimental results obtained by applying our algorithms to a Verilog model of an x86 processor design.