《電子技術(shù)應(yīng)用》
您所在的位置：首頁(yè) > 人工智能 > 設(shè)計(jì)應(yīng)用 > 基于AI加速的可復(fù)用FPV平臺(tái)庫(kù)
基于AI加速的可復(fù)用FPV平臺(tái)庫(kù)
電子技術(shù)應(yīng)用
商思航，江璦琿，彭云霞，徐加山
深圳市中興微電子技術(shù)有限公司
摘要： 形式驗(yàn)證FPV可將DUT抽象為狀態(tài)空間進(jìn)行遍歷，針對(duì)動(dòng)態(tài)仿真難以隨機(jī)到的邊界場(chǎng)景、異常場(chǎng)景和復(fù)雜組合場(chǎng)景可提高收斂速度，增強(qiáng)驗(yàn)證質(zhì)量。但高質(zhì)量Property開(kāi)發(fā)對(duì)驗(yàn)證人員能力有較高的要求。面對(duì)該挑戰(zhàn)，基于Cadence公司Jaspergold ABVIP提出了一種可復(fù)用FPV平臺(tái)庫(kù)解決方案，可在不同模塊之間重用，降低FPV驗(yàn)證平臺(tái)搭建時(shí)間，提升Property質(zhì)量，同時(shí)借助其AI工具Proof Master生成加速Proven效率的database。FPV平臺(tái)庫(kù)+AI Database已在中興微電子某車規(guī)項(xiàng)目落地并復(fù)用，發(fā)現(xiàn)動(dòng)態(tài)仿真遺漏的4個(gè)故障。Proof Master可應(yīng)用于項(xiàng)目全周期內(nèi)，回歸效率平均提升80.17%，F(xiàn)PV平臺(tái)庫(kù)+AI database可提升FPV 初次Proven效率44.96%。與此同時(shí)對(duì)生成式大模型提升Property編寫效率做了一定探討。
中圖分類號(hào)：TN402 文獻(xiàn)標(biāo)志碼：A DOI: 10.16157/j.issn.0258-7998.240801
中文引用格式： 商思航，江璦琿，彭云霞，等. 基于AI加速的可復(fù)用FPV平臺(tái)庫(kù)[J]. 電子技術(shù)應(yīng)用，2024，50(8)：37-41.
英文引用格式： Shang Sihang，Jiang Aihui，Peng Yunxia，et al. AI accelerated reusable FPV platform[J]. Application of Electronic Technique，2024，50(8)：37-41.
AI accelerated reusable FPV platform
Shang Sihang，Jiang Aihui，Peng Yunxia，Xu Jiashan
Shenzhen Sanechips Technology Co.， Ltd.
Abstract： Formal Property Verification can abstract DUT into a state space for traversal, enhancing convergence speed and improving verification quality for boundary, exceptional, and complex combination scenarios that are difficult to reach through dynamic simulation. However, developing high-quality properties requires a high level of expertise from verification engineers. In the face of this challenge, this paper proposes a reusable FPV platform solution based on Cadence Jaspergold ABVIP, which can be reused across different modules, reducing FPV verification platform setup time, improving property quality, and leveraging AI tools to generate an accelerated proof efficiency database. The FPV platform library + AI database has been implemented and reused in a certain automotive project at Sanechips, identifying four faults missed by dynamic simulation. Proof Master can be applied throughout the project lifecycle, with an average regression efficiency improvement of 80.17%, and the FPV platform library + AI Database can enhance FPV initial proven efficiency by 44.96%. Meanwhile, this article also discusses the improvement of property writing efficiency using LLM.
Key words : formal；LLM；AI；Jaspergold

引言

與傳統(tǒng)的動(dòng)態(tài)仿真相比，屬性形式驗(yàn)證（Formal Property Verification, FPV）可將RTL代碼與使用者編寫的Property共同抽象成求解表達(dá)式（Conjunctive Normal Form, CNF），使用形式驗(yàn)證工具中不同的SAT求解器（Satisfiability, SAT）對(duì)其進(jìn)行證明?？蓪?duì)狀態(tài)空間進(jìn)行遍歷，即使結(jié)構(gòu)復(fù)雜的設(shè)計(jì)也能夠準(zhǔn)確地覆蓋邊界場(chǎng)景，保證了驗(yàn)證的完備性。

圖1為傳統(tǒng)FPV流程，其中驗(yàn)證功能點(diǎn)分解、自然語(yǔ)言描述編寫、Property編寫依賴于使用者對(duì)DUT的深入理解以及豐富的形式驗(yàn)證經(jīng)驗(yàn)，并且會(huì)花費(fèi)使用者較多時(shí)間。對(duì)于某些狀態(tài)空間較大的模塊，Property證明會(huì)花費(fèi)較多的時(shí)間和服務(wù)器資源。

000.png

圖1　傳統(tǒng)FPV流程圖

為了應(yīng)對(duì)此類挑戰(zhàn)，中興微電子提出了基于AI加速的可復(fù)用FPV平臺(tái)庫(kù)解決方案。針對(duì)功能類似的DUT，開(kāi)發(fā)一套通用的Property代碼與配套文檔，可實(shí)現(xiàn)同一項(xiàng)目?jī)?nèi)復(fù)用與不同項(xiàng)目間復(fù)用。并且在Jaspergold Proof Master@Cadence工具的支持下，基于平臺(tái)庫(kù)抽象成的CNF記錄當(dāng)前使用的SAT，以AI database的形式存儲(chǔ)下來(lái)，復(fù)用至其余功能類似的DUT。FPV平臺(tái)庫(kù)+AI database可以極大減少Property開(kāi)發(fā)時(shí)間與運(yùn)行時(shí)間，提升FPV驗(yàn)證效率與質(zhì)量。


本文詳細(xì)內(nèi)容請(qǐng)下載：

http://ihrv.cn/resource/share/2000006119


作者信息：

商思航，江璦琿，彭云霞，徐加山

（深圳市中興微電子技術(shù)有限公司，廣東 深圳 518054）


Magazine.Subscription.jpg

此內(nèi)容為AET網(wǎng)站原創(chuàng)，未經(jīng)授權(quán)禁止轉(zhuǎn)載。