Towards the automated modelling and formal verification of analog designs