Intel天價虧損的幕后黑手

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

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

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

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

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

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

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

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

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

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

使其損失了約4.75億美元（圖源：網絡）

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

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

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

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

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

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

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

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

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

形式驗證與仿真（圖源：網絡）

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

形式化驗證

充滿想象力的應用空間

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

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

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

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

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

形式驗證的應用（圖源：阿卡思微電子）

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

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

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

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

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

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

生存法則揭秘：

國內外EDA公司的發展路徑有何差異？

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

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

我本人早期是在AMD和摩托羅拉的芯片設計公司工作，當時我就在公司內部的EDA部門，因為當時這些比較先進的芯片設計公司的一些需求超出了那時候EDA供應商能夠提供的產品或者服務范圍。

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

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

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

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

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

阿卡思形式化驗證特點

（圖源：阿卡思微電子）

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

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

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

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

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

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

形式化驗證的最終形態？

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

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

芯片設計流程中形式化驗證和邏輯等價檢查環節

（圖源：阿卡思微電子）

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

所以我們要想在國內做強，首先就是要對標最好的產品，順理成章，我們如果可以在國內實現替代，其實不妨也走出去試一試。我也是從硅谷過來，我知道那邊的一些市場規律和產品發展方向，我們把握的趨勢還是比較前沿的。我們清楚的知道我們欠缺什么，要做什么。

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

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

袁軍（嘉賓）：首先感謝芯片揭秘平臺提供這么一個機會讓我來聊一聊形式化驗證，希望聽眾能夠對形式化驗證有一些新的認識，對我們公司的產品有一些深入的了解。阿卡思將持續努力，與大家一起把EDA行業做好。

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

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

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

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