EDA領(lǐng)域中的國貨之光！聽阿卡思談半導(dǎo)體形式化驗證

Intel天價虧損的幕后黑手

幻實（主播）：本期節(jié)目我們邀請到了阿卡思的聯(lián)合創(chuàng)始人袁軍先生做客芯片揭秘。阿卡思是國內(nèi)EDA行業(yè)的后起之秀，聚焦的是形式化驗證方向，十分榮幸今天能夠和袁總面對面交流。先請袁總給我們講一講什么是形式化驗證吧！

袁軍（嘉賓）：好的，謝謝幻實，大家好，我叫袁軍。

阿卡思是目前國內(nèi)唯一的商用數(shù)字前端驗證EDA國產(chǎn)軟件供應(yīng)商。我們公司于2018年在成都落地，后來將總部遷到上海，我是上海阿卡思微電子以及成都奧卡思微電子的聯(lián)合創(chuàng)始人。在清華本科畢業(yè)后，我去了美國留學(xué)，從研究生到參加工作幾乎都在從事形式化驗證相關(guān)的工作。

我簡單介紹一下形式化驗證的歷史。嚴(yán)格來說，形式化驗證可以追溯到古代，從形式邏輯開始。我們知道形式邏輯與實驗是現(xiàn)代科學(xué)的兩大支柱，從實驗中提出的結(jié)論，必然要有一個相當(dāng)嚴(yán)密的邏輯關(guān)系和完整性，而不是大家聊天所說的“因為這個，所以那個”，這是形式邏輯的根源。

早在20世紀(jì)初有這么一個運(yùn)動，大家想把所有數(shù)學(xué)、物理的理論全部在形式化邏輯的系統(tǒng)里搭起來，即通過一些簡單的原理和邏輯推導(dǎo)規(guī)則，把所有的數(shù)學(xué)、物理原理推導(dǎo)出來，由于這其中涉及了許多邏輯完整性的問題，這個運(yùn)動最終以失敗告終。

到了上個世紀(jì)五六十年代，計算機(jī)開始發(fā)展，軟件的復(fù)雜度逐步提高，市面上開始出現(xiàn)軟件的驗證需求，其中也包括AI。最早期的人工智能并不是一種隨機(jī)或者統(tǒng)計的算法，它是一種邏輯算法，實際上形式邏輯的早期和AI也是同源的。

時間來到上個世紀(jì)七八十年代，芯片迎來了高速發(fā)展，在仙童、英特爾的芯片設(shè)計發(fā)展起來以后，得益于芯片日漸提高的復(fù)雜度及其流片失敗的高昂成本，芯片的驗證需求水漲船高。形式化驗證在芯片領(lǐng)域的一些創(chuàng)始性原理，大概就出現(xiàn)在這個時候。

雖然軟件也出過許多問題，但最讓我印象深刻的是芯片出的問題，其中比較典型的是在上個世紀(jì)九十年代初，英特爾的芯片產(chǎn)品出了一個浮點除法的問題，出廠前他們并沒有測試出來，結(jié)果召回芯片花了超過4億美元，在當(dāng)時這是一個天文數(shù)字。

其實英特爾在業(yè)界是比較早把形式化驗證用在芯片設(shè)計中的公司，在大型EDA公司做形式化驗證之前，他們就已經(jīng)有了自己的形式化驗證團(tuán)隊，他們的形式化驗證團(tuán)隊用自己的方法一跑，這個bug很快就抓出來了。

英特爾的奔騰處理器的浮點除法缺陷

使其損失了約4.75億美元（圖源：網(wǎng)絡(luò)）

在上個世紀(jì)90年代的時候，出現(xiàn)了新一輪的形式化驗證實用化趨勢，首先是以色列科學(xué)家阿米爾·伯努利獲得了圖靈獎*，他提出了時態(tài)邏輯，即在傳統(tǒng)的邏輯上加上時態(tài)，而這種時態(tài)邏輯對芯片而言尤為重要。2007年，圖靈獎授予了三位科學(xué)家，以表彰他們開發(fā)模型檢測技術(shù)，以及使之成為廣泛應(yīng)用在硬件和軟件工業(yè)中非常有效的算法驗證技術(shù)所做的奠基性貢獻(xiàn)。

圖靈獎是由美國計算機(jī)協(xié)會（ACM）于1966年設(shè)立的計算機(jī)獎項，旨在獎勵對計算機(jī)事業(yè)作出重要貢獻(xiàn)的個人 。圖靈獎對獲獎條件要求極高，評獎程序極嚴(yán)，一般每年僅授予一名計算機(jī)科學(xué)家。圖靈獎是計算機(jī)領(lǐng)域的國際最高獎項，被譽(yù)為“計算機(jī)界的諾貝爾獎”。

所以，形式化驗證本身發(fā)展歷時很長，但其真正開始應(yīng)用于芯片上應(yīng)該是在上個世紀(jì)90年代末，趨于成熟大約在2010年左右，那時候在硅谷幾乎所有大的芯片設(shè)計公司都會用，這是形式化驗證大體的歷史沿革。

說回我們阿卡思，我們的團(tuán)隊做形式化驗證有幾十年的積累，我本人從90年代在University of Texas at Austin攻讀碩士和博士學(xué)位，University of Texas at Austin 也是形式化驗證的一個發(fā)源地，2007年的圖靈獎得主之一艾倫·愛默生（Ernest Allen Emerson），也是我們學(xué)校的教授。我也是在那個時候系統(tǒng)性接觸到了形式化驗證的理論課程。

阿米爾·伯努利與艾倫·愛默生

幻實（主播）：聽起來，很多大公司都把形式化驗證作為一個不可缺少的環(huán)節(jié)來做。如果沒有形式化驗證會怎么樣？在整個芯片的開發(fā)或者制造的過程中，它到底起著什么樣的價值？

袁軍（嘉賓）：首先它做的事情叫功能驗證，設(shè)計芯片之前都會有一些SPEC要求，就是說芯片做出來以后，是否能夠滿足當(dāng)時設(shè)計的要求，這就需要形式化驗證；另外，一顆芯片的誕生從代碼級一層一層走到物理級，最后到量產(chǎn)，中間包含很多步驟，每一步都會做不同方向的優(yōu)化，比如時序優(yōu)化，功耗優(yōu)化，面積優(yōu)化等等，我們在優(yōu)化的時候有時會對設(shè)計做一些改動，這些改動是否合理也需要形式化驗證，所以形式化驗證在芯片從設(shè)計到制造的過程中有著十分重要的地位。

傳統(tǒng)的芯片驗證有仿真，通俗來說，仿真是“測試”的概念，比如我寫了一些測試案例，我知道這些案例激勵芯片以后輸出是怎樣的。但是這種測試首先要考慮生成激勵，其次還要考慮生成激勵的覆蓋率，萬一有些場景沒考慮到的話，這個測試就會有漏洞。

形式化驗證卻恰恰相反，我們會首先對整個芯片建一個數(shù)理邏輯的模型，然后在模型上做一個數(shù)學(xué)證明，證明我的SPEC就是你需要做的事情，即確實被芯片設(shè)計中建立的非常嚴(yán)格的邏輯模型滿足了。因為做的是一個證明過程，所以就不存在覆蓋率的問題了。

形式驗證與仿真（圖源：網(wǎng)絡(luò)）

仿真和形式化驗證應(yīng)該是一個互補(bǔ)的關(guān)系，大家傳統(tǒng)都在用仿真，形式化驗證可能主要是用在設(shè)計一些邏輯比較復(fù)雜、比較難驗的芯片過程中，比如前面提到的Intel的浮點除法這類。當(dāng)然隨著形式化驗證的技術(shù)不斷的發(fā)展，它的應(yīng)用場景會越來越多。

形式化驗證

充滿想象力的應(yīng)用空間

幻實（主播）：芯片公司對SPEC的定義都十分慎重，但是理論能不能走向?qū)嵺`，都離不開驗證這個過程。

我想請教一下袁總，您剛剛提到形式化驗證和常規(guī)的模擬仿真之間是一個互補(bǔ)的關(guān)系，但是可能我們了解到大部分還是以仿真為主，形式化驗證的發(fā)展空間到底有多大？這個市場會不會體量有點小？

袁軍（嘉賓）：在過去的10年，形式化驗證在它成熟的基礎(chǔ)上，不斷在延伸其使用場景及使用規(guī)模，其本身性能也都在提高。我想強(qiáng)調(diào)的是，形式化驗證不是實驗和測試，而是建立一個嚴(yán)格的模型，然后對這個模型做一些數(shù)學(xué)方面的證明，與其他驗證絕對是不一樣的方法學(xué)。

我們所對標(biāo)的Cadence形式化驗證產(chǎn)品Cadence Jasper，除了核心部分，他們還有將近20款的形式化驗證應(yīng)用分別針對不同的場景，而且這些場景還不斷在擴(kuò)展。所以，形式化不會受限于某一個場景。

另外，形式化驗證除了芯片本身應(yīng)用領(lǐng)域之外，它也做了一些其他方面的延伸，比如軟件。其實形式化驗證最早就應(yīng)用于軟件，發(fā)展成熟以后，它又反哺回去?，F(xiàn)在有很多關(guān)鍵軟件，比如說航天航空這些飛行控制，或者汽車的自動控制，人工智能軟件，這些本身都是非常強(qiáng)大的軟件，但是它出問題就會造成非常嚴(yán)重的后果，哪怕萬分之一的概率，也沒人可以保證意外絕對不會發(fā)生。這時候也需要形式化驗證和仿真輔助來做這些事情，所以說它的技術(shù)和市場兩個方面是互補(bǔ)的。

形式驗證的應(yīng)用（圖源：阿卡思微電子）

幻實（主播）：您剛剛例舉了好幾個方向，阿卡思瞄準(zhǔn)的是什么賽道，會不會進(jìn)軍汽車方向？還是依舊堅守在芯片方向？

袁軍（嘉賓）：我們團(tuán)隊的背景主要都是芯片設(shè)計公司或者EDA公司，其實就在5-10年前，EDA公司主要針對的還都是芯片設(shè)計，但現(xiàn)在EDA開始出現(xiàn)一個大趨勢，就是不再僅限于芯片設(shè)計或者硬件，信息安全、自動駕駛方面都浮現(xiàn)出很多機(jī)會。

換句話說，它在往工業(yè)軟件方面拓展，工業(yè)軟件現(xiàn)在衍生出很多比較時髦的叫法，比如說數(shù)字孿生、元宇宙等等。

舉個例子，很多智能駕駛在做路測，幾百公里幾千公里只是剛剛開始，想要把智能駕駛完全訓(xùn)練成熟，可能要上百億公里，現(xiàn)在沒有一家公司能做到這樣的規(guī)模，谷歌街拍會用到智能駕駛，不過它也就在10億公里左右的范圍。

那么問題來了，這個難點是不是能夠通過形式化驗證或者模擬仿真，對所在場景覆蓋率做自動生成，然后進(jìn)行自動檢測，這就是一個革命性的研究，實際上EDA也在向這個方向發(fā)展。

回過頭來，對我們而言，首先阿卡思會深耕芯片領(lǐng)域，這是我們的根據(jù)地和發(fā)源地。我們的對手Jasper有十多個APP，我們也會補(bǔ)齊。在這個基礎(chǔ)上，我們也會向汽車功能驗證的工業(yè)軟件方向發(fā)展。

生存法則揭秘：

國內(nèi)外EDA公司的發(fā)展路徑有何差異？

幻實（主播）：我想問一個比較有挑戰(zhàn)性的問題。形式化驗證如此重要，芯片設(shè)計公司或者車廠會不會自己安排團(tuán)隊去做這塊工作？另外，競爭對手的蓬勃發(fā)展，比如我們國內(nèi)已經(jīng)有好幾家EDA公司陸陸續(xù)續(xù)走上了IPO的道路，一些平臺主張自己未來要做全平臺的軟件服務(wù)，這兩點會不會對您構(gòu)想的產(chǎn)品和服務(wù)帶來一些沖擊，您怎么看待這些事件？

袁軍（嘉賓）：客戶自己去做形式化驗證，或者其他類似于形式化驗證的產(chǎn)品，我認(rèn)為確實可能。不過我覺得，EDA的細(xì)分領(lǐng)域幾乎都會經(jīng)歷這么一段發(fā)展過程，而形式化驗證的這個階段已經(jīng)過了。

我本人早期是在AMD和摩托羅拉的芯片設(shè)計公司工作，當(dāng)時我就在公司內(nèi)部的EDA部門，因為當(dāng)時這些比較先進(jìn)的芯片設(shè)計公司的一些需求超出了那時候EDA供應(yīng)商能夠提供的產(chǎn)品或者服務(wù)范圍。

在有市場和資金的前提下，像Intel、IBM、AT&T貝爾實驗室、包括我當(dāng)時所在的摩托羅拉，他們都有自己的EDA團(tuán)隊。我們內(nèi)部大概發(fā)展10年左右，商用EDA工具公司才接收這些工作，因為他們覺得技術(shù)差不多了，市場也差不多了。

形式化驗證其實已經(jīng)過了這個階段，我相信國內(nèi)的公司應(yīng)該不會再去重復(fù)這一過程，因為趨于成熟的商用工具已經(jīng)問世，他們基本不會自己再去重新研發(fā)。

關(guān)于平臺的問題，我覺得就團(tuán)隊基因來講，形式化驗證有很多延展空間，無論是從市場角度、應(yīng)用角度還是技術(shù)延展角度。這一符合很多在硅谷的科技公司的規(guī)律——從一個點產(chǎn)生突破。

現(xiàn)在的Cadence和Synopsys他們早期也都是擁有一兩個核心產(chǎn)品站穩(wěn)腳跟，然后按照其公司本身的發(fā)展邏輯向外延展，通過上下游的不斷并購，形成一個大的生態(tài)。我覺得這種模式非常好，大公司得到了新的技術(shù)、新的團(tuán)隊或者新的產(chǎn)品，小公司也有退出甚至上市的機(jī)會，這是我看到的美國、歐洲的一些公司的發(fā)展路徑。

我認(rèn)為美國的EDA黃金時代是20年前，現(xiàn)在是中國EDA的黃金時代，中國是一個出奇跡的地方，資金多，市場大，愿意接受新鮮事物。一上來就做平臺公司很難，我也祝愿一些中國的平臺公司能夠早日成功，但從阿卡思角度出發(fā)，我們還是更傾向于深耕我們的強(qiáng)點。如果要往平臺方向發(fā)展，我們會向形式化驗證平臺方向發(fā)展，這個平臺無論往上還是往下延展，空間都很大，也不排除我們以后會與大的平臺，比如前端數(shù)字化驗證平臺公司合作。

阿卡思形式化驗證特點

（圖源：阿卡思微電子）

幻實（主播）：我覺得能夠把一個垂類品牌的所有場景做好，就已經(jīng)是一個足夠大的市場了。何況這個行業(yè)您做了這么久，應(yīng)該也已經(jīng)有很多客戶給了您很多正反饋。您回國創(chuàng)業(yè)至今四五年時間，有什么樣的感受？在中國創(chuàng)業(yè)和你以前在硅谷的區(qū)別大不大，有沒有什么印象中的挑戰(zhàn)可以與我們分享？

袁軍（嘉賓）：回國創(chuàng)業(yè)也是機(jī)緣巧合，2015-2016年我離開了Cadence，當(dāng)時的想法也很復(fù)雜，我可以舒適的在這家公司繼續(xù)工作，但是總覺得自己想要做一些事情，加上當(dāng)時外部形勢變化，我們判斷，像美國早期的高科技外包都是軟件，那么芯片設(shè)計是不是有外包？顯然中國有這么大的市場，也確實有這個趨勢，我們就抱著這么一個想法準(zhǔn)備創(chuàng)業(yè)。幸運(yùn)的是，我們正好碰到一位天使投資人，我們很感動。

因為2017年底國內(nèi)EDA公司不到10家，在成都連正兒八經(jīng)的芯片設(shè)計公司基本都沒有，更不用提EDA公司了。但是我和我們天使投資人很快做出了決定，兩個月之內(nèi)資金就到位了，我們也很快在成都落地。

開始是一個緣分，這4年走過來，我們發(fā)覺一些中國特色的事情。比如說在硅谷，研發(fā)基本上就是一個小的核心的團(tuán)隊，當(dāng)時我的核心研發(fā)團(tuán)隊就5個人，整個公司10多個人。而在國內(nèi)我發(fā)現(xiàn)很多情況下是人數(shù)越多越好，這是市場需求，有些客戶會比較在意這一點，一些資方也會在意。

EDA是門檻很高的底層軟件，我們要做的方向不僅是芯片設(shè)計本身，還有邏輯推理，我們需要的是跨界的人才。比如說我本人到美國學(xué)的是微電子和計算機(jī)系統(tǒng)，這些都是偏工程的專業(yè)，但是做形式化驗證我要去學(xué)計算機(jī)科學(xué)，更偏理論，包括數(shù)理邏輯、離散數(shù)學(xué)等等，需要把多領(lǐng)域的要求加在一個人身上，應(yīng)該說國內(nèi)基本沒有現(xiàn)成的人才培養(yǎng)體系。

另外，各式各樣所謂“愛國版”的盜版軟件，也會對我們有些影響。我覺得這與國內(nèi)芯片發(fā)展的階段有關(guān)聯(lián)，國內(nèi)的芯片會持續(xù)往上走，隨著大家做的芯片產(chǎn)品越來越復(fù)雜，那么所需的EDA工具、產(chǎn)業(yè)對EDA人才的需求自然水漲船高。對我們而言是一個挑戰(zhàn)，也是一個機(jī)會。如果我們把自己這塊做好了，突破了這個難關(guān)，跟隨國內(nèi)的產(chǎn)業(yè)升級以及芯片的自主可控趨勢，我們在市場和人才方面應(yīng)該都會看到一個紅利。

形式化驗證的最終形態(tài)？

幻實（主播）：我非常認(rèn)同您所說的趨勢，隨著產(chǎn)業(yè)升級，迸發(fā)出的需求會很有想象力。和一些傳統(tǒng) EDA公司相比，有戰(zhàn)斗力的團(tuán)隊，沒有歷史包袱的團(tuán)隊，可能更匹配終端需求。您對未來有什么樣的規(guī)劃？您想把阿卡思做成一個什么樣的企業(yè)？

袁軍（嘉賓）：首先，在形式化驗證領(lǐng)域先做強(qiáng)再做大。對標(biāo)國際上最好的產(chǎn)品，我們現(xiàn)在延伸了兩大方向，一個是叫Model cheking MC,對標(biāo)的是Jasper，另外一塊是EC等價性驗證，對標(biāo)的是Synopsys的Formality，這兩款是兩大龍頭企業(yè)最好的產(chǎn)品。我們也不僅限于國內(nèi)的市場，現(xiàn)在已經(jīng)考慮在國際上大展身手。

芯片設(shè)計流程中形式化驗證和邏輯等價檢查環(huán)節(jié)

（圖源：阿卡思微電子）

我剛剛在說一個好的趨勢，但是真正需要讓國內(nèi)的芯片公司用你的工具，不可能依靠價格便宜而性能一般。因為芯片設(shè)計的流片失敗成本很高，帶來的后果也很大，對市場窗口的影響非常大，所以客戶不會因為你是國產(chǎn)就會網(wǎng)開一面。這是EDA的生存法則，我也完全理解。

所以我們要想在國內(nèi)做強(qiáng)，首先就是要對標(biāo)最好的產(chǎn)品，順理成章，我們?nèi)绻梢栽趪鴥?nèi)實現(xiàn)替代，其實不妨也走出去試一試。我也是從硅谷過來，我知道那邊的一些市場規(guī)律和產(chǎn)品發(fā)展方向，我們把握的趨勢還是比較前沿的。我們清楚的知道我們欠缺什么，要做什么。

再往長遠(yuǎn)打算，往工業(yè)軟件方向延伸，在汽車功能安全這個方向做出名堂，讓大家說到汽車驗證，就能想到阿卡思，這就非常好。

幻實（主播）：非常務(wù)實的一個想法，非常感謝袁總在芯片揭秘欄目中與跟大家分享那么多形式化驗證的過往、今天以及未來，它將在中國的智能制造場景下帶來的屬于它的價值。節(jié)目最后，您有沒有什么對外發(fā)表的呼吁或者號召？

袁軍（嘉賓）：首先感謝芯片揭秘平臺提供這么一個機(jī)會讓我來聊一聊形式化驗證，希望聽眾能夠?qū)π问交炞C有一些新的認(rèn)識，對我們公司的產(chǎn)品有一些深入的了解。阿卡思將持續(xù)努力，與大家一起把EDA行業(yè)做好。

幻實（主播）：我們將持續(xù)關(guān)注阿卡思，也祝福阿卡思未來在形式化驗證方向都能取得你們所預(yù)想的成就。

“一個不懂?dāng)?shù)學(xué)的工程師不是一個好工程師”。很多數(shù)學(xué)家們認(rèn)為，不論硬件還是軟件工程，歸根結(jié)底是數(shù)學(xué)問題。如果所有的設(shè)計開發(fā)都能夠按照嚴(yán)格的數(shù)學(xué)方法進(jìn)行，那么軟件將不會出錯，硬件會永遠(yuǎn)正常。當(dāng)然，這是數(shù)學(xué)家的理想。形式化方法最基本的特點是利用數(shù)學(xué)的概念、方法和工具來解決設(shè)計的正確性問題。

形式化驗證是形式化方法在數(shù)字硬件設(shè)計領(lǐng)域中的應(yīng)用，以智能汽車為代表的新時代應(yīng)用中軟件和硬件的復(fù)雜性不斷提高，尤其是電動汽車的普及和自動駕駛技術(shù)的出現(xiàn)，對硬件及軟件的驗證都提出了新的挑戰(zhàn)，同時也是新的市場機(jī)遇。

在芯片設(shè)計中增加安全機(jī)制意味著設(shè)計邏輯更趨復(fù)雜，系統(tǒng)性的設(shè)計缺陷也可能會增加，這些缺陷甚至可能改變芯片設(shè)計的功耗和性能，同時需要做完備性驗證，形式驗證將是一個極具想象力、十分有效的方法。讓我們期待它在更多的場景下大放光彩，讓我們的制造更加智能！