Formal verification of bond graph modelled analogue circuits

Analogue circuits are an increasingly critical component in embedded system designs. Traditionally, simulation is used for verification, but owing to the infinite state space of analogue components, the 100% correctness of a design cannot be guaranteed. Formal methods, based around applying mathematical expressions and reasoning to prove correctness, have been developed to increase the verification confidence level. This study introduces and demonstrates a methodology for formally verifying safety properties of analogue circuits. In the proposed approach, system equations are automatically extracted from a SPICE netlist by means of energy-conservative bond graph models. Verification based on abstract model checking and constraint solving is then applied on the extracted equation models. The authors methodology avoids an exhaustive and time demanding simulation that is normally encountered during analogue circuit verification. To this end, the authors have used a set of tools to implement the proposed verification flow and applied it on tunnel diode, Chua and Colpitts oscillators as case studies.