1. A computer-implemented method, the method performed by a processor, the method comprising: obtaining a set of functional attributes and associated domains with respect to a System Under Test (SUT); obtaining a set of restrictions over the functional attributes and associated domains; encoding 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 the Cartesian cross-product test-space by manipulating the BDD so as to assist in performing dynamic verification of the SUT.