2020年4月20日，成都奧卡思微電科技(ARCASTECH)迎來(lái)公司成立兩周年，并正式發(fā)布國(guó)內(nèi)首款基于亞馬遜AWS云平臺(tái)的形式化驗(yàn)證工具AveMC Cloud，標(biāo)志著本公司EDA工具正式邁入云計(jì)算時(shí)代，用戶(hù)可以遠(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ī)核心控制軟件、汽車(chē)自動(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年開(kāi)始處于試運(yùn)行狀態(tài)，曾在2018年DVCON會(huì)議和2019年中國(guó)ICCAD會(huì)議上展示，今年正式上線(xiàn)運(yùn)行?；谠破脚_(tái)的AveMC Cloud軟件是芯片數(shù)字前端驗(yàn)證EDA軟件，利用模型檢驗(yàn)算法證明RTL設(shè)計(jì)和用戶(hù)的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í)例可供用戶(hù)選擇，用戶(hù)無(wú)需進(jìn)行本地?cái)U(kuò)容，直接根據(jù)需要選用對(duì)應(yīng)的計(jì)算實(shí)例在云上進(jìn)行計(jì)算，能夠有效降低開(kāi)發(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)的模式，可以有效減少客戶(hù)成本開(kāi)銷(xiāo)

如何申請(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è)，獲得更快的客戶(hù)響應(yīng)，同時(shí)也幫助芯片設(shè)計(jì)企業(yè)節(jié)省了EDA軟件和IT建設(shè)成本，EDA上云可以使得客戶(hù)支持服務(wù)更通暢快捷?！?-丁勇(杭州國(guó)家集成電路設(shè)計(jì)產(chǎn)業(yè)化基地有限公司副總經(jīng)理，浙江大學(xué)信息與電子工程學(xué)院教授，博導(dǎo))

“成都奧卡思為我們實(shí)現(xiàn)形式化驗(yàn)證APP的定制服務(wù)，幫助我們提高客戶(hù)委托設(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)始人)

“肇觀電子專(zhuān)注于AI機(jī)器視覺(jué)芯片的研發(fā)，在我們最新一代芯片中使用了奧卡思公司的形式化驗(yàn)證EDA軟件AVEMC，在總線(xiàn)模塊發(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)

成都奧卡思微電科技有限公司是由海歸博士創(chuàng)立，2018年3月成立于成都高新區(qū)。公司核心人員來(lái)自于Cadence，Synopsys，Xilinx等國(guó)際知名EDA公司和芯片設(shè)計(jì)公司，具有平均超過(guò)15年的全球EDA行業(yè)經(jīng)驗(yàn)，是多項(xiàng)業(yè)內(nèi)知名軟件工具的主要研發(fā)者。公司主要業(yè)務(wù)為集成電路設(shè)計(jì)自動(dòng)化系統(tǒng)(EDA)的研發(fā)和咨詢(xún)，目前是國(guó)內(nèi)唯一推出商業(yè)化驗(yàn)證EDA軟件的公司。