中國成都，2020年4月20日，成都奧卡思微電科技(ARCASTECH)公司正式發(fā)布國內首款基于亞馬遜AWS云平臺的形式化驗證工具AveMC Cloud，標志著本公司EDA工具正式邁入云計算時代，用戶可以遠程完成復雜芯片RTL設計的驗證及調試工作，也為本公司EDA軟件走向國際市場打下了堅實的基礎。

形式化方法廣泛應用于芯片設計、發(fā)動機核心控制軟件、汽車自動駕駛等復雜關鍵系統(tǒng)領域，它利用數學定理來完備性證明設計的實現方案是否反映所描述的功能。與傳統(tǒng)的仿真相比，形式化驗證無需提供激勵，驗證更加完備充分。

成都奧卡思微電的AveMCCloud亞馬遜云平臺從2018年開始處于試運行狀態(tài)，曾在2018年DVCON會議和2019年中國ICCAD會議上展示，今年正式上線運行?；谠破脚_的AveMC Cloud軟件是芯片數字前端驗證EDA軟件，利用模型檢驗算法證明RTL設計和用戶的SVA(systemverilog assertion)斷言屬性是否等價，從而驗證芯片的功能的正確性。同時AveMC Cloud還具有特有的斷言可視化功能和支持多系統(tǒng)平臺(X86、ARM和MIPS)的特點。針對復雜的設計會消耗大量CPU及內存資源，對本地計算機的要求較高的特點，AveMC Cloud可以利用AWS EC2針對不同的需求提供了大量的計算實例可供用戶選擇，用戶無需進行本地擴容，直接根據需要選用對應的計算實例在云上進行計算，能夠有效降低開發(fā)成本。 基于AWS云平臺的AveMC Cloud特點如下：

采用Client-Server模式，Client端完成RTL設計和system verilog assertion建模并把模型發(fā)送至AWS云端，AWS云端Server端完成對assertion的證明并把結果返回Client端，在Client端完成Debug工作，因此設計數據只存在本地，保證了數據的安全性;

數據通過SSH通道使用AWS 的秘鑰進行加密傳輸，保證數據的安全性

可提供高達128個虛擬CPU, 1952GiB內存的計算實例供選擇

可支持上百個AWS EC2實例, 根據所使用的實例數目自動對驗證任務分組，利用實例進行并行計算加速整個驗證過程，大大縮短芯片數字邏輯設計的驗證時間

工具可實現按小時計費，而不是傳統(tǒng)的按天數計費的模式，可以有效減少客戶成本開銷

如何申請AveMC cloud試用版本帳號： 

 請使用所在公司郵箱發(fā)送試用版本申請郵件到wangrui@arcas-da.com,說明軟件需要運行的操作系統(tǒng)(支持ubuntu或centos系統(tǒng))，并注明工作單位及軟件使用目的。

“成都奧卡思為華為杯第二屆中國研究生創(chuàng)芯大賽參賽提供了AVEMC形式化驗證軟件，現在他們又發(fā)布了AveMC Cloud云計算產品，我們對它非常感興趣，這可以幫助我們杭州集成電路產業(yè)化基地更好的服務于眾多芯片設計企業(yè)，獲得更快的客戶響應，同時也幫助芯片設計企業(yè)節(jié)省了EDA軟件和IT建設成本，EDA上云可以使得客戶支持服務更通暢快捷?！?-丁勇(杭州國家集成電路設計產業(yè)化基地有限公司副總經理，浙江大學信息與電子工程學院教授，博導) 

 “成都奧卡思為我們實現形式化驗證APP的定制服務，幫助我們提高客戶委托設計服務的質量，AveMC Cloud云計算平臺靈活的license授權模式可以降低我們的EDA成本，同時也會大大縮短我們驗證的時間，我們項目模塊的500多個斷言證明在AveMC AWS cloud上可以得到幾十倍的提升，而且斷言屬性越多，加速效果越好，我們期待成都奧卡思可以推出更多基于云平臺的形式化驗證APP，幫助我們更快更好的完成項目?！? --- 胡永華(合肥芯榮微電子有限公司創(chuàng)始人) 

 “肇觀電子專注于AI機器視覺芯片的研發(fā)，在我們最新一代芯片中使用了奧卡思公司的形式化驗證EDA軟件AVEMC，在總線模塊發(fā)現了18個設計BUG，這降低了我們產品流片的風險，提高了芯片的質量，我們對他們基于云計算的AveMC CloudEDA云很感興趣，云平臺可以幫助我們節(jié)省IT成本，加快項目的驗證收斂” ----周驥博士(上海肇觀電子科技有限公司CTO)