The design of a VLSI system involves multiple design representations; and the design must go through several iterations aimed at meeting many performance and cost constraints. Verification that the design meets constraints is necessary. This research is developing rigorous verification methods that span multiple design representations, accommodate design revisions, and provide incisive partial verification methods (e.g. verification focussed on the "corners" of the behavioral space) that fit within designers' time budgets. These ideas are being validated by verifying the real asynchronous designs.