摘要: 1．本文的创新点
1)本文首次采用结构化方法在数据驱动异步流水线中进行死锁检测，避免了采用传统模型检验方法时的状态空间爆炸问题，降低了算法的复杂度，提高了检测效率。
2)本文提出在数据驱动异步流水线中进行slack弹性分析，指出Steer-Merge组合中通道的无slack弹性性质，并将该结论应用到异步流水线中进行死锁检测。
2．实现方法
首先采用形式化的方法定义一个由Steer, Merge, Fork, Join组成的部件网络是Well-formed的充分必要条件，并进行证明；然后通过分析部件网络中通道的Slack弹性指数，在原有的部件网络中引入Latch部件，从而解耦原有部件网络，引出数据驱动异步流水线是Well-formed的条件。作为应用，我们在Teak中实现了基于结构化方法的数据驱动异步流水线死锁的判定条件。针对Teak中存在的While和Loop循环结构，本文采取先破环后验证的方法，实验结果表明，该方法可以很好地解决数据驱动异步流水线中死锁判定问题。作为比较，我们还实现了传统基于Petri Net展开方法来进行死锁判定的方法。通过对每一个异步部件进行相应的Petri Net描述，构建整个部件网络的Petri Net描述，然后通过利用现有Petri Net展开工具Punf和验证工具MPSAT来进行测试。实验结果表明，我们的基于结构化的死锁判定方法大大降低了死锁判定的时间，提高了判定效率。值得一提的是，原有的采用传统方法几乎不可能解决的问题，用我们的方法可以在相对很短的时间内解决。
3．结论及未来待解决的问题
结论：本文采用基于结构化的方法来解决数据驱动异步流水线中的死锁判定问题，与传统基于状态可达性判定方法相比具有很高的效率优势。本文通过形式化证明的方法，证明了由Steer, Merge, Fork, Join组成的部件网络中不存在死锁的充要条件，同时研究了数据驱动异步流水线中的Slack弹性指数，并在一个现有的异步电路设计自动化工具Teak中实现了基于结构化死锁判定方法。实验方面，在几个较大规模电路中与传统验证方法进行了比较，效率优势明显。
未来的工作：本文主要局限性体现在它只是针对一类部件集合组成的部件网络进行死锁判定，在将来的工作中，我们会扩展这个部件集合，使得该方法可以有更大的适用范围。同时，由于本文只是针对了四段握手协议进行了分析，在将来的工作中，我们将研究两段握手协议的情况。