Analysis of digital circuits through symbolic reduction

The authors describe a semi-algorithmic method to extract finite-state models from an analog circuit-level model by means of homomorphic (behavior preserving) transformations. Properties to be verified are defined by ω-automata. Efficient algorithms for testing language containment of automata can then be applied to verify properties of the finite-state models. Proof of the property in the finite-state model guarantees the property in the analog circuit-level model over a continuous range of input waveforms and circuit parameters. While in practice this method applies directly only to smaller circuit components, it can be used to analyze larger circuits as well by deriving a hierarchy of increasingly abstract models, through repeated applications of homomorphic transformations. Examples of extraction, homomorphism, and verification are described