A major challenge in today's functional verification is the lack of a formal specification with which to compare the RTL model. The authors propose a novel top-down verification approach that allows specification of a design above the RTL. From this specification, it is possible to automatically generate assertion models and RTL reference models. The authors also demonstrate that symbolic simulation and equivalence checking can be applied to verify an RTL design against its specification.