提供形式化驗證EDA工具，阿卡思助力中國自主創芯

芯片是人類歷史上最宏大也最細微的工程產品。芯片的電路制程一般僅為幾納米,這能夠使上億個晶體管集成在一個指甲大小的芯片上并發揮出強大的算力,但同時,要想實現這一壯舉必須依托于完備的上下游產業鏈,包括材料、設計和制造等環節。

我國和美國之間的政治、經濟摩擦使得我國高端芯片領域自主生產能力不足的問題得以暴露,除了已經被大眾所熟知的光刻機等生產裝備,在芯片設計領域,高性能的EDA工具同樣需要奮起直追。而這也是上海阿卡思微電子技術有限公司(以下簡稱“阿卡思”)所發力的方向。

阿卡思正式成立于2020年5月,其前身成都奧卡思微電科技有限公司在2018年便開始運營。

阿卡思創始人袁軍擁有德克薩斯大學奧斯汀分校博士學位,曾先后在AMD、摩托羅拉、Verplex、Jasper、Cadence等公司任形式化驗證EDA研發負責人或技術主管,其他核心團隊成員也均來自世界知名EDA公司或芯片公司,擁有豐富的研發經驗。

國內市場EDA工具的風口相較于芯片的制造浪潮是滯后的,大約在2019年才開始興起,但對袁軍來說,打造國產的高性能EDA工具是一件極其自然并必須要做的事。“我一直認為中國人很適合做EDA工具的開發,中國市場也應該擺脫對國外品牌EDA工具的依賴。”袁軍說到。

EDA工具是一個很大的概念,具體來說,阿卡思專注在了EDA前端驗證工具上。

從芯片的設計流程上來說,驗證貫穿始終,無論是前端設計、后端設計還是物理設計,都需要驗證工具和驗證技術的參與。先進的EDA驗證工具和手段可以保證設計結果和原始描述的正確性與一致性,這將直接影響一個半導體產品的性能和產出時間。

此前,我國的芯片設計一直處于中低端水平,對高性能的前端驗證工具的需求并不旺盛。但隨著世界半導體技術的發展,芯片的制程越來越小,集成度和相應的流片成本也越來越高,這意味著在前端設計環節驗證工具越來越重要。同時,隨著我國開始向高端半導體產品領域發力,我國市場比以往任何時候都更需要先進的EDA驗證工具。

不同于其他EDA工具公司,阿卡思專門針對前端設計環節推出了形式化驗證EDA工具——AveMC和邏輯等價性檢查EDA工具——AveCEC。形式化驗證方法正在越來越多地取代傳統仿真驗證。

其使用方法是用戶根據設計要求提供驗證所需的屬性和約束,用數學歸納和推理的方法回答這些屬性是否正確。如果不正確,驗證工具會自動生成可用于仿真的激勵鏈,以便于查錯。

形式驗證的數學嚴密性使它成為對安全可靠性要求極高的芯片設計的必備選擇,當然也意味著驗證工具的性能要十分可靠。

形式化驗證方法邏輯

阿卡思AveMC形式化驗證工具包含了20多種先進的引擎算法,同時可以通過引擎并行,使多引擎驗證同一屬性。此外,AveMC還能處理最為廣義的斷言空泛,保障驗證的完整性。

袁軍告訴創業邦:“形式化驗證可以覆蓋一些仿真驗證無法運營的場景,它更像是一種對芯片設計思路的嚴謹的邏輯證明,同時也具有極高的可靠性和準確性。”

據了解,某AI視覺公司第二代AI芯片采用阿卡思AveMC驗證performance monitor模塊,采用signoff流程,最終發現和確認了18個RTL bug。

而AveCEC則是阿卡思推出的一款邏輯等價性檢查工具。在現代芯片設計流程中,很多環節都需要設計人員對不同的功能點或電路文件進行優化或修改,因此,保證芯片設計在被修改后仍能保持初始功能不變就顯得十分重要。

阿卡思AveCEC運用形式化驗證的靜態分析方法,能夠簡單快速地幫助用戶確保在每一次電路文件發生改動之后,電路的功能仍然不變。

據介紹,阿卡思AveCEC具有很高的兼容性,其不與任何綜合工具綁定,而是獨立于其他綜合工具運行,也無需其他綜合工具提供綜合優化描述文件。作為第三方軟件,阿卡思AveCEC保持了高度的中立性和客觀性。

同時,AveCEC還具備強大的功能完整性和可擴展性,無論是RTL到網表的等價性檢查還是網表到網表的等價性檢查,都在該工具的功能覆蓋范圍之內。

阿卡思AveMC界面

目前阿卡思已經與國內某芯片大廠完成了深度合作,在高性能計算、人工智能等領域也與多家頭部客戶建立了業務綁定,同時在各領域的研究所中也做到了產品的落地,并登錄了亞馬遜云平臺和華為云平臺。

即使近年來國產EDA工具領域玩家日益增多,但阿卡思仍是前端驗證工具環節中為數不多的實現了工具商業化并完成市場部署的公司。

袁軍表示:“EDA工具是一個很容易被驗證性能的產品,用兩個工具去驗證同一個設計文件,哪個能在更短的時間里得到更準確的結果,那它的性能就是優秀的,就是會被用戶認可的。阿卡思就是國內形式化驗證工具的代表。”

阿卡思產品的收付費方式為國際上慣用的年費授權,目前全部采用直銷模式進行市場推廣,預計今年全年的營業額將達到千萬元級別。

人員方面,阿卡思目前擁有員工30余人,幾乎全部為技術研發人員。

袁軍告訴創業邦:“由于國內EDA市場剛剛興起,很多環節還不完善,在人才方面也面臨著緊缺的問題,從人才培養到市場機制都需要全面發展,當然阿卡思也在開足馬力擴充自己的隊伍,以保證我們產品的更新和技術的迭代。”

融資方面,7月2日阿卡思宣布完成了數千萬元Pre-A輪融資,本輪融資由上海合見工業軟件集團有限公司領投,哈勃科技投資有限公司、上海科技創業投資有限公司和上海張江燧峰創新股權投資基金合伙企業(有限合伙)跟投。據了解,本輪融資將用于擴充人員和開拓EDA新產品。