Hardware-software timing coverification of distributed embedded systems

Most of current codesign tools or methodologies only support validation in the form of cosimulation and testing of design alternatives. The results of hardware-software codesign of a distributed system are often not verified, because they are not easily verifiable. In this paper, we propose a new fo rmal coverification approach based on linear hybrid automata, and an algori thm for automatically converting codesign results to the linear hybrid auto mata framework. Our coverification approach allows automatic verification o f real-time constraints such as hard deadlines. Another advantage is that t he proposed approach is suitable for verifying distributed systems with arb itrary communication patterns and system architecture. The feasibility of o ur approach is demonstrated through several application examples. The propo sed approach has also been successfully used in verifying deadline violatio ns when there are inter-task communications between tasks with different pe riod lengths.