针对同步时序电路VHDL设计的有效模型判别器VERIS

摘要：

介绍了一个针对同步时序电路 VHDL 设计的性质验证的解决方案——一个有效的符号模型判别器VERIS.该模型判别器利用同步时序电路设计的特点以及待验证性质的局部性，可显著地减少有限状态机（FSM）的状态空间；大大地提高可达性分析和性质验证的速度；同时，实现了反例生成机制.实验结果表明，与Deharbe的模型判别器相比，用这个模型判别器验证一些基准电路更加适用于同步时序电路.

关键词：形式验证、模型判别器、VHDL、同步时序电路、有限状态机、FSM

所属期刊栏目：13

分类号：TP302(计算技术、计算机技术)

资助基金：国家重点基础研究发展计划973计划G1998030411

在线出版日期：2004-01-08（万方平台首次上网日期，不代表论文的发表时间）

页数：共5页

页码：485-489