@phdthesis{dub-19-aa-mixsig-th,
  author = {Dubikhin, Vladimir}
  title = {Synthesis and Verification of Mixed-Signal Systems with Asynchronous Control},
  year = 2019,
  school = {Newcastle University},
  number = {NCL-EEE-MICRO-TR-2020-217},
  pages = {145},
  month = nov,
  note = {Advisor: Alex Yakovlev. No DOI?},
  url = {http://async.org.uk/tech-reports/NCL-EEE-MICRO-TR-2020-217.pdf},
  comment = {Mentions AA only briefly},
  abstract = {Analog/mixed signal (AMS) systems are widely used in electronic devices, such as mobile phones, autonomous sensors, and radio transmitters. The traditional design flows are based on synchronous circuits, which simplify the design process but raise a number of limitations in certain applications. For example, in order to react promptly to the changes in an analog environment the control module needs to have a high clocking frequency. This in return leads to higher power consumption and wasted clock cycles, when no changes occur in the environment. Asynchronous circuits do not have this disadvantage as they react to input events at the rate they occur. However, with design automation being a huge concern asynchronous circuits are not widely used by industry. Another problem related to the AMS system design is the reliance on simulation as the verification method. A simulation trace shows only one possible behavior of the system, as a result simulation based verification largely depends on quantity and diversity of tests. Formal methods, such as the reachability analysis, aim to address this problem. However, a lot of the proposed methodologies are disruptive to the existing design flows and require engineers to manually construct abstract models for their systems. The main goal of this work is to introduce the novel automated workflow, which enables formal verification of AMS systems with asynchronous control that has been optimized with correct timing assumptions extracted from the full-system model. One of the key features of the proposed design flow is the ability to reuse existing simulation traces to generate abstract models, used for system validation. To overcome a number of flaws in the existing model generator a new version, utilizing data clusterization and process mining techniques, is created as a stand-alone framework in Java. The new model generator is designed to construct more general models that produce correct behavior, when used with a different control module}
}