An Integrated Verification Architecture

Abstract:
Research in formal verification is hampered by a lack of an integrated verification architecture. Each verification tool in development typically uses its own language for models and properties. This fact means that when a designer wants to verify their system using multiple verification tools, it often requires a time-consuming and error-prone recoding of the model. Furthermore, a system includes both digital and analog hardware, software, and a physical operating environment. Each part of the system may be better encoded with a different modeling formalism and analyzed using a different methodology. For example, digital hardware may require accurate timing, analog circuits require accurate continuous dynamics, software needs efficient data representation, and the operating environment may be stochastic in nature. An integrated verification architecture would enable each part of the system to be represented and analyzed using the appropriate framework. This talk will describe our experiences in verification of heterogeneous systems including asynchronous, analog/mixed signal, and genetic circuits, and looking forward to how these methodologies can be unified into an integrated framework.