论文部分内容阅读
符号模型检查是一种有效的形式验证方法,该方法主要有2个难点:一个是建模,即如何建立并用有限内存来表示电路的状态机模型;另一个是在此模型基础上的验证算法,由于验证时间和有限状态机模型的大小是直接相关的,因而模型的大小就成为SMC中的关键问题;本文提出一种基于同步电路行为描述的有限状态机模型S^2-FSM,并给出从同步电路的VHDL描述建立这种模型的全过程,由于该模型的状态转换函数是基于时钟周期的,消