Desynchronisation Technique Using Petri Nets
Desynchronisation Technique Using Petri Nets
复制标题
DOI：
10.1016/j.entcs.2009.07.028
复制
发表时间：
2009-08
期刊：
影响因子：
--
通讯作者：
S. Dasgupta;A. Yakovlev
中科院分区：
文献类型：
--
作者：
S. Dasgupta;A. Yakovlev
在本文中，我们考虑了将模块化同步规范去同步以实现到GALS架构中并获得可使用现有合成工具高效合成的简单包装器的问题。该系统建模使用Petri网（PN）和desperisation技术是基于PN局部理论。全局同步系统的触发语义的特征在于输入和输出转换的最大触发。同步系统的划分是通过将输入转换拆分并允许输出转换以最大步长触发来实现的，以便在分布式环境中实现异步通信。我们的模型满足两个基本的正确性属性，即语义保存和死锁预防，在从最大发射语义，其次是同步系统，标准的交错语义输入转换和最大步骤发射语义输出转换，其次是GALS架构。通过添加内部信号来支持局部的形成，所述内部信号对于在将生成局部时钟使能的局部中构建包装器是必要的。这些包装可以随后使用基于PN的合成工具进行合成。
In this paper we consider the problem of desynchronising modular synchronous specifications for their realisation into GALS architectures and obtaining simple wrappers that are efficiently synthesisable using existing synthesis tools. The systems are modeled using Petri nets (PN) and the desynchronisation technique is based on the theory of PN Localities. The firing semantics of a globally synchronous system is characterised by maximal firing of input and output transitions. The partitioning of a synchronous system is achieved by unbundling the input transitions and allowing the output transitions to fire in maximal steps, in order to enable asynchronous communication in a distributed environment. Our model satisfies the two essential correctness properties, namely, semantics preservation and deadlock prevention, during the shift from maximal firing semantics, followed by synchronous systems, to standard interleaving semantics for input transitions and maximal step firing semantics for output transitions, followed by GALS architectures. The formation of localities is supported by adding internal signals which are necessary for building wrappers in the localities that will generate local clock enables. These wrappers can be subsequently synthesised using PN based synthesis tools.