The rapid growth in hardware complexity has lead to a need for formal verification of hardware designs to prevent bugs from entering the final silicon. Model-checking [3] is by far the most popular technique for automatically verifying properties of designs. In model-checking, a model of a design is exhaustively checked against a property, often specified in some temporal logic. Today, all major hardware companies use model-checkers in order to reduce the number of bugs in their designs. Most model-checking techniques are state-based. This means that some kind of representation of all reachable states of the design is used when checking that the temporal properties are fulfilled. One popular way of representing the set of reachable states of a design is by using Binary Decision Diagrams (BDDs) [2]. A BDD is a canonical way of representing a boolean formula over a fixed set of variables. When the set of reachable states of a design can be calculated using BDDs, state-based model-checking techniques work very well. However, for some types of designs, it is very hard to represent all reachable states by BDDs; they grow exponentially in size and lead to a BDD blow-up.