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.