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.