Symbolic functional and timing verification of transistor-level circuits

We introduce a new method of verifying the timing of custom CMOS circuits. Due to the exponential number of patterns required, traditional simulation methods are unable to exhaustively verify a medium-sized modern logic block. Static analysis can handle much larger circuits but is not robust with respect to variations from standard circuit structures. Our approach applies symbolic simulation to analyze a circuit over all input combinations without these limitations. We present a prototype simulator (SirSim) and experimental results. We also discuss using SirSim to verify an industrial design which previously required a special-purpose verification methodology.