形式驗(yàn)證工具 文章 進(jìn)入形式驗(yàn)證工具技術(shù)社區(qū)

利用先進(jìn)形式驗(yàn)證工具來高效完成RISC-V處理器驗(yàn)證

• 我們在上一篇技術(shù)白皮書《基于形式驗(yàn)證的高效RISC-V處理器驗(yàn)證方法》中，以Codasip L31這款用于微控制器應(yīng)用的32位中端嵌入式RISC-V處理器內(nèi)核為例，介紹了一個(gè)基于形式驗(yàn)證的、易于調(diào)動(dòng)的RISC-V處理器驗(yàn)證程序。它與RISC-V ISA黃金模型和RISC-V合規(guī)性自動(dòng)生成的檢查一起，展示了如何有效地定位那些無法進(jìn)行仿真的漏洞。RISC-V的開放性允許定制和擴(kuò)展基于RISC-V內(nèi)核的架構(gòu)和微架構(gòu)，以滿足特定需求。這種對設(shè)計(jì)自由的渴望也正在將驗(yàn)證部分的職責(zé)轉(zhuǎn)移到不斷壯大的開發(fā)人員社群。然而，隨
• 關(guān)鍵字： 形式驗(yàn)證工具  RISC-V  驗(yàn)證