We present a symbolic simulation based verification approach
        which can be applied to large synchronous circuits.
A new technique to encode the state and input
        constraints as {\em parametric Boolean expressions}
        over the state and input variables is used to make our 
        symbolic simulation based verification approach efficient.
The constraints which are encoded through parametric Boolean
        expressions can involve
        the Boolean connectives ($\cdot , + , \neg $), the
        relational operators ($< , \le , > , \ge, \ne , = $), and
        logical connectives ($\wedge , \vee $).
This technique of using parametric Boolean expressions vastly
        reduces the number of symbolic simulation vectors
        and the time for verification.
Our verification approach can also be applied for
        efficient modular verification of large designs;
        the technique used is to verify each constituent sub-module
        separately, however in the context of the overall design.
Since regular arrays are part of many large designs,
        we have developed an approach for the verification of regular arrays
        which combines formal verification at the high level
        and symbolic simulation at the low level(e.g., switch-level).
We show the verification of a circuit called {\em Minmax},
        a pipelined cache memory system,
        and an LRU array implementation of the least recently used
        block replacement policy, to illustrate our verification approach.
The experimental results are obtained using the COSMOS symbolic simulator.