CSP模型驱动的异步硬件分层验证法

异步硬件验证方法基于CSP模型检测的层次结构是一种针对异步电路设计中的形式验证策略，随着异步和GALS设计技术的兴起，它们取代了传统的同步设计，通过局部握手协议去除全局时钟，带来了并发性和不确定性的增加，使得传统的仿真方法不足以充分检测潜在的问题，如死锁和延迟敏感性。 本文的核心贡献在于提出了一种创新的验证方法，它利用了Balsa系统，这是曼彻斯特大学AMULET小组开发的一种基于Communicating Sequential Processes (CSP)的工具。CSP是一种强大的建模语言，适用于描述并发系统的交互行为。文章展示了如何将异步硬件组件如握手网络和异步门电路转换为CSP形式，以便使用成熟的模型检查器FDR进行验证。这种方法的优势在于它能够适应异步硬件设计的分层结构，允许在不同抽象层次上进行验证，确保系统的一致性、延迟不敏感性和避免死锁等问题。 作者强调了数据独立性在解决数据路径缩减问题上的作用，这意味着提出的验证方法不仅可以增强设计过程的精确性，还能作为现有Balsa设计和合成流程的补充。论文的结构清晰，首先介绍了异步硬件设计的VLSI编译框架背景，接着详细介绍验证方法及其在解决实际设计挑战中的应用。 通过自动检测延迟敏感性和由死锁引发的错误，作者证明了这种方法的有效性和可行性，这对于保证异步硬件系统的正确性和性能至关重要。本文的研究成果对于异步硬件设计者和验证工具开发者来说，具有显著的实际价值和理论意义，推动了异步系统设计的可靠性提升。