To make symbolic model checking approach applicable to all ω-regular properties, this paper studies symbolic model checking for ETL (extended temporal logic). First, the Tableau approach for LTL (linear temporal logic) is extended to that of ETL, and then the BDD (binary decision diagram)-based encodings of this technique is given. Moreover, the model checking tool ENuSMV is implemented based on NuSMV, which allows users to customize temporal connectives, and hence all ω-regular properties can be verified. Experimental results show that ETL can also be efficiently verified by the symbolic approach.