《電子技術應用》
您所在的位置:首頁 > 人工智能 > 設計應用 > 基于AI加速的可復用FPV平臺庫
基于AI加速的可復用FPV平臺庫
電子技術應用
商思航,江璦琿,彭云霞,徐加山
深圳市中興微電子技術有限公司
摘要: 形式驗證FPV可將DUT抽象為狀態空間進行遍歷,針對動態仿真難以隨機到的邊界場景、異常場景和復雜組合場景可提高收斂速度,增強驗證質量。但高質量Property開發對驗證人員能力有較高的要求。面對該挑戰,基于Cadence公司Jaspergold ABVIP提出了一種可復用FPV平臺庫解決方案,可在不同模塊之間重用,降低FPV驗證平臺搭建時間,提升Property質量,同時借助其AI工具Proof Master生成加速Proven效率的database。FPV平臺庫+AI Database已在中興微電子某車規項目落地并復用,發現動態仿真遺漏的4個故障。Proof Master可應用于項目全周期內,回歸效率平均提升80.17%,FPV平臺庫+AI database可提升FPV 初次Proven效率44.96%。與此同時對生成式大模型提升Property編寫效率做了一定探討。
中圖分類號:TN402 文獻標志碼:A DOI: 10.16157/j.issn.0258-7998.240801
中文引用格式: 商思航,江璦琿,彭云霞,等. 基于AI加速的可復用FPV平臺庫[J]. 電子技術應用,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

引言

與傳統的動態仿真相比,屬性形式驗證(Formal Property Verification, FPV)可將RTL代碼與使用者編寫的Property共同抽象成求解表達式(Conjunctive Normal Form, CNF),使用形式驗證工具中不同的SAT求解器(Satisfiability, SAT)對其進行證明。可對狀態空間進行遍歷,即使結構復雜的設計也能夠準確地覆蓋邊界場景,保證了驗證的完備性。

圖1為傳統FPV流程,其中驗證功能點分解、自然語言描述編寫、Property編寫依賴于使用者對DUT的深入理解以及豐富的形式驗證經驗,并且會花費使用者較多時間。對于某些狀態空間較大的模塊,Property證明會花費較多的時間和服務器資源。

000.png

圖1 傳統FPV流程圖

為了應對此類挑戰,中興微電子提出了基于AI加速的可復用FPV平臺庫解決方案。針對功能類似的DUT,開發一套通用的Property代碼與配套文檔,可實現同一項目內復用與不同項目間復用。并且在Jaspergold Proof Master@Cadence工具的支持下,基于平臺庫抽象成的CNF記錄當前使用的SAT,以AI database的形式存儲下來,復用至其余功能類似的DUT。FPV平臺庫+AI database可以極大減少Property開發時間與運行時間,提升FPV驗證效率與質量。


本文詳細內容請下載:

http://m.xxav2194.com/resource/share/2000006119


作者信息:

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

(深圳市中興微電子技術有限公司,廣東 深圳 518054)


Magazine.Subscription.jpg

此內容為AET網站原創,未經授權禁止轉載。
主站蜘蛛池模板: 欧美在线视频二区| 诗涵留学荷兰被黑人摘小说| 成全高清视频免费观看| 亚洲国产av无码精品| 精品人妻少妇一区二区三区不卡 | 好吊妞视频这里只有精品| 久久精品国产精品国产精品污| 波多野结衣潜入搜查官| 国产XXX69麻豆国语对白| 欧美性狂猛bbbbbxxxxx| 欧美大黑bbb| 午夜看片在线观看| 麻豆成人精品国产免费| 国产色视频在线| 久久亚洲精品无码gv| 欧美精品亚洲精品日韩| 国产人与zoxxxx另类| 2019国产麻豆剧传媒视| 宝贝过来趴好张开腿让我看看| 久久精品午夜福利| 欧美日韩亚洲国产精品| 免费人成网站在线观看不卡 | freee×xx性欧美| 无翼乌全彩无遮挡之老师| 亚洲AV无码成人网站在线观看| 波多野结衣系列cesd819| 午夜在线观看免费影院| 韩国伦理片久久电影网| 妖精www视频在线观看高清| 久久精品国1国二国三| 欧美大尺度xxxxx视频| 人人鲁免费播放视频人人香蕉| 老司机一级毛片| 国产成人免费一区二区三区| 3d动漫精品啪啪一区二区免费| 女人扒开腿让男人桶| 中文字幕亚洲欧美日韩在线不卡 | 最近更新2019中文字幕国语4| 十分钟免费视频高清完整版www| 黑人大长吊大战中国人妻| 女人扒开腿让男人捅啪啪|