A set of methods and their implementations are described that ensure efficient solution of verification problem for descriptions of combinational circuits under design and allow to detect errors at early design phases. The methods are based on simulation of a combinational circuit and formulating the overall problem as conjunctive normal form satisfiability testing.