In this paper we demonstrate a potential extension of formal verification methodology in order to deal with analog and mixed-signal circuits. In particular, we focus on verifying time-domain properties. The time-dependent behavior of an analog circuit can be described by a system of differential algebraic equations. To model and analyse such circuits under all possible input signals and all values of parameters, we apply various techniques developed in the context of hybrid (discrete-continuous) control systems. First, we extend dense-time reachability analysis and apply it in the case of a biquad lowpass filter. Then, an important mixed-signal circuit, the Delta-Sigma modulator, is modelised with a discrete-time hybrid system and its stability is analysed using techniques based on mixed integer linear programming.