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

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

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

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

數(shù)據(jù)通過(guò)SSH通道使用AWS 的秘鑰進(jìn)行加密傳輸，保證數(shù)據(jù)的安全性

可提供高達(dá)128個(gè)虛擬CPU, 1952GiB內(nèi)存的計(jì)算實(shí)例供選擇

可支持上百個(gè)AWS EC2實(shí)例, 根據(jù)所使用的實(shí)例數(shù)目自動(dòng)對(duì)驗(yàn)證任務(wù)分組，利用實(shí)例進(jìn)行并行計(jì)算加速整個(gè)驗(yàn)證過(guò)程，大大縮短芯片數(shù)字邏輯設(shè)計(jì)的驗(yàn)證時(shí)間

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

如何申請(qǐng)AveMC cloud試用版本帳號(hào)： 

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

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

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

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