1. A computer-implemented method comprising: obtaining a set of functional attributes and domains with respect to a System Under Test (SUT), wherein each domain is associated with a functional attribute; obtaining a set of restrictions that restrict combinations of values of the functional attributes; encoding, by a computer on a non-transitory computer-readable medium, a Binary Decision Diagram (BDD) to represent a Cartesian cross-product test-space of all possible combinations of values of the functional attributes excluding combinations that are restricted by the set of restrictions, whereby the BDD symbolically represents the Cartesian cross-product test-space; and analyzing, by the computer, the Cartesian cross-product test-space by manipulating the BDD so as to assist in performing verification of the SUT.