專家在座：半導(dǎo)體工程與 Axiomise 首席執(zhí)行官 Ashish Darbari 坐下來討論形式驗(yàn)證工具和方法的進(jìn)步;張瑾，Cadence 驗(yàn)證組產(chǎn)品管理組總監(jiān);新思科技研發(fā)執(zhí)行董事 Sean Safarpour;以及西門子 EDA 數(shù)字驗(yàn)證技術(shù)首席工程師 Jeremy Levitt。以下是該討論的摘錄。

從左到右：Axiomise 的 Darbari;Cadence 的 Zhang;新思科技的 Safarpour;和西門子的萊維特。

SE：當(dāng)有初創(chuàng)公司時，我們聽到了很多關(guān)于形式驗(yàn)證的進(jìn)步，但當(dāng)大型 EDA 公司內(nèi)部進(jìn)行開發(fā)時，我們聽到的就更少了。這里正在取得哪些技術(shù)進(jìn)步？

萊維特：這些都是指數(shù)級的問題，所以有足夠的空間來提高性能。有些地方存在不連續(xù)性，并且出現(xiàn)了新的算法。但即使沒有這一點(diǎn)，從一個版本到另一個版本，從年復(fù)一年，你會看到這些工具的速度提高了 25% 到兩倍。我們看到性能呈指數(shù)級增長。當(dāng)然，設(shè)計會越來越大，你在這里玩的是一個非常困難的追逐游戲。但是工具的性能有了顯著提高。這有時是由于啟發(fā)式方法的調(diào)整、應(yīng)用機(jī)器學(xué)習(xí)來找出更好的參數(shù)設(shè)置或更好的調(diào)查領(lǐng)域。這部分是由于使用了云，其中有額外的計算資源可用，這允許您并行執(zhí)行許多作。我們開始看到法學(xué)碩士的應(yīng)用帶來一些改進(jìn)，但這在未來可能比今天的工具更多。

Safarpour：初創(chuàng)公司確實(shí)會發(fā)出很大的噪音。我們已經(jīng)有一段時間沒有在純形式驗(yàn)證領(lǐng)域有初創(chuàng)公司了。使用正式的人們看到了大量的創(chuàng)新、巨大的影響以及他們可以解決的問題類型的擴(kuò)展。誰使用正式驗(yàn)證的情況發(fā)生了巨大變化。其中許多公司都表明，形式化驗(yàn)證可以在發(fā)現(xiàn)錯誤和簽核方面增加很多價值。我想談?wù)?SAT 比賽。SAT求解器是形式化驗(yàn)證的主要基礎(chǔ)求解器之一，SAT競賽已經(jīng)存在了大約20年。每隔一段時間，就會出現(xiàn)一個新的 SAT 求解器。有 Chaff 和 zChaff。這是開創(chuàng)性的，人們說這對于 NP 完全問題來說可能是最好的。然后 MiniSAT 出現(xiàn)了。這些事情發(fā)生了，然后有一段時間，即使是 SAT 專家也會說事情平靜下來。但如果你回到五年前，kissat，MapleSAT，很多新的求解器即將到來。如果你看看 SAT 比賽和最近的成績，他們只是把前一年的成績從水面上吹了出來。從求解器的基本層面一直到應(yīng)用鏈，仍然有很多創(chuàng)新正在發(fā)生。即使在這個基本層面上，仍然有很多創(chuàng)新正在發(fā)生。一些最新數(shù)據(jù)還顯示了人工智能如何幫助改進(jìn)許多此類 SAT 求解器算法。這非常令人興奮，而且有很多動作。對于社區(qū)之外的人來說，這很難看到，但我認(rèn)為在這個地區(qū)是一個非常激動人心的時刻。

張：Jasper（Cadence 旗下）在市場上仍然非常成功。大家的努力讓研發(fā)團(tuán)隊(duì)在開發(fā)新技術(shù)方面保持警惕。其中很多都是在引擎層面的幕后進(jìn)行的。這些是用戶可能看不到的改進(jìn)。我們的理想目標(biāo)不是給他們很多旋鈕讓他們調(diào)音，而是給他們編排，讓他們更容易使用正式的。這是多年來最大的挑戰(zhàn)。技術(shù)改進(jìn)、SAT 求解器和云、分布式計算——所有這些事情都在發(fā)生。所有公司都投入了大量資金，只是為了在競爭中保持平起平坐或領(lǐng)先。

Darbari：所有 EDA 公司都在生產(chǎn)出色的工具，這讓像我們這樣的人在該領(lǐng)域看起來很聰明。最近完成的很多工作都是在 SAT 求解器中完成的。作為形式化工具的用戶，我們看到它們在證明收斂率方面發(fā)揮了很大的作用。但讓我退后一步，描述定義正式用法的五個關(guān)鍵領(lǐng)域。第一個是財產(chǎn)生成。誰編寫了這些屬性，這些屬性有多好？除非它們是標(biāo)準(zhǔn)協(xié)議，否則它們不會在以太中發(fā)明。如果它們與規(guī)范掛鉤，那么房間里的大象問題就是，“你如何將復(fù)雜、龐大的規(guī)范轉(zhuǎn)化為有意義的屬性？除非你具備這一點(diǎn)，否則你實(shí)際上無法用形式來解決功能驗(yàn)證問題，盡管許多應(yīng)用程序驅(qū)動的形式仍在繼續(xù)使用并且正在產(chǎn)生很大的影響。除非我們開始通過與規(guī)范建立更好的聯(lián)系來在功能空間中采用形式化，并使屬性生成更快、更好、更高效，否則我們實(shí)際上無法在形式化方面產(chǎn)生太大的影響。效率帶來了另一個相關(guān)的挑戰(zhàn)，即約束細(xì)化并確保正確捕獲約束并有效地對其進(jìn)行建模。一旦完成了這兩件事——例如，編寫斷言并充分模擬假設(shè)以確保正確性和效率——那么如果它們失敗，您將面臨第三個挑戰(zhàn)，即調(diào)試。工具中發(fā)生了很多事情。然后你想談?wù)劮块g里的下一頭大象，這就是證明收斂。我們?nèi)绾巫屵@些事情變得更好更快？設(shè)計復(fù)雜性不斷增加數(shù)倍，因此總有追趕工作要做。但是，然后是簽字和報道，以及如何全面解決故事的所有最后部分，以確保所有經(jīng)過正式驗(yàn)證的內(nèi)容實(shí)際上都正確完成，芯片中沒有留下任何錯誤等等。從用戶的角度來看，這種轉(zhuǎn)變正在朝著解決方案層的定制化方向發(fā)展。這也是我們做很多工作的地方。客戶現(xiàn)在以一種他們以前沒有感知到的方式看到正式。例如，如果您談?wù)摰氖?RISC-V，我們已經(jīng)做了很多定制解決方案工作。我們從中發(fā)現(xiàn)了好處。十年前，如果你去找某人說你可以用正式的詳盡地驗(yàn)證一個有序處理器或無序處理器，他們會嘲笑你。這不是他們能想到的。但今天我們可以做到這一點(diǎn)。它是求解器和有效編寫屬性的應(yīng)用程序工程師的組合。許多正式的正在悄悄地在驗(yàn)證的各個方面發(fā)揮作用。我只談到了功能性，但它在其他方面也產(chǎn)生了巨大的影響。

Jeremy：我的第一個答案是關(guān)于發(fā)動機(jī)的性能，它肯定呈指數(shù)級增長。但 Ashish 提出了一個很好的觀點(diǎn)，即改進(jìn)的使用模型以及這些工具允許用戶訪問這種能力的難易程度。我們看到工具方面的持續(xù)創(chuàng)新，使用戶更容易指定他們想要的東西，就工具需求進(jìn)行溝通，并改進(jìn)整體流程，以便更廣泛的客戶和知識水平可以更有效地使用這些工具。

張：如果我回顧過去 20 年，一路上有哪些重大變化真正將正式推廣到更廣泛的用戶群？SystemVerilog 斷言的標(biāo)準(zhǔn)化是其中的關(guān)鍵部分，形式化作為一種技術(shù)在不同領(lǐng)域的擴(kuò)散。圍繞工具創(chuàng)建的特定于應(yīng)用程序的解決方案有助于找到可以使用正式的所有不同用例，也許沒有專業(yè)知識。這是一次偉大的冒險，它擴(kuò)大了正式應(yīng)用范圍。另一個想到的是正式簽字。在此之前，正式一直被視為一種調(diào)試工具。如果你不能在一個塊上簽字，它就會成為一個可有可無的，也許不是必備的。但是，一旦你能夠進(jìn)行簽核和有限制的簽核，當(dāng)你有了一種真正幫助人們從更嚴(yán)肅的角度看待正式的方法時，你就可以真正在流程中部署它。最近，隨著機(jī)器學(xué)習(xí)的注入，以及最近的 GenAI，正在發(fā)生的許多事情都是重要的里程碑，將正式視為驗(yàn)證流程的一部分。如今，我們必須做的宣教推銷少了很多。研發(fā)團(tuán)隊(duì)正在進(jìn)行的幕后所有其他事情——標(biāo)準(zhǔn)化、方法論——都有助于正式化。這確實(shí)是當(dāng)今每家公司都在使用的主流工具。

SE：我們聽到了很多關(guān)于數(shù)據(jù)中心進(jìn)步、CXL 和 HBM 等新技術(shù)的信息。正式版一直受到它需要的內(nèi)存量和計算量的限制。從理論上講，現(xiàn)在我們擁有無限的內(nèi)存和無限的計算。這對正式有多少幫助？

Levitt：這些新架構(gòu)可靠地為您提供了線性加速，但問題是指數(shù)級的，或者至少是 NP 困難的。我們會接受這一點(diǎn)，但我仍然想說大部分進(jìn)步是由 SAT 求解器的改進(jìn)推動的。這些正在呈指數(shù)級增長。與我們運(yùn)行的算法以及我們?nèi)绾尉幣潘鼈兿嚓P(guān)的工程改進(jìn)也呈指數(shù)級增長。提高計算能力，我們會接受這一點(diǎn)，但這是一種線性加速，如果它能讓你同時做更多的事情，有時是超線性的。但真正的性能改進(jìn)仍然來自基本的 SAT 求解器級別和算法級別，而不是來自資源可用性的增加。

Darbari：除了 SAT 求解器的效率之外，你如何對事物進(jìn)行建模也會對抽象產(chǎn)生重大影響。我有一個很好的例子，來自我們最近在 DVCon India 上展示的工作，關(guān)于 RISC-V 處理器。它有一個五到六級的深度管道，在一臺具有 1.5 TB RAM 和 96 個內(nèi)核的機(jī)器上運(yùn)行。我們得到了 10,331 個曲柄的有界證明。試圖證明“add”指令的一個實(shí)例可以在管道中發(fā)送并且實(shí)際上可以正確執(zhí)行。不要介意整個指令空間，只需一條“添加”指令。然后，我們完成了分解它并引入覆蓋率分析和抽象引擎的過程。然后，我們能夠在大約 100 秒內(nèi)證明相同的屬性，界限為 18。我們無法更早地證明這一點(diǎn)的唯一原因是處理器中存在活鎖。我們開始尋找它，因?yàn)檫@是一個 NP 難題，所以我們試圖一次性驗(yàn)證作數(shù)的所有實(shí)例和所有情況。如果這些案例中的任何一個遇到駝峰，則證明被卡住。你可以把最大的機(jī)器扔給它，但你實(shí)際上無法有所作為。一直使用正式的人都明白這一點(diǎn)。我能在較小的機(jī)器上獲得相同的結(jié)果嗎？在這種情況下，當(dāng)我們確實(shí)在具有 18 GB RAM 的 128 核機(jī)器上放置相同的測試平臺時，我們也得到了證明，只是花費(fèi)的時間有點(diǎn)長。計算會有所作為，但它是漸近的，除非我們了解正在驗(yàn)證的內(nèi)容以及如何建模，否則在問題上投入更多計算不會產(chǎn)生重大影響。

Safarpour：如果我們從用戶的問題角度來看，Ashish 說的是一個難以證明的單個屬性的問題，而且總是有這樣的案例。但我們看到的是，問題的巨大規(guī)模，以及他們試圖解決的財產(chǎn)的絕對數(shù)量，比前幾代人要大幾個數(shù)量級。從我們的客戶那里聽到，在正式的財產(chǎn)驗(yàn)證設(shè)置中，而不是連接或覆蓋范圍或類似的東西，他們有數(shù)十萬甚至數(shù)百萬的財產(chǎn)需要證明，這并不少見。在這些設(shè)置中，計算會產(chǎn)生很大的不同。如果您有數(shù)百個可用內(nèi)核或數(shù)千個可用內(nèi)核，那么您可以做很多事情。雖然證明一處房產(chǎn)總是很困難，但我們發(fā)現(xiàn)自己必須解決的挑戰(zhàn)之一是管理。您擁有數(shù)十萬個屬性，您有數(shù)百個核心可供您使用。即使您每晚運(yùn)行回歸或一周以上，有些屬性也沒有足夠的時間讓任何單個引擎對其進(jìn)行處理。你必須創(chuàng)新，因?yàn)樵谶^去，你不會遇到像現(xiàn)在這樣廣泛的問題。我們的客戶為我們帶來的大量產(chǎn)品已成為一項(xiàng)重大挑戰(zhàn)。機(jī)器可用性是存在的，但我們需要在編排和智能部署方面做的事情確實(shí)起著至關(guān)重要的作用。客戶確實(shí)會來找我們問，'如果我給你 10,000 個內(nèi)核怎么辦？如果我給你 100,000 個核心幾個小時怎么辦？你能破解這個嗎？它正在打開這個大規(guī)模并行的領(lǐng)域。這很棒。問題越來越難了。計算可用。這使我們能夠解決這些新問題。

張：從工具的角度來看，我們肯定希望利用并行化，利用所有的計算。但現(xiàn)實(shí)情況是，客戶沒有無限的計算能力。我們?nèi)栽谂ぷ鳎次覀兡転槟峁┑挠嬎懔坑邢蓿⑶椅覀冋谂c模擬和所有其他工具競爭。存在現(xiàn)實(shí)生活中的限制，但在技術(shù)方面，有很多進(jìn)步正在利用我們可以做的事情來并行化作業(yè)，以最有效的方式編排作業(yè)，利用以前的結(jié)果。所有這些改進(jìn)都是從工具的角度出發(fā)的。但我希望我們有無限的計算能力。