题目： 形式化验证在IC设计中的应用
主讲人： 刘莉亚 博士 超威半导体高级工程师
时间地点：7月2日周一 上午10:00 院楼106会议室
个人简介： 刘莉亚博士是超威半导体公司多伦多分部的高级工程师，也是PCIe设计团队形式化验证领域的领头人。她的主要研究兴趣包括形式化验证、机器学习、马可夫模型、超大规模集成电路设计验证自动化、微处理器和片上系统的验证等。她曾经发表过多篇国际会议论文和学术期刊论文，是形式化验证核心会议Formal Methods in Computer-Aided Design Conference（FMCAD 2011）、Third NASA Formal Methods Symposium（NFM 2012）和Journal of Computer Science and Technology（JCST 2012）等的审稿人之一。她于2013年在加拿大魁北克省蒙特利尔获得Concordia University电子工程学科博士学位。
摘要：随着现代专用芯片的规模越来越大，验证芯片实现的功能是否符合设计需求将面临着巨大的挑战。仿真技术是基于计算机最常用的传统验证技术。然而，仿真方法往往因为不能穷尽所有可能的情形，导致依赖这种技术验证通过的芯片很难保证其功能的正确性。因此，应用这样的芯片在敏感而安全性要求极高的系统上，会给系统带来潜在的毁灭性危险。另一方面，由于仿真环境复杂以及芯片本身规模巨大，超长的仿真时间也难以满足日趋缩短的产品上市要求，令人难以接受。形式化验证是用数学的方法证明产品（电路或算法）实现的正确性或者不正确性。这种方法能够在一定程度上穷尽所有可能输入，捕捉到仿真方法难以发现的小概率差错以弥补仿真验证方法的不足。现代ＥＤＡ产商提供了自动提取产品属性的形式化验证工具，可以全面地分析产品测试覆盖率以及测试平台的正确性和完整性。作为仿真技术的强大后盾，形式化验证工具充分应用在芯片的设计周期中，将大大提高产品的合格率，缩短设计生产周期、加速产品上市过程。在这次的演讲中，刘莉亚将首先介绍形式化方法的概念；然后讲述应用在芯片设计过程中的形式化验证工具以及应用该方法在芯片设计过程中所能获得的效果；最后，展示形式化验证在现代工业领域中潜在的机遇与面临的挑战。
Title： Formal Verification Applied in IC Design Process
Bio: Dr. Liya Liu is a senior engineer, the leader who employs formal verification on PCIe IP design team in Advanced Micro Device (AMD), Markham, Toronto, Ontario, Canada. Her current research interests are formal verification, machine learning, Markov model, VLSI design verification automation, microprocessor and system-on-chip (SOC) verification. She published various conference and Journal papers and was invited to be the external reviewer of several conferences in formal verification domain, such as, Formal Methods in Computer-Aided Design Conference(FMCAD 2011), Third NASA Formal Methods Symposium(NFM 2012), Journal of Computer Science and Technology(JCST
2012). She received her Ph.D. in the department of Electrical and Computer Engineering at Concordia University, Montreal, Quebec, Canada in 2013.
Abstract:
Nowadays, the increasing size of ASIC has brought about diverse challenges in verifying that the implementation matches with the requirements of products. Traditionally, simulation and emulation are the most commonly used computer-based analysis techniques. However, due to the fact that the complicated ICs have incredible input combinations, simulation and emulation can hardly provide exhaustive scenarios to prove the correctness of product properties. Hence, simulation poses serious threat in ICs applied in safety critical systems. On the other hand, the unbounded running time introduced by complex scenarios and big size of products becomes generally unacceptable comparing to the increasingly shorter time-to-market and high productivity increase requirements. Formal verification is such a methodology that proves the correctness of product implementation compared with its specification using mathematical reasoning. Thus, it is capable to exhaust all corner cases to capture bugs on a reasonable level, as a complementary of simulation and emulation technologies. Modern formal tools provided by various EDA companies facilitate auto-generated properties to formally check product features and supply unreachability analysis for evaluating the quality of ICs. Moreover, these tools offer formal test bench analysis to avoid bug(s) hidden in test environment. Utilizing these rich EDA resources and employing formal verification in IC design process as a complement to simulation, it is feasible to provide high productivity in a shorter period. In this talk, Dr. Liu introduces the concept of formal methods at beginning, then, presents formal tools and their applications in IC design process. The results indicate the benefits of this methodology. Based on this background, Dr. Liu also presents various potential application areas in modern industry as well as the challenges on the road of exploiting formal verification.
