本期主题：
点击上方小程序即可收听直播音频
英特尔巨额亏损的幕后黑手
石欢（主持人）：本期我们邀请了Akas联合创始人袁军先生来为大家揭秘芯片的秘密。 阿卡西是国内EDA行业的后起之秀，专注于形式化验证方向。 今天很荣幸能够与袁先生进行面对面的交流。 首先请袁老师给我们介绍一下什么是形式化验证！
袁军（嘉宾）：好的，谢谢环狮，大家好，我叫袁军。
Akath是目前国内唯一的商用数字前端验证EDA软件供应商。 我们公司于2018年在成都成立，后来总部迁至上海。 我是上海阿卡西微电子和成都阿卡西微电子的联合创始人。 清华大学毕业后，我去美国留学。 从研究生到工作，我几乎一直在从事形式化验证相关的工作。
我简单介绍一下形式化验证的历史。 严格来说，形式验证可以追溯到远古时代，始于形式逻辑。 我们知道，形式逻辑和实验是现代科学的两大支柱。 实验得出的结论必须有相当严格的逻辑关系和完整性，而不是大家闲聊的“因为如此，所以如此”。 它是形式逻辑的根源。
早在20世纪初，就有一场运动想要将所有数学和物理理论整合到一个形式逻辑系统中，即通过一些简单的原理和逻辑推导规则来推导所有数学和物理原理。 由于涉及逻辑完整性的诸多问题，这场运动最终以失败告终。
20世纪50年代和1960年代，计算机开始发展，软件的复杂性逐渐增加，市场上开始出现软件验证的需求，包括AI。 最早的人工智能不是随机或统计算法，而是逻辑算法。 事实上，早期的形式逻辑与人工智能有着相同的起源。
时间来到了20世纪70年代和80年代，芯片迎来了快速发展。 Fairchild和Intel的芯片设计发展起来后，由于芯片的复杂性越来越高，流片失败的成本很高，芯片开发验证的需求不断上升。 芯片领域形式化验证的一些基本原则可能就是在这个时候出现的。
虽然软件问题也出现过很多，但给我印象最深的还是芯片的问题。 最典型的就是20世纪90年代初，Intel的芯片产品出现了浮点除法问题。 他们没有进行测试，召回该芯片花费了超过 4 亿美元，这在当时是一个天文数字。
事实上，英特尔是业内第一家在芯片设计中使用形式化验证的公司。 在大型EDA公司做形式化验证之前，他们就已经有自己的形式化验证团队了。 他们的正式验证团队使用了他们自己的方法，一旦运行，这个bug很快就被捕获了。
英特尔奔腾处理器中的浮点除法缺陷
损失约4.75亿美元（来源：互联网）
20世纪90年代，出现了新一轮形式化验证的实用化趋势。 首先，以色列科学家阿米尔·伯努利获得了图灵奖*。 他提出了时序逻辑，即传统的Logically相加时态，而这个时序逻辑对于芯片来说尤为重要。 2007年，图灵奖被授予三位科学家，以表彰他们在开发模型检查技术并使之成为广泛应用于硬件和软件行业的非常有效的算法验证技术方面做出的基础性贡献。
图灵奖是计算机协会（ACM）于1966年设立的计算机奖项，旨在奖励对计算机行业做出重要贡献的个人。 图灵奖获奖要求极高，颁奖流程极其严格。 一般来说，每年仅授予一名计算机科学家。 图灵奖是计算机领域的国际最高奖项，被誉为“计算机界的诺贝尔奖”。
因此，形式化验证本身的发展经历了很长一段时间，但它真正应用在芯片上应该是在20世纪90年代后期，在2010年左右变得成熟。当时硅谷各大芯片设计公司几乎都会使用，这就是形式验证的一般历史演变。
回到Akas，我们团队几十年来一直在做形式化验证。 我本人于20世纪90年代在德克萨斯大学奥斯汀分校攻读硕士和博士学位。 德克萨斯大学奥斯汀分校也是形式验证的发源地。 2007年图灵奖获得者之一欧内斯特·艾伦·爱默生（Ernest Allen Emerson）也是我校教授。 也是在那个时候，我系统地接触了形式化验证的理论课程。
阿米尔·伯努利（左）和艾伦·爱默生（右）
环石（主播）：听起来很多大公司都把形式化验证作为不可或缺的环节。 如果没有形式验证会怎样？ 它在整个芯片研发或制造过程中发挥什么价值？
袁军（嘉宾）：首先它所做的事情叫功能验证。 在设计芯片之前有一些 SPEC 要求。 也就是说，芯片做出来之后，是否能够满足当时的设计要求，需要进行形式验证； 另外，一款芯片产品的诞生要从代码层面到物理层面，最后到量产。 中间有很多台阶。 每一步都会在不同的方向进行优化，比如时序优化、功耗优化、面积优化等。我们在优化的时候有时会对设计进行一些改变。 这些改变是否合理需要形式化验证，因此形式化验证在芯片设计到制造的过程中起着非常重要的作用。
传统的芯片验证涉及模拟。 通俗地说，模拟就是“测试”的概念。 例如，如果我编写一些测试用例，我知道这些用例将来的输出会是什么样。 但这种测试首先要考虑产生激励，其次要考虑产生激励的覆盖范围。 如果不考虑某些场景，这个测试就会存在漏洞。
形式化验证则恰恰相反。 我们首先会建立整个芯片的数学逻辑模型，然后在模型上做数学证明，证明我的SPEC是你需要做的，就是在芯片设计上确实是非常严格的。 逻辑模型得到满足。 因为这是一个证明过程，所以不存在覆盖问题。
形式化验证与模拟（来源：互联网）
模拟和形式验证应该是一种互补的关系。 每个人都传统上使用模拟。 形式化验证可能主要用在一些逻辑复杂、难以验证的芯片设计过程中，比如上面提到的Intel浮点。 分部等。 当然，随着形式化验证技术的不断发展，其应用场景将会越来越普遍。
点击图片跳转名人谈话声音合集，快来听听吧！
形式验证
充满想象力的应用空间
施焕（主持人）：芯片公司对SPEC的定义非常谨慎，但理论能否付诸实践取决于验证过程。
我想问一下袁老师，您刚才提到形式化验证和常规模拟是一种互补的关系，但也许我们知道大部分还是基于模拟。 形式化验证的发展空间有多大？ 这个市场是不是有点小？
袁军（嘉宾）：过去10年，形式化验证在成熟的基础上不断延伸其使用场景和规模，性能也得到提升。 我想强调的是，形式化验证不是实验和测试，而是建立一个严格的模型，然后在模型上做一些数学证明。 这绝对是与其他验证不同的方法。
我们对标的Cadence形式化验证产品Cadence Jasper，除了核心部分之外，他们还有近20个针对不同场景的形式化验证应用，而且这些场景还在不断扩展。 因此，形式化并不局限于某种场景。
此外，除了芯片本身的应用领域之外，形式化验证还延伸到了其他方面，比如软件。 事实上，形式化验证首先应用于软件，成熟后又得到反馈。 现在有很多关键软件，比如航天领域的飞行控制，或者汽车的自动控制，还有人工智能软件。 这些本身都是非常强大的软件，但是如果出了问题，就会造成非常严重的后果，哪怕是万分之一。 概率很高，谁也不能保证绝对不会发生意外。 这个时候做这些事情也需要形式化验证和模拟辅助，所以它的技术和市场方面是互补的。
形式化验证的应用（来源：阿卡西微电子）
环时（主持人）：您刚才列举了几个方向。 Akas 的目标赛道是什么？ 会进军汽车方向吗？ 还是仍坚持芯片方向？
袁军（嘉宾）：我们团队的背景主要来自芯片设计公司或者EDA公司。 事实上，就在5-10年前，EDA公司主要专注于芯片设计，但现在EDA有一个大趋势，不再局限于芯片设计或硬件，在信息安全和自主领域涌现出很多机会驾驶。
换句话说，它正在扩展到工业软件领域。 工业软件现在有很多更时髦的名字，比如数字孪生、元宇宙等。
例如，很多智能驾驶测试正在路上进行。 几百公里或几千公里只是一个开始。 智能驾驶的完全训练和成熟可能需要数百亿公里。 目前还没有一家公司能够达到这样的规模。 谷歌智能驾驶将用于街头摄影，但其范围只有约10亿公里。
那么问题来了，这个难度是否可以通过形式化验证或者模拟的方式自动生成，然后自动检测，这是一个革命性的研究。 事实上，EDA也在朝这个方向发展。
回过头来看，对我们来说，首先，阿卡西会深耕芯片领域，这是我们的根据地和发源地。 我们的对手Jasper有十多个APP，我们也会补上。 在此基础上，我们还将向汽车功能验证的工业软件方向发展。
点击图片了解爱心果精英班课程
生存法则揭晓：
国内外EDA公司的发展路径有何差异？
环石（主持人）：我想问一个更有挑战性的问题。 形式验证非常重要。 芯片设计公司或者汽车制造商会安排自己的团队来做这项工作吗？ 此外，竞争对手也在蓬勃发展。 例如，国内多家EDA公司纷纷走上IPO之路。 一些平台宣称未来将提供全平台软件服务。 这两点会对你的想象力产生什么影响吗？ 产品和服务带来了一定的影响。 您对这些事件有何看法？
袁军（嘉宾）：我觉得客户自己做形式化验证，或者类似形式化验证的其他产品，确实是可以的。 不过，我认为几乎所有的EDA细分领域都会经历这样的发展过程，并且形式化验证的这个阶段已经过去了。
我个人早期曾在AMD和摩托罗拉的芯片设计公司工作过。 当时我在公司内部的EDA部门，因为当时这些比较先进的芯片设计公司的一些需求超出了EDA供应商当时可以提供的产品或服务范围。 。
只要有市场、有资金，Intel、IBM、AT&T贝尔实验室、我当时工作的摩托罗拉等公司都有自己的EDA团队。 我们内部开发了大约10年，然后商业EDA工具公司接手了这些工作，因为他们觉得技术和市场已经差不多了。
形式化验证其实已经过了这个阶段。 我相信国内企业不会再重复这个过程，因为成熟的商业工具已经发布了，他们自己基本上不会重新开发。
关于平台的问题，我认为从团队基因来看，形式化验证无论是从市场角度、应用角度、还是技术延伸角度，都有很大的拓展空间。 这符合硅谷很多科技公司的模式——突破从一点开始。
如今的Cadence和Synopsys都是早期凭借一两个核心产品站稳脚跟，然后按照公司自身的发展逻辑向外扩张，通过上下游的不断并购形成了一个大的生态系统。 我认为这个模型非常好。 大公司获得新技术、新团队或新产品，小公司也有机会退出甚至上市。 这是我在美国和欧洲看到的一些公司的发展路径。
我认为美国EDA的黄金时代是20年前，现在是中国EDA的黄金时代。 中国是一个创造奇迹的地方，资金多，市场大，愿意接受新鲜事物。 平台公司从一开始就很难。 我也祝愿中国的一些平台公司尽快取得成功，但从阿卡西的角度来看，我们还是更愿意深化自己的优势。 如果我们要往平台方向发展，那就往形式化验证平台方向发展。 这个平台无论向上还是向下延伸，都有很大的空间。 我们不排除未来会和大平台合作，比如前端数字验证平台公司。 。
Akash形式化验证的特点
（来源：阿卡西微电子）
环时（主播）：我觉得如果一个垂直品牌能够把所有的场景都做好，那就已经是一个足够大的市场了。 另外，你在这个行业呆了这么久，应该有很多客户给你很多积极的反馈。 您回国创业已经四五年了。 你怎么看这件事？ 您在中国创业和之前在硅谷创业的经历有很大区别吗？ 您心中有什么挑战可以与我们分享吗？
袁军（嘉宾）：我回国创业是一个机缘巧合。 我于 2015-2016 年离开 Cadence。 我当时的想法很复杂。 我可以继续在这家公司安逸地工作，但我总觉得我想做点什么。 当时外部形势发生了变化，我们判断美国早期的高科技外包都是软件，那么芯片设计外包也是吗？ 显然中国有这么大的市场，也确实有这个趋势。 我们正抱着这样的想法准备创业。 幸运的是，我们偶然遇到了一位天使投资人，我们非常感动。
因为2017年底国内EDA公司不到10家，所以成都基本上没有正经的芯片设计公司，更不用说EDA公司了。 但我和我们的天使投资人很快就做出了决定，两个月之内资金就到位了，我们很快就落地了成都。
它开始于一种命运。 四年来，我们发现了一些有中国特色的东西。 比如在硅谷，研发基本上就是一个小型的核心团队。 当时我的核心研发团队只有5个人，整个公司有10多人。 在中国，我发现很多时候人越多越好。 这就是市场需求。 有的客户会关心这个，有的雇主也会关心这个。
EDA是低级软件，门槛较高。 我们要做的不仅仅是芯片设计本身软件开发的形式化方法，还有逻辑推理。 我们需要的是跨界人才。 例如，我去美国学习微电子和计算机系统，这些都是以工程为主的专业。 但是要做形式化验证，我想学的是计算机科学，它比较理论化，包括数理逻辑、离散数学等，而且我需要对一个人提出多个领域的要求时，应该说有我国基本上没有现成的人才培养体系。
另外，各种所谓“爱国版”的盗版软件也会对我们造成一定的影响。 我觉得这和国产芯片发展的阶段有关。 国产芯片将持续增长。 随着我们做的芯片产品越来越复杂，所需的EDA工具以及行业对EDA人才的需求自然会增加。 这对我们来说是一个挑战也是一个机遇。 如果我们做好自己的事情，突破这个难点，顺应国内产业升级和芯片自主可控的趋势，应该会看到市场和人才方面的红利。
点击图片了解爱鑫博盛投资更多信息
形式验证的最终形式？
环时（主持人）：我非常同意你提到的这个趋势。 随着产业升级，将爆发的需求将非常具有想象力。 与一些传统的EDA公司相比，有战斗力的团队、没有历史包袱的团队可能更适合终端需求。 你未来的计划是什么？ 您希望阿卡西成为什么样的公司？
袁军（嘉宾）：首先，在形式化验证领域，我们要先做强，再做大。 为了对标世界上最好的产品，我们现在已经扩展到两个主要方向。 一种称为 Model cheking MC，它以 Jasper 为基准，另一种是 EC 等效性验证，它以 Synopsys 的 Formality 为基准。 这两款机型是两家大领先公司的最佳产品。 我们不仅仅局限于国内市场，现在正在考虑在国际上大展拳脚。
芯片设计过程中的形式验证和逻辑等效性检查
（来源：阿卡西微电子）
我只是说一个好的趋势，但是你确实需要让国内的芯片公司使用你的工具。 仅仅依靠便宜的价格和平均的性能是不可能的。 因为芯片设计流片失败的成本很高，后果也很大，对市场窗口的影响也很大，所以客户不会因为你是国产就对你开放。 这就是EDA的生存法则，我完全明白。
所以，要想在国内做强，首先要对标最好的产品。 按理说，如果能在国内实现替代，我们不妨出去尝试一下。 我也来自硅谷，了解那里的一些市场规则和产品发展方向，我们掌握的趋势也相当前沿。 我们清楚地知道自己缺少什么软件开发的形式化方法，需要做什么。
在长远的规划中，我们会向工业软件方向延伸，在汽车功能安全方向打响名堂，这样大家在谈到汽车验证的时候，就能想到Akas，这是非常好的。
史焕（主持人）：非常务实的想法。 非常感谢袁老师在芯片揭秘专栏中分享了这么多关于形式化验证的过去、今天和未来。 将为中国智能制造场景带来独特效益。 这是值得的。 节目结束后，您对外界有什么诉求或者诉求吗？
袁军（嘉宾）：首先感谢Chip Reveal Platform给我提供了这样一个机会来谈形式化验证。 希望观众能够对形式化验证有一些新的认识，对我们公司的产品有一些深入的了解。 阿卡西将继续与大家一起努力，让EDA行业走向成功。
环石（主持人）：我们会持续关注阿卡西，祝愿阿卡西未来在形式化验证的方向上取得大家所期待的成绩。
“不懂数学的工程师不是好工程师。” 许多数学家认为，硬件和软件工程最终都是数学问题。 如果所有的设计和开发都能按照严格的数学方法进行，那么软件就不会出错，硬件也永远正常。 当然，这是数学家的理想。 形式化方法最基本的特征是运用数学概念、方法和工具来解决设计的正确性问题。
形式化验证是形式化方法在数字硬件设计领域的应用。 以智能汽车为代表的新时代应用的软硬件复杂度不断增加，尤其是电动汽车的普及和自动驾驶技术的出现，对硬件产生了很大的影响。 和软件验证提出了新的挑战，也带来了新的市场机遇。
在芯片设计中加入安全机制意味着设计逻辑将变得更加复杂，系统性设计缺陷也可能会增加。 这些缺陷甚至可能改变芯片设计的功耗和性能。 同时需要完整性验证，形式化验证将是一种非常有想象力、非常有效的方法。 让我们期待它在更多场景中闪耀，让我们的制造更加智能！
