On the Functional Qualification of a Platform Model

This work focuses on the use of functional qualification for measuring the quality of co-verification environments for hardware/software (HW/SW) platform models. Modeling and verifying complex embedded platforms requires co-simulating one or more CPUs running embedded applications on top of an operating system, and connected to some hardware devices. The paper describes first a HW/SW co-simulation framework which supports all mechanisms used by software, in particular by device drivers, to access hardware devices so that the target CPU's machine code can be simulated. In particular, synchronization between hardware and software is performed by the co-simulation framework and, therefore, no adaptation is required in device drivers and hardware models to handle synchronization messages. Then, Certitude¿, a flexible functional qualification tool, is introduced. Functional qualification is based on the theory of mutation analysis, but it is extended by considering a mutation to be killed only if a testcase fails. Certitude¿ automatically inserts mutants into the HW/SW models and determines if the verification environment can detect these mutations. A known mutant that cannot be detected points to a verification weakness. If a mutant cannot be detected, there is evidence that actual design errors would also not be detected by the co-verification environment. This is an iterative process and functional qualification solution provides the verifier with information to improve the co-verification environment quality. The proposed approach has been successfully applied on an industrial platform as shown in the experimental result section.