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

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