Functional verification of task partitioning for multiprocessor embedded systems

Das, Dipankar ; Chakrabarti, P. P. ; Kumar, Rajeev (2007) Functional verification of task partitioning for multiprocessor embedded systems ACM Transactions on Design Automation of Electronic Systems, 12 (4). No pp. given.. ISSN 1084-4309

Full text not available from this repository.

Official URL: http://portal.acm.org/citation.cfm?id=1278349.1278...

Related URL: http://dx.doi.org/10.1145/1278349.1278357

Abstract

With the advent of multiprocessor embedded platforms, application partitioning and mapping have gained primacy as a design step. The output of this design step is a multithreaded partitioned application where each thread is mapped to a processing element (processor or ASIC) in the multiprocessor platform. This partitioned application must be verified to be consistent with the native unpartitioned application. This verification task is called application (or task) partitioning verification. This work proposes a code-block-level containment-checking-based methodology for application partitioning verification. We use a UML-based code-block-level modeling language which is rich enough to model most designs. We formulate the application partitioning verification problem as a special case of the containment checking problem, which we call the complete containment checking problem. We propose a state space reduction technique specific to the containment checking, reachability analysis, and deadlock detection problems. We propose novel data structures and token propagation methodologies which enhance the efficiency of containment checking. We present an efficient containment checking algorithm for the application partitioning verification problem. We develop a containment checking tool called TraceMatch and present experimental results. We present a comparison of the state space reduction achieved by TraceMatch with that achieved by formal analysis and verification tools like Spin, PEP, PROD, and LoLA.

Item Type:Article
Source:Copyright of this article belongs to Association for Computing Machinery.
ID Code:5982
Deposited On:19 Oct 2010 10:00
Last Modified:20 May 2011 08:59

Repository Staff Only: item control page