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

Intel天價(jià)虧損的幕后黑手

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

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

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

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

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

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

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

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

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

英特爾的奔騰處理器的浮點(diǎn)除法缺陷

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

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

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

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

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

阿米爾·伯努利與艾倫·愛(ài)默生

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

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

傳統(tǒng)的芯片驗(yàn)證有仿真，通俗來(lái)說(shuō)，仿真是“測(cè)試”的概念，比如我寫(xiě)了一些測(cè)試案例，我知道這些案例激勵(lì)芯片以后輸出是怎樣的。但是這種測(cè)試首先要考慮生成激勵(lì)，其次還要考慮生成激勵(lì)的覆蓋率，萬(wàn)一有些場(chǎng)景沒(méi)考慮到的話，這個(gè)測(cè)試就會(huì)有漏洞。

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

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

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

形式化驗(yàn)證

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

幻實(shí)（主播）：芯片公司對(duì)SPEC的定義都十分慎重，但是理論能不能走向?qū)嵺`，都離不開(kāi)驗(yàn)證這個(gè)過(guò)程。

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

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

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

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

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

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

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

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

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

那么問(wèn)題來(lái)了，這個(gè)難點(diǎn)是不是能夠通過(guò)形式化驗(yàn)證或者模擬仿真，對(duì)所在場(chǎng)景覆蓋率做自動(dòng)生成，然后進(jìn)行自動(dòng)檢測(cè)，這就是一個(gè)革命性的研究，實(shí)際上EDA也在向這個(gè)方向發(fā)展。

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

生存法則揭秘：

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

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

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

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

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

形式化驗(yàn)證其實(shí)已經(jīng)過(guò)了這個(gè)階段，我相信國(guó)內(nèi)的公司應(yīng)該不會(huì)再去重復(fù)這一過(guò)程，因?yàn)橼呌诔墒斓纳逃霉ぞ咭呀?jīng)問(wèn)世，他們基本不會(huì)自己再去重新研發(fā)。

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

現(xiàn)在的Cadence和Synopsys他們?cè)缙谝捕际菗碛幸粌蓚€(gè)核心產(chǎn)品站穩(wěn)腳跟，然后按照其公司本身的發(fā)展邏輯向外延展，通過(guò)上下游的不斷并購(gòu)，形成一個(gè)大的生態(tài)。我覺(jué)得這種模式非常好，大公司得到了新的技術(shù)、新的團(tuán)隊(duì)或者新的產(chǎn)品，小公司也有退出甚至上市的機(jī)會(huì)，這是我看到的美國(guó)、歐洲的一些公司的發(fā)展路徑。

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

阿卡思形式化驗(yàn)證特點(diǎn)

（圖源：阿卡思微電子）

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

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

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

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

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

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

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

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

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

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

（圖源：阿卡思微電子）

我剛剛在說(shuō)一個(gè)好的趨勢(shì)，但是真正需要讓國(guó)內(nèi)的芯片公司用你的工具，不可能依靠?jī)r(jià)格便宜而性能一般。因?yàn)樾酒O(shè)計(jì)的流片失敗成本很高，帶來(lái)的后果也很大，對(duì)市場(chǎng)窗口的影響非常大，所以客戶不會(huì)因?yàn)槟闶菄?guó)產(chǎn)就會(huì)網(wǎng)開(kāi)一面。這是EDA的生存法則，我也完全理解。

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

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

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

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

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

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

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

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