论文部分内容阅读
符号模型检查（ＳｙｍｂｏｌｉｃＭｏｄｅｌＣｈｅｃｋｉｎｇ，ＳＭＣ）是一种有效的形式验证方法．该方法主要有２个难点：一个是建模，即如何建立并用有限内存来表示电路的状态机模型；另一个是在此模型基础上的验证算法．由于验证时间和有限状态机模型的大小是直接相关的，因而模型的大小就成为ＳＭＣ中的关键问题．本文提出一种基于同步电路行为描述的新的有限状态机模型Ｓ２－ＦＳＭ，并给出从同步电路的ＶＨＤＬ描述建立这种模型的过程．由于该模型的状态转换函数是基于时钟周期的，消去了与时钟无关的大量中间变量，所以同Ｄｅｈａｒｂｅ提出的模型相比，它的状态数大大减少．若干电路的实验结果表明，该模型由于减少了状态规模，建模时间和可达性分析时间大大减少，效果十分显著．
SymbolicModelChecking (SMC) is an effective method of formal verification. The method has two main difficulties: one is modeling, that is, how to build and use finite memory to represent the state machine model of the circuit; the other is the verification algorithm based on this model. Since the verification time is directly related to the size of the finite state machine model, the size of the model becomes a key issue in SMC. In this paper, we present a new finite state machine model S2-FSM based on the description of synchronous circuit behavior and give the procedure of establishing this model from the VHDL description of the synchronous circuit. Since the state transition function of the model is clock-based, eliminating a large number of clock-independent intermediate variables, its number of states is significantly reduced compared to the model proposed by Deharbe. The experimental results of several circuits show that the model has a significant effect due to the reduced state scale, greatly reduced modeling time and reachability analysis time.