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

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

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

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

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

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

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

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

雖然軟件也出過許多問題，但最讓我印象深刻的是芯片出的問題，其中比較典型的是在上個(gè)世紀(jì)九十年代初，英特爾的芯片產(chǎn)品出了一個(gè)浮點(diǎn)除法的問題，出廠前他們并沒有測試出來，結(jié)果召回芯片花了超過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很快就抓出來了。

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

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

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

圖靈獎(jiǎng)是由美國計(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)域的國際最高獎(jiǎng)項(xiàng)，被譽(yù)為“計(jì)算機(jī)界的諾貝爾獎(jiǎng)”。

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

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

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

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

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

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

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

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

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

形式化驗(yàn)證

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

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

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

袁軍（嘉賓）：在過去的10年，形式化驗(yàn)證在它成熟的基礎(chǔ)上，不斷在延伸其使用場景及使用規(guī)模，其本身性能也都在提高。我想強(qiáng)調(diào)的是，形式化驗(yàn)證不是實(shí)驗(yàn)和測試，而是建立一個(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ì)不同的場景，而且這些場景還不斷在擴(kuò)展。所以，形式化不會(huì)受限于某一個(gè)場景。

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

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

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

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

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

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

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

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

生存法則揭秘：

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

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

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

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

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

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

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

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

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

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

（圖源：阿卡思微電子）

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

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

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

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

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

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

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

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

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

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

（圖源：阿卡思微電子）

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

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

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

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

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

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

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

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

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