{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T11:49:38Z","timestamp":1740138578957,"version":"3.37.3"},"reference-count":19,"publisher":"Walter de Gruyter GmbH","issue":"5-6","funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["286525601"],"award-info":[{"award-number":["286525601"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020,12,16]]},"abstract":"<jats:title>Abstract<\/jats:title>\n               <jats:p>In this paper we present a methodology to automatically generate an accurate behavioral model from an analog circuit description. The current machine learning method is limited to circuits with up to 80 transistors, limiting our approach to small and mid size circuit blocks due to a state explosion problem. However, if complex building blocks such as IOT systems should be modeled, the current approach needs to recoup with feasible simulation and modeling time. To come up with a solution for this problem, we extend the current method by a compositional approach. The approach is illustrated upon an example from the area of autonomous driving. Our method decomposes this large example into smaller building blocks and models each of them automatically. All models are combined into a compositional hybrid automaton of the whole complex system.<\/jats:p>\n               <jats:p>Compared to the original state space, the building blocks operate on smaller and reduced state spaces and hence drastically reduce the complexity. Using a back-transformation on the compositional automaton, all values from the original state space can be reconstructed. Moreover, we perform a formal verification on the generated compositional automaton. Results from a meaningful example are presented and discussed.<\/jats:p>","DOI":"10.1515\/itit-2020-0004","type":"journal-article","created":{"date-parts":[[2020,10,7]],"date-time":"2020-10-07T12:27:52Z","timestamp":1602073672000},"page":"257-270","source":"Crossref","is-referenced-by-count":0,"title":["From transistor level to cyber physical\/hybrid systems: Formal verification using automatic compositional abstraction"],"prefix":"10.1515","volume":"62","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9174-5598","authenticated-orcid":false,"given":"Ahmad","family":"Tarraf","sequence":"first","affiliation":[{"name":"University Frankfurt , Computer Science Institute , Frankfurt\/M. , Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lars","family":"Hedrich","sequence":"additional","affiliation":[{"name":"University Frankfurt , Computer Science Institute , Frankfurt\/M. , Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"374","published-online":{"date-parts":[[2020,10,7]]},"reference":[{"key":"2023033120444117105_j_itit-2020-0004_ref_001_w2aab3b7d368b1b6b1ab2ab1Aa","doi-asserted-by":"crossref","unstructured":"M.\u2009H. Zaki, S. Tahar, G. Bois, Formal verification of analog and mixed signal designs: A survey, Microelectronics Journal 39 (12) (2008) 1395\u20131404.","DOI":"10.1016\/j.mejo.2008.05.013"},{"key":"2023033120444117105_j_itit-2020-0004_ref_002_w2aab3b7d368b1b6b1ab2ab2Aa","doi-asserted-by":"crossref","unstructured":"L. Yin, Y. Deng, P. Li, Verifying dynamic properties of nonlinear mixed-signal circuits via efficient SMT-based techniques, in: Proceedings of the International Conference on Computer-Aided Design, ICCAD\u201912, ACM, New York, NY, USA, 2012, pp.\u2009436\u2013442. doi:10.1145\/2429384.2429474.","DOI":"10.1145\/2429384.2429474"},{"key":"2023033120444117105_j_itit-2020-0004_ref_003_w2aab3b7d368b1b6b1ab2ab3Aa","doi-asserted-by":"crossref","unstructured":"L. Yin, Y. Deng, P. Li, Simulation-Assisted Formal Verification of Nonlinear Mixed-Signal Circuits with Bayesian Inference Guidance, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 32 (7) (2013) 977\u2013990. doi:10.1109\/TCAD.2013.2245941.","DOI":"10.1109\/TCAD.2013.2245941"},{"key":"2023033120444117105_j_itit-2020-0004_ref_004_w2aab3b7d368b1b6b1ab2ab4Aa","doi-asserted-by":"crossref","unstructured":"M. Barnasconi, M. Dietrich, K. Einwich, T. V\u00f6rtler, J.\u2009P. Chaput, M.\u2009M. Lou\u00ebrat, F. P\u00eacheux, Z. Wang, P. Cuenot, I. Neumann, T. Nguyen, R. Lucas, E. Vaumorin, UVM-SystemC-AMS Framework for System-Level Verification and Validation of Automotive Use Cases, IEEE Design Test 32 (6) (2015) 76\u201386. doi:10.1109\/MDAT.2015.2427260.","DOI":"10.1109\/MDAT.2015.2427260"},{"key":"2023033120444117105_j_itit-2020-0004_ref_005_w2aab3b7d368b1b6b1ab2ab5Aa","doi-asserted-by":"crossref","unstructured":"A. Tarraf, L. Hedrich, Behavioral modeling of transistor-level circuits using automatic abstraction to hybrid automata, in: Design Automation and Test in Europe (DATE), Florence, 2019.","DOI":"10.23919\/DATE.2019.8715184"},{"key":"2023033120444117105_j_itit-2020-0004_ref_006_w2aab3b7d368b1b6b1ab2ab6Aa","unstructured":"A. Tarraf, L. Hedrich, Automatic abstraction of analog circuits to hybrid automata, in: 16. GMM\/ITG-Fachtagung-ANALOG, 2018."},{"key":"2023033120444117105_j_itit-2020-0004_ref_007_w2aab3b7d368b1b6b1ab2ab7Aa","doi-asserted-by":"crossref","unstructured":"N. Kochdumper, A. Tarraf, M. Rechmal, M. Olbrich, L. Hedrich, M. Althoff, Establishing reachset conformance for the formal analysis of analog circuits, in: ASP-DAC, 2020.","DOI":"10.1109\/ASP-DAC47756.2020.9045120"},{"key":"2023033120444117105_j_itit-2020-0004_ref_008_w2aab3b7d368b1b6b1ab2ab8Aa","unstructured":"AMS HitKit \u2013 Process Design Kit (PDK) for Circuit Simulation, Austria Microsystems."},{"key":"2023033120444117105_j_itit-2020-0004_ref_009_w2aab3b7d368b1b6b1ab2ab9Aa","doi-asserted-by":"crossref","unstructured":"W. Hartong, R. Klausen, L. Hedrich, Formal Verification for Nonlinear Analog Systems: Approaches to Model and Equivalence Checking, Advanced Formal Verification, R. Drechsler, ed., Kluwer Academic Publishers, Boston (2004), pp.\u2009205\u2013245.","DOI":"10.1007\/1-4020-2530-0_6"},{"key":"2023033120444117105_j_itit-2020-0004_ref_010_w2aab3b7d368b1b6b1ab2ac10Aa","doi-asserted-by":"crossref","unstructured":"L. Hedrich, E. Barke, A formal approach to nonlinear analog circuit verification, in: Proc. IEEE\/ACM International Conference on Computer-Aided Design ICCAD-95. Digest of Technical Papers, 5, pp.\u2009123\u2013127. doi:10.1109\/ICCAD.1995.480002.","DOI":"10.1109\/ICCAD.1995.480002"},{"key":"2023033120444117105_j_itit-2020-0004_ref_011_w2aab3b7d368b1b6b1ab2ac11Aa","doi-asserted-by":"crossref","unstructured":"S. Steinhorst, L. Hedrich, Advanced methods for equivalence checking of analog circuits with strong nonlinearities, Formal Methods in System Design 36 (2) (2010) 131\u2013147.","DOI":"10.1007\/s10703-009-0086-9"},{"key":"2023033120444117105_j_itit-2020-0004_ref_012_w2aab3b7d368b1b6b1ab2ac12Aa","doi-asserted-by":"crossref","unstructured":"J. Phillips, J. Afonso, A. Oliveira, L.\u2009M. Silveira, Analog macromodeling using kernel methods, in: Proceedings of the 2003 IEEE\/ACM International Conference on Computer-Aided Design, IEEE Computer Society, 2003, p.\u2009446.","DOI":"10.1109\/ICCAD.2003.159722"},{"key":"2023033120444117105_j_itit-2020-0004_ref_013_w2aab3b7d368b1b6b1ab2ac13Aa","doi-asserted-by":"crossref","unstructured":"S. Steinhorst, L. Hedrich, Trajectory-directed discrete state space modeling for formal verification of nonlinear analog circuits, in: Proceedings of the International Conference on Computer-Aided Design, ACM, 2012, pp.\u2009202\u2013209.","DOI":"10.1145\/2429384.2429423"},{"key":"2023033120444117105_j_itit-2020-0004_ref_014_w2aab3b7d368b1b6b1ab2ac14Aa","unstructured":"A. Davis, An overview of algorithms in Gnucap, in: University\/Government\/Industry Microelectronics Symp., 2003, pp.\u2009360\u2013361."},{"key":"2023033120444117105_j_itit-2020-0004_ref_015_w2aab3b7d368b1b6b1ab2ac15Aa","unstructured":"A. Tarraf, L. Hedrich, Automatic abstraction of transistor level circuits to hybrid automata, in: Frontiers in Analog Circuit Design (FAC), 2018."},{"key":"2023033120444117105_j_itit-2020-0004_ref_016_w2aab3b7d368b1b6b1ab2ac16Aa","doi-asserted-by":"crossref","unstructured":"A. Tarraf, L. Hedrich, Automatic modeling of transistor level circuits by hybrid systems with parameter variable matrices, in: International Conference on Synthesis, Modeling, Analysis and Simulation Methods and Applications to Circuit Design (SMACD), Lausanne, Switzerland, 2019.","DOI":"10.1109\/SMACD.2019.8795271"},{"key":"2023033120444117105_j_itit-2020-0004_ref_017_w2aab3b7d368b1b6b1ab2ac17Aa","unstructured":"M. Althoff, An introduction to CORA 2015, in: Proc. of the Workshop on Applied Verification for Continuous and Hybrid Systems."},{"key":"2023033120444117105_j_itit-2020-0004_ref_018_w2aab3b7d368b1b6b1ab2ac18Aa","unstructured":"Cora 2018 Manual, https:\/\/tumcps.github.io\/CORA\/data\/Cora2018Manual.pdf (2019)."},{"key":"2023033120444117105_j_itit-2020-0004_ref_019_w2aab3b7d368b1b6b1ab2ac19Aa","doi-asserted-by":"crossref","unstructured":"D. Schramm, M. Hiller, R. Bardini, Vehicle Dynamics, 2nd Edition, Springer, Berlin, 2018. doi:10.1007\/978-3-662-54483-9.","DOI":"10.1007\/978-3-662-54483-9"}],"container-title":["it - Information Technology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.degruyter.com\/view\/journals\/itit\/62\/5-6\/article-p257.xml","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/www.degruyter.com\/document\/doi\/10.1515\/itit-2020-0004\/xml","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/www.degruyter.com\/document\/doi\/10.1515\/itit-2020-0004\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,1]],"date-time":"2023-04-01T10:09:28Z","timestamp":1680343768000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.degruyter.com\/document\/doi\/10.1515\/itit-2020-0004\/html"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,10,7]]},"references-count":19,"journal-issue":{"issue":"5-6","published-online":{"date-parts":[[2020,10,7]]},"published-print":{"date-parts":[[2020,12,16]]}},"alternative-id":["10.1515\/itit-2020-0004"],"URL":"https:\/\/doi.org\/10.1515\/itit-2020-0004","relation":{},"ISSN":["2196-7032","1611-2776"],"issn-type":[{"type":"electronic","value":"2196-7032"},{"type":"print","value":"1611-2776"}],"subject":[],"published":{"date-parts":[[2020,10,7]]}}}