案例研究: 成都奥卡思微电科技有限公司

“通过AWS云计算的雄厚技术实力和Arcas在形式化验证EDA工具的深耕和专业性为半导体行业提供具有真正创新力的解决方案。”

王锐 博士 成都奥卡思微电科技 市场与销售总监

成都奥卡思微电科技有限公司（以下简称“Arcas”）是由两位硅谷博士创立，2018年4月成立于成都高新区。公司核心人员来自于Cadence，Synopsys，Xilinx等国际知名EDA公司和芯片设计公司，具有平均超过15年的全球EDA行业经验，是多项业内知名软件工具的主研或管理者。公司主要业务为集成电路设计自动化系统(EDA)的研发和咨询。公司立足于最新的EDA技术，结合本土用户需求，竭诚服务中国芯片自主设计产业。

之前采用自建服务器方式，存在CPU计算资源，内存不够用的问题。特别是对于一些复杂的形式化验证本地的IT资源无法需求，需要排队等待，严重影响项目交付时间和进度，希望软件有更弹性的收费模式。由于Amazon Elastic Compute Cloud (Amazon EC2) 可以按需启动并按照实际使用时间计费，客户使用AveMC形式化验证软件的费用也可以实现按需计费，与传统的使用许可授权按年计费模式有很大优势。

Arcas 产品设计之初就和AWS进行结合，提供了云端运算的能力，并且取得很好的效果。AWS合作伙伴网络（APN）是一个全球的合作伙伴计划，加入APN在技术层面和AWS有更好的耦合。Arcas也是立足本土拓展全球市场，在APN体系中可以有效触达和服务更广的客户。在技术、市场活动和商机上面可以通过APN和AWS加深合作，共同推进云在半导体行业的使用和落地，也使形式化验证工具可以更加高效的服务最终用户。在安全，合规，数据保护上AWS有独到的技术优势，并且在半导体有很多的成功案例非常广泛可选的服务，简便易用的Console环境，特别是Amazon EC2计算集群的类型丰富，这对形式化验证的密集计算有很大的价值。
在引入AWS之后，帮助公司实现了下面的目标：
1. 大大提高形式化验证效率，缩短验证时间。因为形式化验证是计算密集型，所以主要时间在运算上，AWS云上计算资源大大缩短了计算时间，使得原本需要1天才能完成的验证工作可以在一个小时内做完。
2. 能让芯片设计者远程办公，增加设计弹性。用户可以远程完成复杂芯片RTL设计的验证及调试工作。
3. 减少公司IT资源的投入，运维工作大大减少。
4. 提高形式化验证的速度和效率，形成具有强烈的差异性工具特色来竞争市场。
5. 利用AWS的云上各类弹性资源，在开发软件中可以随时启用各类EC2计算集群，而无须单独购买和配置各类服务器，来评估软件性能和功能，节省了开发和调试时间。
6. 开拓国际市场。

Arcas 基于 AWS 建设的 AveMC Cloud软件是芯片数字前端验证EDA软件，利用模型检验算法证明RTL设计和用户的SVA（SystemVerilog Assertion）断言属性是否等价，从而验证芯片的功能的正确性。同时AveMC Cloud还具有特有的断言可视化功能和支持多系统平台（X86、ARM和MIPS）的特点。针对复杂的设计会消耗大量CPU及内存资源，对本地计算机的要求较高的特点，AveMC Cloud可以利用Amazon EC2针对不同的需求提供了大量的计算实例可供用户选择，用户无需进行本地扩容，直接根据需要选用对应的计算实例在云上进行计算，能够有效降低开发成本。平台从2018年开始处于试运行状态，曾在2018年DVCON会议和2019年中国ICCAD会议上展示，今年正式上线运行，目前已经有多个客户在试用和使用中。

基于AWS云平台的AveMC Cloud特点如下：
1. 采用Client-Server模式，Client端完成RTL设计和SVA建模并把模型发送至AWS云端，AWS云端Server端完成对assertion的证明并把结果返回Client端，在Client端完成Debug工作，因此设计数据只存在本地，保证了数据的安全性。
2. 数据通过SSH通道使用AWS 的秘钥进行加密传输，保证数据的安全性。
3. 可提供高达128个虚拟CPU, 1952GiB内存的计算实例供选择。
4. 可支持上百个Amazon EC2实例, 根据所使用的实例数目自动对验证任务分组，利用实例进行并行计算加速整个验证过程，大大缩短芯片数字逻辑设计的验证时间。
5. 工具可实现按小时计费，而不是传统的按天数计费的模式，可以有效减少客户成本开销。

在产品和解决方案的实际应用方面，Arcas为华为杯第二届中国研究生创芯大赛参赛提供了AveMC形式化验证软件，现在又发布了AveMC Cloud云计算产品，丁勇（杭州国家集成电路设计产业化基地有限公司副总经理，浙江大学信息与电子工程学院教授，博导）表示可以帮助杭州集成电路产业化基地更好的服务于众多芯片设计企业，获得更快的客户响应，同时也帮助芯片设计企业节省了EDA软件和IT建设成本，EDA上云可以使得客户支持服务更通畅快捷。

“Arcas为我们实现形式化验证APP的定制服务，帮助我们提高客户委托设计服务的质量，AveMC Cloud云计算平台灵活的license授权模式可以降低我们的EDA成本，同时也会大大缩短我们验证的时间，我们项目模块的500多个断言证明在AveMC Cloud上可以得到几十倍的提升，而且断言属性越多，加速效果越好。”芯荣微电子创始人胡永华谈到，“我们期待成都奥卡思可以推出更多基于云平台的形式化验证APP，帮助我们更快更好的完成项目。”

“肇观电子专注于AI机器视觉芯片的研发，在我们最新一代芯片中使用了Arcas的形式化验证EDA软件AveMC，在总线模块发现了18个设计BUG，这降低了我们产品流片的风险，提高了芯片的质量，我们对他们基于云计算的AveMC Cloud EDA云很感兴趣，云平台可以帮助我们节省IT成本，加快项目的验证收敛。” 上海肇观电子科技有限公司CTO周骥博士谈到。

展望未来，Arcas将继续优化当前产品，评估AWS Batch, AWS ParallelCluster等HPC集群调度服务。计划进一步将公司其他一些软件部署到AWS云上，以及探索提供SaaS化EDA工具。