@inproceedings{rec-kor-gun-olb-20-aa-reach,
  author = {Rechmal-Lesse, Malgorzata and Koroa, Gerald Alexander and Gunawan Adhisantoso, Yeremia and Olbrich, Markus},
  title = {Automatically Generated Nonlinear Analog Circuit Models Enclosing Variations with Intervals and Affine Forms for Reachability Analysis}, 
  booktitle = {2020 23rd International Symposium on Design and Diagnostics of Electronic Circuits   Systems (DDECS)}, 
  year = 2020,
  volume = {},
  number = {},
  pages = {1-4},
  keywords = {},
  doi = {10.1109/DDECS50862.2020.9095655},
  ISSN = {2473-2117},
  month = apr,
  comment = {Static analysis of analog circuits and reachability analysis},
  abstract = {In contrast to the formal verification of digital circuits, analog formal verification requires appropriate tolerances of the device parameters. Enclosing these tolerances in set-valued models leads to unwanted overapproximation. In this paper, we present an automated modeling approach, which is applicable to nonlinear analog and mixed-signal circuits. We describe the behavioral circuit models as well as the device parameter variations and modeling errors by symbolic equations. We substitute these symbols with intervals and affine forms, respectively. In each case we provide semi-symbolic hybrid automata models. Then, we insert numerical values in these models for reachability analysis. The results of both reachability analyses are used to reduce the overapproximation.}
}