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

VERIS: An Efficient Model Checker for Synchronous VHDL Designs

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

A solution for property verification of synchronous VHDL design is introduced, and VERIS an efficient symbolic model checker is implemented. The model checker makes use of the specific feature of synchronous circuit design and the locality of verified property to reduce the state space of the internal finite state machine (FSM) model, thus speeding up the reachability analysis and property checking of circuits. A counterexample generation mechanism is also implemented. We have used the model checker to verify several benchmark circuits, the experimental results show that VERIS is more practicable and more suitable for the synchronous circuit design than Deharbe's model checker.