Functional verification of task partitioning for multiprocessor embedded systems
Functional verification of task partitioning for multiprocessor embedded systems
复制标题
多处理器嵌入式系统任务划分的功能验证
DOI：
10.1145/1278349.1278357
复制
发表时间：
2007
期刊：
影响因子：
--
通讯作者：
Rajeev Kumar
中科院分区：
文献类型：
--
作者：
D. Das;Partha Chakrabarti;Rajeev Kumar
随着多处理器嵌入式平台的出现，应用程序划分和映射已成为设计的首要步骤。该设计步骤的输出是多线程分区应用程序，其中每个线程被映射到多处理器平台中的处理元件(处理器或ASIC)。必须验证该分区应用程序与本机未分区应用程序一致。这种验证任务称为应用程序(或任务)划分验证。
提出了一种基于代码块级包容检查的应用划分验证方法。我们使用了一种基于统一建模语言的代码块级建模语言，该语言非常丰富，足以对大多数设计进行建模。我们将应用划分验证问题描述为包容检查问题的一个特例，我们称之为完全包容检查问题。我们提出了一种专门针对包容检查、可达性分析和死锁检测问题的状态空间约简技术。我们提出了新的数据结构和令牌传播方法，提高了包容检查的效率。针对应用程序划分验证问题，提出了一种高效的包容检查算法。我们开发了一个叫做TraceMatch的包容检测工具，并给出了实验结果。我们给出了TraceMatch与形式化分析和验证工具SPIN、PEP、PROD和LOLA所实现的状态空间缩减的比较。
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.