Universitätspublikationen
Refine
Year of publication
Document Type
- Article (13724)
- Part of Periodical (3487)
- Doctoral Thesis (3329)
- Contribution to a Periodical (2163)
- Book (2108)
- Working Paper (1888)
- Preprint (1739)
- Review (1064)
- Report (909)
- Conference Proceeding (699)
Language
- English (17475)
- German (14010)
- Portuguese (231)
- Spanish (123)
- Italian (66)
- French (64)
- Multiple languages (64)
- Turkish (12)
- Ukrainian (10)
- slo (7)
Keywords
- Deutschland (132)
- COVID-19 (98)
- inflammation (96)
- Financial Institutions (92)
- ECB (69)
- Capital Markets Union (67)
- SARS-CoV-2 (64)
- Financial Markets (61)
- Adorno (58)
- Banking Regulation (52)
Institute
- Medizin (6677)
- Präsidium (5133)
- Physik (3575)
- Wirtschaftswissenschaften (2298)
- Gesellschaftswissenschaften (2021)
- Biowissenschaften (1767)
- Frankfurt Institute for Advanced Studies (FIAS) (1671)
- Sustainable Architecture for Finance in Europe (SAFE) (1403)
- Biochemie und Chemie (1400)
- Informatik (1393)
Kein gemeinsames Mittagessen im Dasein, kein Kinobesuch in der Pupille – und der letzte Kaffee im Hopplo ist auch schon eine Weile her. Spätestens im März war klar: Das Sommersemester 2020 wird anders. Corona geht herum, und wir bleiben zu Hause. Nachdem der Semesterstart auf den 20. April verschoben wurde, startete die Universität erstmals mit einem reinen Online-Angebot. Doch was bedeutet Studieren in Zeit der Pandemie? Und wie kommen die Studis mit dieser ungewohnten Situation zurecht?
In this dissertation the formal abstraction and verification of analog circuit is examined. An approach is introduced that automatically abstracts a transistor level circuit with full Spice accuracy into a hybrid automaton (HA) in various output languages. The generated behavioral model exhibits a significant simulation speed-up compared to the original netlist, while maintaining an acceptable accuracy, and can be therefore used in various verification and validation routines. On top of that, the generated models can be formally verified against their Spice netlists, making the obtained models correct by construction.
The generated abstract models can be extended to enclose modeling as well as technology dependent parameter variations with little over approximations. As these models enclose the various behaviors of the sampled netlists, the obtained models are of significant importance as they can replace several simulations with just a single reachability analysis or symbolic simulation. Moreover, these models can be as well be used in different verification routines as demonstrated in this dissertation.
As the obtained models are described by HAs with linear behaviors in the locations, the abstract models can be as well compositionally linked, allowing thereby the abstraction of complex analog circuits.
Depending on the specified modeling settings, including for example the number of locations of the HA and the description of the system behavior, the accuracy, speedup, and various additional properties of the HA can be influenced. This is examined in detail in this dissertation. The underlying abstraction process is first covered in detail. Several extensions are then handled including the modeling of the HAs with parameter variations. The obtained models are then verified using various verification methodologies. The accuracy and speed-up of the abstraction methodology is finally evaluated on several transistor level circuits ranging from simple operational amplifiers up to a complex circuits.