基于可满足性模理论求解器与限界模型检测的符号轨迹计值方法和系统

本发明属于模型检测与符号模拟领域，涉及一种基于可满足性模理论求解器与限界模型检测的符号轨迹计值方法和系统。该方法包括：以硬件描述语言Chisel和以扩展轨迹计值逻辑描述的电路规范作为输入，通过预处理模块对扩展轨迹计值逻辑进行读取和对Chisel电路进行逻辑综合及SMT编码；通过模型检测后端模块基于SMT编码结合STE算法和BMC算法对电路规范进行验证。本发明结合了BMC和STE两者各自的优势来增强符号轨迹计值的求解能力，提高了模型检测的效率和可靠性，同时在Chisel层面扩展了STE的规范描述能力，大大简化了验证流程。