Efficient transistor-level symbolic timing simulation using cached partial circuit states

Previous work has demonstrated the feasibility of transistor-level symbolic timing simulation, using MTBDDs to share computations across input combinations with similar behaviors. This paper introduces an alternative approach using cached Partial Circuit States paired with simple BDD guards. The proposed approach improves efficiency by decoupling the numerical and Boolean computations required for symbolic circuit simulation, with no loss of verification capability. The logical computations become more efficient by using BDDs, which have more significant internal sharing since they are no longer differentiated by floating point terminal values, and which can now take advantage of the classical BDD negation pointer method. The numerical computations benefit as well, by enabling caching of circuit-level computations and reuse across similar topologies and multiple time-steps in the simulation. We have implemented this approach in a commercial symbolic simulator, and validated the performance benefits in the verification of 21 industrial designs.