FSM Modeling of Synchronous VHDL Design for Symbolic Model Checking*

Abstract: In this paper, we defined a new FSM model that based on the synchronous behavior and symbolic representation technique. The algorithm to elaborate the model from the VHDL description of synchronous circuits is presented. By eliminating the unnesessary transition function, our model has much less states than Deharbe's mixed model[1]. The exprimental results demonstrate the model and modeling method can make symbolic model checking more practical