System-on-a-Chip (SoC) is centered at reuse of silicon Intellectual Properties (IPs) and characterized by separation of IP development and SoC system integration. Complexity of both IP and SoC system design grows exponentially and challenges the functional verification of these designs. Therefore, the dissertation finds the general goal of establishing a beyond-state-of-the-art, metrics-driven verification methodology. Mutation analysis is the focused metric here, which has a unique, complex test generation problem to detect (kill) an error-injected design (called a mutant). At IP level, first, an adaptive random simulation method is developed. Based on a modeling of random tests with Markov chain and constraints, the simulation process is continuously steered by a heuristic towards tests that are regarded more efficient in killing mutants. Second, with a portion of the mutants expected to be un-killed after random simulation, we solve the problem of further generating tests that kill each individual mutant. A search-based test generation method is developed, using real simulation results to guide an iterative process of finding a target test. At SoC system level, an IP-XACT mutation analysis framework is developed, assuming IP-XACT as the default language for SoC integration. A simulation engine for IP-XACT, in the form of an IP-XACT-to-SystemC generator that incorporates Transaction-Level Modeling, is built as the verification basis. IP-XACT mutation operators are defined by compiling a table of possible error injections on IP-XACT schema. The experiments show the efficiency of adaptive simulation of having more mutants killed with less simulation, the consistent performance from the cost function as guidance to search algorithm, and the practicality of IP-XACT simulation and mutation analysis for SoC system verification.