公开(公告)号：CN117075969B

公开(公告)日：2024-07-23

申请号：CN202311088711.4

申请日：2023-08-28

申请人： 中国科学院软件研究所

发明人： 申世东 ,  刘易铖 ,  吴志林 ,  张立军

IPC分类号： G06F9/38 ,  G06F9/30 ,  G06F12/1009

摘要： 本发明公开了一种面向RISC‑V处理器特权指令集一致性的形式验证方法及装置，所述方法包括：在Chisel设计的待验证处理器中引出指令信号、通用寄存器信号、访存信号、控制和状态寄存器信号、TLB页表翻译信号到信号同步模块；将指令信号作为特权指令集参考模型执行的指令输入，并将通用寄存器信号、访存信号、控制和状态寄存器信号、TLB页表翻译信号与特权指令集参考模型的执行结果是否一致设为待验证性质；将特权指令集参考模型、待验证处理器、信号同步模块与待验证性质共同转换迁移系统模型；基于迁移系统模型，交由模型检测算法进行求解，得到待验证处理器的验证结果。本发明可以对RISC‑V特权指令集进行一致性验证。

公开(公告)号：CN117075969A

公开(公告)日：2023-11-17

申请号：CN202311088711.4

申请日：2023-08-28

申请人： 中国科学院软件研究所

发明人： 申世东 ,  刘易铖 ,  吴志林 ,  张立军

IPC分类号： G06F9/38 ,  G06F9/30 ,  G06F12/1009

摘要： 本发明公开了一种面向RISC‑V处理器特权指令集一致性的形式验证方法及装置，所述方法包括：在Chisel设计的待验证处理器中引出指令信号、通用寄存器信号、访存信号、控制和状态寄存器信号、TLB页表翻译信号到信号同步模块；将指令信号作为特权指令集参考模型执行的指令输入，并将通用寄存器信号、访存信号、控制和状态寄存器信号、TLB页表翻译信号与特权指令集参考模型的执行结果是否一致设为待验证性质；将特权指令集参考模型、待验证处理器、信号同步模块与待验证性质共同转换迁移系统模型；基于迁移系统模型，交由模型检测算法进行求解，得到待验证处理器的验证结果。本发明可以对RISC‑V特权指令集进行一致性验证。