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)證的完備性。
