Embodiments of the present invention provide for a method and system for verifying that an implementation design is functionally equivalent to a predetermined functionality of a reference design where the reference and implementation designs may correspond to a portion of a larger integrated circuit design. The use of Symbolic Trajectory Evaluation (STE) to compare the designs may result in false failures. Therefore, one aspect of the present invention provides for comparing an expected result from the reference design to an actual result of the implementation design in order to determine a set of failure conditions. Constraints are then selectively applied to the set of failure conditions in an attempt to remove them. Another aspect of the present invention allows for the selective use of symbols rather than "X"s (unknowns) in order to avoid false failures due to certain inputs of the implementation design not being properly stimulated.