SHF: Medium: Booleanized Verification of Analog/Mixed Signal Systems

当今几乎所有的电子设备，特别是智能手机、平板电脑等便携式设备，不仅包含数十亿个被称为晶体管的微小开关，而且还包含许多关键的模拟/混合信号(AMS)电路。设计AMS电路通常比设计数字电路困难得多；它们需要受过专门训练的设计师供不应求，设计时间要长得多，而且往往需要多次设计迭代。此外，当嵌入到带有数字电路的芯片中时，由于不可预见的数字-模拟交互而导致的故障很常见，很难准确定位。这项研究旨在解决使AMS设计和调试更容易、更可靠和更快的问题。这项研究的成功应该会有力地推动电子设计技术，最终以更低的成本制造出更复杂、更有用的小工具。此外，本研究还将有助于培养一批研究生和本科生，从而为电子设计自动化行业培养未来的劳动力。在此背景下开展的外展活动也将有助于吸引高中生到STEM地区。该项目背后的关键技术理念是将AMS部件准确地建模为数字部件；然后使用更容易使用和更快的数字技术进行调试和设计。该项目将在这一范例中追求两个大的方向：1)开发更好和更准确的布尔化技术，以将AMS电路和系统近似为数字电路和系统；以及2)开发更好的技术，以确定布尔化/数字模型是否正确工作。

Almost all electronic equipment today, particularly portable devices such as smartphones, tablets etc., contain not only billions of tiny switches called transistors, but also a number of critical analog/mixed-signal (AMS) circuits. Designing AMS circuits is usually far more difficult than designing digital circuits; they require specially trained designers in short supply, much longer design times, and often require several design iterations. Furthermore, when embedded in a chip with digital circuits, malfunctions stemming from unforeseen digital-analog interactions are common and difficult to pinpoint. This research aims to address the problem of making AMS design and debug easier, more reliable, and faster. Success of this research should provide a powerful boost to electronic design technology, eventually resulting in more complex and useful gadgets at lower cost. Moreover, this research will help train a number of graduate and undergraduate students, thus helping to develop the future workforce for electronic design automation industry. Outreach activities to be undertaken in this context will also help attract high-school students to STEM areas.The key technical idea behind this project is to model AMS components accurately as digital ones; and then to use digital techniques, which are much easier to use and faster, for debugging and design. The project will pursue two broad directions within this paradigm: 1) develop better and more accurate Booleanization techniques for approximating AMS circuits and systems as digital ones; and 2) develop better techniques for determining if the Booleanized/digital models work correctly or not.