In this paper, we propose a practical compositional verification approach based on symbolic model checking. The verification here is automatically and mechanically checked using the VIS (Verification Interacting with Synthesis) tool.  Based on the proposed compositional verification approach, we verified an Asynchronous Transfer Mode (ATM) Bit Error Rate MONitor (BERMON) circuit, which entire state space is beyond the capability of VIS and the memory available in the machine we used. Through out this paper, we use the BERMON circuit to illustrate the proposed abstraction and compositional reasoning techniques.