Symbolic verification of CMOS synchronous circuits using characteristic functions
Yuji Kukimoto, Masahiro Fujita, Masamitsu Tanaka · 2002
The authors present a functional verification method for CMOS synchronous circuits by representing circuit behaviors with characteristic functions. Bidirectional signal effects and charge effects are formalized based on these functions. This method makes it possible to verify dynamic switch-level circuits, such as pass-transistor networks and precharge logic circuits, which cannot be accurately modeled at gate-level. An automatic switch-level verification system has been implemented, and experimental results are reported.>