Abstract: A solution for property verification of synchronous VHDL design is introduced, and VERIS-an efficient symbolic model checker is implemented. The model checker makes use of the specific feature of synchronous circuit design and the locality of verified property to reduce the state space of the internal finite state machine (FSM) model, thus speeding up the reachability analysis and property checking of circuits. A counterexample generation mechanism is also implemented. We have used the model checker to verify several benchmark circuits, the experimental results show that VERIS is more practicable and more suitable for the synchronous circuit design than Deharbe's model checker.