基于动作细化的握手扩展
Handshaking Expansion Based on Action Refinement
-
摘要: 基于并发系统层次化设计动作细化的强大策略,建立了异步电路握手扩展的形式化语义,提出了一种握手扩展的细化模型。该语义采用等待事件结构,派生出带最大并发的真并发模型,细化系统同垂直互模拟关系的最初规范相一致,并且可以维护细化系统的正确性以及无死锁行为。构建的最大化并发模型,能有效地处理并发信息的综合和验证。Abstract: Handshaking expansion is a main procedure in the design of asynchronous circuits. At present, there is not description and definition for the refinement of handshaking expansion formality. Through investigating formal semantics of the handshaking expansion of asynchronous circuits, a refinement model for handshaking expansion is presented based on a powerful strategy of action refinement in the hierarchical design of concurrent systems. The proposed semantics employs wait event structures and then derives a true concurrency model with maximum parallelism. The refined system conforms to the original specification with respect to a vertical bisimulation relation. Furthermore, the refinement function preserves correctness and deadlock-freeness of the behavior in the refined system.