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