Abstract: Symbolic Model Checking is the state-o-f 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²-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．