由于同步电路设计的局限性,如时钟偏移、抖动、噪声和能耗方面,异步电路设计越来越受到人们的关注。异步电路已被广泛应用于各类电子系统中,因此它们的正确性必须仔细考虑。对异步电路的行为的描述和验证,是关于异步电路系统研究的关键问题。近些年,大多数的模拟和验证使用的都是基于状态的形式化模型,而基于动作的形式化模型,即事件结构,因为建模过程复杂的原因,很少被应用于系统的形式化仿真模拟和验证。本文选择扩展的绑定事件结构(EBES)对异步电路进行建模和验证,并对EBES的进程代数语义进行详细的介绍。事件是事件结构的基本单元,事件表示一个动作的发生,那么如何在异步电路中获取动作是十分关键的。为此,在本文中给出了从信号传输波型中获取动作的方法。通过信号传输波形,将每个信号分为4个动作,其中包含两个稳定动作表示信号的有效传输。根据EBES的定义,文中呈现了简单逻辑门的标记语义。由于复杂逻辑可以由基本逻辑单元组合而成,因此可以以组合的形式构建其EBES。异步电路的验证主要是判断其EBES实现和规范是否具有一致性。在使用互模拟等价检验时发现,要达到预想的结果,必须给实现添加太多的限制,但这样的电路是很难设计出来的。因此,文中选择逻辑符合,并且为了确保异步电路的准确性,在EBES的实现的基础上添加相对时序约束。最后,以常用的异步控制单元CElement为例,并对其进行了EBES建模和相对时序逻辑符合验证。除此之外,对CElement基于EBES和基于状态机的两种不同实现进行了比较,发现前者在描述行为时比后者更加直接、自然。