Symbolic trajectory evaluation is a new approach to formal hardware verification combining the circuit modeling capabilities of symbolic logic simulation with some of the analytic methods found in temporal logic model checkers. We have created such an evaluator by extending the symbolic switch-level simulator COSMOS. This program gains added efficiency by exploiting the ability of COSMOS to evaluate circuit operation over a ternary logic model, where the third value X represents an unknown logic value. This program can formally verify systems containing complex features such as switch-level models, detailed timing, and pipelining.