基于动作细化的握手扩展

杨昕梅，孙秀莉，李绍荣

(1. 电子科技大学光电信息学院; 2. 美国波特兰州立大学电子与计算机工程学院)

近几年来，由于异步电路具有能够消除时钟歪斜问题，提供模块化设计以及适合处理环境变量的能力，异步电路设计引起了人们的广泛关注[1-2]。但由于CAD和设计方法的落后，限制了异步电路设计的发展。刻画异步电路是一个繁琐且容易出错的过程，而形式刻画是异步硬件设计的最主要问题。

层次化设计是当今广泛接受的硬件电路设计的最主要方法之一。动作细化是系统层次化刻画方法的核心操作，已发展成为常用的自顶向下系统设计理论[3-4]：以分层的方式描述系统，用较低抽象层次上复杂的进程解释较高抽象层次上的动作，从而改变其抽象层次，达到实现层次。虽然对该理论人们已经研究了多年，但是到目前为止，动作细化技术还没有被成功地应用于工业实际中。

握手扩展是异步控制电路分析自动化的重要步骤。文献[5]在动作系统的细化演算内证明了握手扩展的正确性，并重组了握手扩展，在其中插入了几个周期。文献[6]给出了一种异步控制电路分析自动化方法，该方法通过握手扩展及采用并发减少的事件重组来实现。然而，目前还没有对握手扩展过程作形式化细化定义和描述。

本文把动作细化的理论和技术应用到实际中,与具体的异步电路设计和验证相结合，产生一种新的握手扩展形式化描述方法。具体地，本文通过一个基于事件结构框架[7-8]中的参数化动作细化[9]的层次化方法，解决了握手扩展的形式化细化符号问题，并派生出一个带最大并发的真并发握手电路模型。而包含在事件结构框架中的细化系统与垂直互模拟关系的最初规范相一致[10]。该参数化动作细化功能可以维护细化系统的正确性以及无死锁行为[11]。

1 等待事件结构

在并发系统中，系统与它的环境交互需要依靠一些同步动作。从系统方面看，只有这些交互动作影响到系统的正确性。将系统中由环境触发的动作称为等待动作。为了区别等待动作和系统中的其他动作，将后者定义为活动动作。

设U是一个已知动作集，τ∉U是一个不可见的无声动作，而√∉U是终点标签，Act⊆U是一个活动动作集，W⊆U是一个由[a]指示的等待事件集。本文中a是活动动作。令是非自反且对称的关系，称为全局依赖关系，用作细化与序列合成的参数，依赖关系是一个抽象关系。

定义 1 一个等待事件结构是7元组

s∈ 是初始值。信号集合N包含电路规范的信号线；动作集合A包含N中的每一个信号x，以及升序的变型x+和降序的变型x－；事件集合E包含与发生指数匹配的动作；≺表示两事件的因果关系，每一个≺以(e,f)形式表示，由使能事件e以及被使能事件f构成。一个事件的使能事件发生了，该事件被使能。使能事件可以是活动动作，也可以是等待动作；状态s0包含N中每个信号的初始值；冲突关系#用来对分离行为和选择建模。

等待事件的结构描述如下：事件由黑点表示，黑点旁显示动作标签；e#e′由e与e′之间的点线标明，流动关系由箭头标明，而重复动作标记为箭头和点，为了不引起混淆，有时会用一个事件的动作标签来标记。图1a描述了一个选择接口(SEL)，图1b显示了等待事件结构的通道事件规范。

图1 SEL系统的框图和SEL等待事件结构规范

2 动作细化的握手扩展

一般系统都能分解为控制子系统和数据子系统。图2显示了多通道系统，图中L、M 和R是控制系统，P是数据系统，对于系统M，动作cd+是初始化数据计算和从输入到输出的传输，动作cd－是完成数据的计算。

图2 信道

在图2中，假设c1是输入通道，c2是系统M中c1对应的输出。不同信道类型组合而成的一般系统如图3所示。

图3 不同信道组合的等待事件结构

用4个阶段握手。将单信道周期由下一个转移序列取代，称为握手周期。req和ack的动作有req+，ack+，req ，ack－。相应的握手周期的下一部分只用来将所有动作设为false。

图4 系统M的细化函数

图5 图3a的带最大并发的细化等待事件结构

3 研究案例

最后，其实现如图7所示，它具有最大并发，并正确地保持其行为。

图6 系统SEL的细化函数

图7 细化后的SEL系统的等待事件结构

4 总 结

本文通过层次化方法派生出一个最大并发的真并发握手电路模型。基于参数化动作细化，通过将异步控制电路模拟为等待事件结构和公式化正确性准则，垂直互模拟，证明了握手扩展的正确性。此外，细化函数也保持握手电路的无死锁行为。根据本文的方法构建的最大化并发模型，能有效地处理并发信息的综合和验证。

[1] MYERS C J. Asynchronous circuit design[M]. NJ, USA:John Wiley & Sons Inc, 2001.

[2] EDWARDS D, MYERS B A. Balsa: an asynchronous hardware synthesis language[J]. Computer Journal, 2002 ,45(1): 12-18.

[3] WU Jin-zhao, YUE Hou-guang. Towards action refinement for concurrent systems w ith causal ambiguity[C]//Second International Conference on Software Engineering and Formal Methods (SEFM'04). [S.l.]: IEEE, 2004: 300-309.

[4] BIJL M van der , RENSINKk A, TRETMANS J. Action refinement in conformance testing[J]. Lecture Notes in Computer Science, 2005, 3502: 381-96.

[5] PLOSILA J, RUKSENAS R, SERE K. Action systems synthesis of DI circuits[C]//Proc of the International Refinement Workshop and Formal Methods Pasific 1998,Springer Series in Discrete Mathematics and Theoretical Computer Science. [S.l.]: Springer Verlag, 1998: 286-305.

[6] KONDRATYEV A, CORTADELLA J, KISHINEVSKY M,et al. Automatic synthesis and optimization of partially specified asynchronous system[C]//Proc International Conference on Computer-Aided Design. New Orleans,Louisiana, USA: ACM, 1999: 110-115.

[7] MAJSTER-CEDERBAUM M, WU J, YUE H. Refinement of actions for real-time concurrent systems w ith causal ambiguity[J]. Act a Information, 2006, 426(7): 389-418.

[8] WINSKEL G. An introduction to event structures[J]. Lecture Notes In Computer Science, 1988, 354: 364- 397.

[9] WEHRHEIM H. Parametric action refinement[J]. IFIP Transactions: Programming Concepts, Methods and Calculi,Elsevier, 1994, A(56): 247-266.

[10] RENSINK A, GORRIERI R. Action refinement as an implementation relation[C]//TAPSOFT’97: Theory and Practive of Software Development. [S.l.]: Springer-Velag,1997: 772-786.

[11] 孙秀莉. 基于动作细化的异步电路自动综合[D]. 成都:中国科学院研究生院(成都计算机应用研究所), 2005.

SUN Xiu-li. Automatic Synthesis of Asynchronous Circuits Based on Action Refinement[D]. Chengdu: Graduate University of Chinese Academy of Sciences (Chengdu Institute of Computer Application), 2005.

编 辑 漆 蓉