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