Freibothe, M.M.FreibotheDöge, J.J.DögeCoym, T.T.CoymLudwig, S.S.LudwigStraube, B.B.StraubeKock, E.E.Kock2022-03-102022-03-102007https://publica.fraunhofer.de/handle/publica/35771010.1007/978-1-4020-6149-3_3In this work, an approach to the "verification-oriented" modeling of the analog parts' behavior of mixed-signal circuits is presented. Starting from a continuous-time, continuous-valued behavioral representation of an analog part in terms of a differential -algebraic equation system, a discrete-time, discrete-valued behavioral model is derived. This kind of model both captures dynamic aspects of the analog behavior and can be implemented using the synthesizable subset of a hardware description language like VHDL. With the help of the proposed approach, the continuous-time, continuous-valued analog parts' behavioral descriptions can be replaced by digital behavioral models leading to a verification-oriented model of the underlying mixed-signal circuit. The resulting model can be formally verified using established methods and tools from formal digital verification.en621Verification-oriented behavioral modeling of nonlinear analog parts of mixed-signal circuitsconference paper