成都奥卡思发布国内首款的芯片数字形式化验证EDA云计算工具--AveMC Cloud

中国成都，2020年4月20日，成都奥卡思微电科技(ARCASTECH)公司正式发布国内首款基于亚马逊AWS云平台的形式化验证工具AveMC Cloud，标志着本公司EDA工具正式迈入云计算时代，用户可以远程完成复杂芯片RTL设计的验证及调试工作，也为本公司EDA软件走向国际市场打下了坚实的基础。

形式化方法广泛应用于芯片设计、发动机核心控制软件、汽车自动驾驶等复杂关键系统领域，它利用数学定理来完备性证明设计的实现方案是否反映所描述的功能。与传统的仿真相比，形式化验证无需提供激励，验证更加完备充分。

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

采用Client-Server模式，Client端完成RTL设计和system verilog assertion建模并把模型发送至AWS云端，AWS云端Server端完成对assertion的证明并把结果返回Client端，在Client端完成Debug工作，因此设计数据只存在本地，保证了数据的安全性;

数据通过SSH通道使用AWS 的秘钥进行加密传输，保证数据的安全性

可提供高达128个虚拟CPU, 1952GiB内存的计算实例供选择

可支持上百个AWS EC2实例, 根据所使用的实例数目自动对验证任务分组，利用实例进行并行计算加速整个验证过程，大大缩短芯片数字逻辑设计的验证时间

工具可实现按小时计费，而不是传统的按天数计费的模式，可以有效减少客户成本开销

如何申请AveMC cloud试用版本帐号： 

 请使用所在公司邮箱发送试用版本申请邮件到wangrui@arcas-da.com,说明软件需要运行的操作系统(支持ubuntu或centos系统)，并注明工作单位及软件使用目的。

“成都奥卡思为华为杯第二届中国研究生创芯大赛参赛提供了AVEMC形式化验证软件，现在他们又发布了AveMC Cloud云计算产品，我们对它非常感兴趣，这可以帮助我们杭州集成电路产业化基地更好的服务于众多芯片设计企业，获得更快的客户响应，同时也帮助芯片设计企业节省了EDA软件和IT建设成本，EDA上云可以使得客户支持服务更通畅快捷。”--丁勇(杭州国家集成电路设计产业化基地有限公司副总经理，浙江大学信息与电子工程学院教授，博导) 

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

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