袁军|提供形式化验证EDA工具，「阿卡思」助力中国自主创＂芯＂

芯片是人类历史上最宏大也最细微的工程产品。芯片的电路制程一般仅为几纳米，这能够使上亿个晶体管集成在一个指甲大小的芯片上并发挥出强大的算力，但同时，要想实现这一壮举必须依托于完备的上下游产业链，包括材料、设计和制造等环节。
我国和美国之间的政治、经济摩擦使得我国高端芯片领域自主生产能力不足的问题得以暴露，除了已经被大众所熟知的光刻机等生产装备，在芯片设计领域，高性能的EDA工具同样需要奋起直追。而这也是上海阿卡思微电子技术有限公司（以下简称“阿卡思”）所发力的方向。
阿卡思正式成立于2020年5月，其前身成都奥卡思微电科技有限公司在2018年便开始运营。
阿卡思创始人袁军拥有德克萨斯大学奥斯汀分校博士学位，曾先后在AMD、摩托罗拉、Verplex、Jasper、Cadence等公司任形式化验证EDA研发负责人或技术主管，其他核心团队成员也均来自世界知名EDA公司或芯片公司，拥有丰富的研发经验。
国内市场EDA工具的风口相较于芯片的制造浪潮是滞后的，大约在2019年才开始兴起，但对袁军来说，打造国产的高性能EDA工具是一件极其自然并必须要做的事。“我一直认为中国人很适合做EDA工具的开发，中国市场也应该摆脱对国外品牌EDA工具的依赖。”袁军说到。

文章插图
芯片设计概念图
EDA工具是一个很大的概念，具体来说，阿卡思专注在了EDA前端验证工具上。
从芯片的设计流程上来说，验证贯穿始终，无论是前端设计、后端设计还是物理设计，都需要验证工具和验证技术的参与。先进的EDA验证工具和手段可以保证设计结果和原始描述的正确性与一致性，这将直接影响一个半导体产品的性能和产出时间。
此前，我国的芯片设计一直处于中低端水平，对高性能的前端验证工具的需求并不旺盛。但随着世界半导体技术的发展，芯片的制程越来越小，集成度和相应的流片成本也越来越高，这意味着在前端设计环节验证工具越来越重要。同时，随着我国开始向高端半导体产品领域发力，我国市场比以往任何时候都更需要先进的EDA验证工具。
不同于其他EDA工具公司，阿卡思专门针对前端设计环节推出了形式化验证EDA工具——AveMC和逻辑等价性检查EDA工具——AveCEC。形式化验证方法正在越来越多地取代传统仿真验证。
其使用方法是用户根据设计要求提供验证所需的属性和约束，用数学归纳和推理的方法回答这些属性是否正确。如果不正确，验证工具会自动生成可用于仿真的激励链，以便于查错。
形式验证的数学严密性使它成为对安全可靠性要求极高的芯片设计的必备选择，当然也意味着验证工具的性能要十分可靠。

文章插图
形式化验证方法逻辑
阿卡思AveMC形式化验证工具包含了20多种先进的引擎算法，同时可以通过引擎并行，使多引擎验证同一属性。此外，AveMC还能处理最为广义的断言空泛，保障验证的完整性。
袁军告诉创业邦：“形式化验证可以覆盖一些仿真验证无法运营的场景，它更像是一种对芯片设计思路的严谨的逻辑证明，同时也具有极高的可靠性和准确性。”
据了解，某AI视觉公司第二代AI芯片采用阿卡思AveMC验证performance monitor模块，采用signoff流程，最终发现和确认了18个RTL bug。
而AveCEC则是阿卡思推出的一款逻辑等价性检查工具。在现代芯片设计流程中，很多环节都需要设计人员对不同的功能点或电路文件进行优化或修改，因此，保证芯片设计在被修改后仍能保持初始功能不变就显得十分重要。
阿卡思AveCEC运用形式化验证的静态分析方法，能够简单快速地帮助用户确保在每一次电路文件发生改动之后，电路的功能仍然不变。
据介绍，阿卡思AveCEC具有很高的兼容性，其不与任何综合工具绑定，而是独立于其他综合工具运行，也无需其他综合工具提供综合优化描述文件。作为第三方软件，阿卡思AveCEC保持了高度的中立性和客观性。
同时，AveCEC还具备强大的功能完整性和可扩展性，无论是RTL到网表的等价性检查还是网表到网表的等价性检查，都在该工具的功能覆盖范围之内。

文章插图
阿卡思AveMC界面
目前阿卡思已经与国内某芯片大厂完成了深度合作，在高性能计算、人工智能等领域也与多家头部客户建立了业务绑定，同时在各领域的研究所中也做到了产品的落地，并登录了亚马逊云平台和华为云平台。