在过去的二十年中,异步电路由于与同步电路相比具有无时钟偏差,易于集成,可靠性强等优势,在微处理器,低功耗电路等领域表现出相当的潜力。然而,异步电路的固有并发性也使得它们难以验证。由于组件和线延迟的变化,电路执行路径的数量可能非常大。因此,必须确保所有可能执行路径中电路行为的正确性。本文采用基于状态的模型检测方法,根据电路中的状态转换关系,提出了交织模式下积累状态向量的偏序关系模型,该模型能够详细地描述异步电路中状态的变化,通过向量的相关运算结果反映电路中状态变化的特点。半模性是异步电路设计中的一个重要属性,它与无危害电路密切相关。本文在基于交织模式的积累状态模型基础上,对电路的半模性进行检验。在积累状态偏序集对应的Hasse图上,详细讨论了逻辑门电路的半模格语义。鉴于电路的状态会随复杂度指数增长,本文提出了自动生成Hasse图和检验半模性的算法。最后,以异步电路基本单元C单元为例,对其进行了自动化验证,检验了算法的有效性。