形式验证中同步时序电路的VHDL描述到S^2-FSM的转换

S 2 FSM:A VERIFICATION ORIENTED MODEL OF SYNCHRONOUS SEQUENTIAL CIRCUITS AND ITS MODELING ALGORITHM

符号模型检查（ＳｙｍｂｏｌｉｃＭｏｄｅｌＣｈｅｃｋｉｎｇ，ＳＭＣ）是一种有效的形式验证方法．该方法主要有２个难点：一个是建模，即如何建立并用有限内存来表示电路的状态机模型；另一个是在此模型基础上的验证算法．由于验证时间和有限状态机模型的大小是直接相关的，因而模型的大小就成为ＳＭＣ中的关键问题．本文提出一种基于同步电路行为描述的新的有限状态机模型Ｓ２－ＦＳＭ，并给出从同步电路的ＶＨＤＬ描述建立这种模型的过程．由于该模型的状态转换函数是基于时钟周期的，消去了与时钟无关的大量中间变量，所以同Ｄｅｈａｒｂｅ提出的模型相比，它的状态数大大减少．若干电路的实验结果表明，该模型由于减少了状态规模，建模时间和可达性分析时间大大减少，效果十分显著．

Symbolic Model Checking is the state of the art technique for property verification of sequential circuits. One key issue in the method is how to transform a circuit design to the corresponding FSM model with a compact state space. In this paper we present a new model S 2 FSM, which is specific of synchronous circuits, and give the modeling algorithm from synchronous VHDL descriptions. By fully utilizing the features of synchronous circuits, our model reduces the state variables greatly. Experimental results show that our model has much less states, costs much less CPU time in reachability analysis and makes symbolic model checking more practical.