A symbolic core approach to the formal verification of integrated mixed-mode applications

In the past, formal verification-the promising alternative to simulation-based verification-has primarily been applied to digital system designs. Despite the ever-growing importance of integrated mixed analog/digital systems, hardly any formal approaches have been introduced to verify such designs. In this paper, a preliminary study of a symbolic modelling technique is presented which allows us to formally verify the functional correctness of integrated mixed-mode systems. The usefulness of the approach has been demonstrated by verifying the SmartPen^TM a practical integrated mixed-mode application