成都奧卡思發(fā)布國內(nèi)首款的芯片數(shù)字形式化驗(yàn)證EDA云計(jì)算工具--AveMC Cloud
中國成都,2020年4月20日,成都奧卡思微電科技(ARCASTECH)公司正式發(fā)布國內(nèi)首款基于亞馬遜AWS云平臺的形式化驗(yàn)證工具AveMC Cloud,標(biāo)志著本公司EDA工具正式邁入云計(jì)算時代,用戶可以遠(yuǎn)程完成復(fù)雜芯片RTL設(shè)計(jì)的驗(yàn)證及調(diào)試工作,也為本公司EDA軟件走向國際市場打下了堅(jiān)實(shí)的基礎(chǔ)。
形式化方法廣泛應(yīng)用于芯片設(shè)計(jì)、發(fā)動機(jī)核心控制軟件、汽車自動駕駛等復(fù)雜關(guān)鍵系統(tǒng)領(lǐng)域,它利用數(shù)學(xué)定理來完備性證明設(shè)計(jì)的實(shí)現(xiàn)方案是否反映所描述的功能。與傳統(tǒng)的仿真相比,形式化驗(yàn)證無需提供激勵,驗(yàn)證更加完備充分。
成都奧卡思微電的AveMCCloud亞馬遜云平臺從2018年開始處于試運(yùn)行狀態(tài),曾在2018年DVCON會議和2019年中國ICCAD會議上展示,今年正式上線運(yùn)行?;谠破脚_的AveMC Cloud軟件是芯片數(shù)字前端驗(yàn)證EDA軟件,利用模型檢驗(yàn)算法證明RTL設(shè)計(jì)和用戶的SVA(systemverilog assertion)斷言屬性是否等價,從而驗(yàn)證芯片的功能的正確性。同時AveMC Cloud還具有特有的斷言可視化功能和支持多系統(tǒng)平臺(X86、ARM和MIPS)的特點(diǎn)。針對復(fù)雜的設(shè)計(jì)會消耗大量CPU及內(nèi)存資源,對本地計(jì)算機(jī)的要求較高的特點(diǎn),AveMC Cloud可以利用AWS EC2針對不同的需求提供了大量的計(jì)算實(shí)例可供用戶選擇,用戶無需進(jìn)行本地?cái)U(kuò)容,直接根據(jù)需要選用對應(yīng)的計(jì)算實(shí)例在云上進(jìn)行計(jì)算,能夠有效降低開發(fā)成本。 基于AWS云平臺的AveMC Cloud特點(diǎn)如下:
采用Client-Server模式,Client端完成RTL設(shè)計(jì)和system verilog assertion建模并把模型發(fā)送至AWS云端,AWS云端Server端完成對assertion的證明并把結(jié)果返回Client端,在Client端完成Debug工作,因此設(shè)計(jì)數(shù)據(jù)只存在本地,保證了數(shù)據(jù)的安全性;
數(shù)據(jù)通過SSH通道使用AWS 的秘鑰進(jìn)行加密傳輸,保證數(shù)據(jù)的安全性
可提供高達(dá)128個虛擬CPU, 1952GiB內(nèi)存的計(jì)算實(shí)例供選擇
可支持上百個AWS EC2實(shí)例, 根據(jù)所使用的實(shí)例數(shù)目自動對驗(yàn)證任務(wù)分組,利用實(shí)例進(jìn)行并行計(jì)算加速整個驗(yàn)證過程,大大縮短芯片數(shù)字邏輯設(shè)計(jì)的驗(yàn)證時間
工具可實(shí)現(xiàn)按小時計(jì)費(fèi),而不是傳統(tǒng)的按天數(shù)計(jì)費(fèi)的模式,可以有效減少客戶成本開銷
如何申請AveMC cloud試用版本帳號:
請使用所在公司郵箱發(fā)送試用版本申請郵件到wangrui@arcas-da.com,說明軟件需要運(yùn)行的操作系統(tǒng)(支持ubuntu或centos系統(tǒng)),并注明工作單位及軟件使用目的。
“成都奧卡思為華為杯第二屆中國研究生創(chuàng)芯大賽參賽提供了AVEMC形式化驗(yàn)證軟件,現(xiàn)在他們又發(fā)布了AveMC Cloud云計(jì)算產(chǎn)品,我們對它非常感興趣,這可以幫助我們杭州集成電路產(chǎn)業(yè)化基地更好的服務(wù)于眾多芯片設(shè)計(jì)企業(yè),獲得更快的客戶響應(yīng),同時也幫助芯片設(shè)計(jì)企業(yè)節(jié)省了EDA軟件和IT建設(shè)成本,EDA上云可以使得客戶支持服務(wù)更通暢快捷?!?-丁勇(杭州國家集成電路設(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ì)算平臺靈活的license授權(quán)模式可以降低我們的EDA成本,同時也會大大縮短我們驗(yàn)證的時間,我們項(xiàng)目模塊的500多個斷言證明在AveMC AWS cloud上可以得到幾十倍的提升,而且斷言屬性越多,加速效果越好,我們期待成都奧卡思可以推出更多基于云平臺的形式化驗(yàn)證APP,幫助我們更快更好的完成項(xiàng)目。” --- 胡永華(合肥芯榮微電子有限公司創(chuàng)始人)
“肇觀電子專注于AI機(jī)器視覺芯片的研發(fā),在我們最新一代芯片中使用了奧卡思公司的形式化驗(yàn)證EDA軟件AVEMC,在總線模塊發(fā)現(xiàn)了18個設(shè)計(jì)BUG,這降低了我們產(chǎn)品流片的風(fēng)險(xiǎn),提高了芯片的質(zhì)量,我們對他們基于云計(jì)算的AveMC CloudEDA云很感興趣,云平臺可以幫助我們節(jié)省IT成本,加快項(xiàng)目的驗(yàn)證收斂” ----周驥博士(上海肇觀電子科技有限公司CTO)