A Symbolic Modelling Approach for the Formal Verification of Integrated Mixed-Mode Systems

In this paper, a symbolic modelling approach is presented for the formal representation and verification of mixed analog/digital systems. The proposed modelling technique can be incorporated in the SFG-Tracing – a pragmatic methodology originally aimed at the formal verification of digital (VLSI) designs. Existing symbolic analysis and reasoning techniques can be employed to analyse the digital subsystems of a mixed analog/digital design. The development of appropriate, symbolic models to express the functional behaviour of the individual analog components, ultimately enables us to exploit a symbolic evaluation or simulation tool to formally verify the overall functional behaviour of a mixed-mode system.