Verifying real-time properties of MOS-transistor circuits

A verification approach which allows the verification of functional and timing behavior of circuits at transistor level is presented. It is aimed at the verification of asynchronous interfaces and standard-cell library modules. In contrast to other approaches, timing is explicitly considered, allowing one to verify timing-dependent effects with a high degree of accuracy. To conveniently specify desired properties, a specification language based on Linear Quantized Temporal Logic (QLTL) is provided. For an efficient verification, input constraints, necessary for a proper circuit functioning, are converted into input constraining automata, reducing the reachable state space and providing a model linearisation, necessary to prove linear QLTL formulas by branching CTL model checking