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

形式化方法廣泛應用于芯片設計、發(fā)動機核心控制軟件、汽車自動駕駛等復雜關鍵系統(tǒng)領域，它利用數學定理來完備性證明設計的實現(xiàn)方案是否反映所描述的功能。與傳統(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實例, 根據所使用的實例數目自動對驗證任務分組，利用實例進行并行計算加速整個驗證過程，大大縮短芯片數字邏輯設計的驗證時間

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

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

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

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

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

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