随着数字系统规模的不断增大,单时钟域设计会极大地限制数字系统性能,现代数字系统为了提升性能,常采用多时钟域的设计。跨时钟域的信号在传输时会遇到亚稳态现象,如何保持系统稳定地传输数据是多时钟域系统设计者重点关注的问题,异步FIFO是一种优秀和有效的解决方案。如何避免亚稳态现象及空满控制信号的产生是异步FIFO设计的难点问题,常见的异步FIFO设计采用先同步读写指针后比较产生空满标志的方法,工作频率低,面积大,本文提出了一种新型异步FIFO的设计方法,优化了以格雷码编码的电路,提高异步FIFO的工作频率,用先比较读写指针产生空满标志,再同步到相应时钟域的方法,避免使用大量的同步寄存器,减少了面积空间。FPGA验证及EDA综合的结果表明,改进后的异步FIFO性能有了显著的提高。传统设计的验证是通过模拟验证来完成的,然而随着电路复杂性的日益增加,模拟验证需要开销大量的CPU时间,并且穷举的模拟验证很难保证设计的正确性。为了克服模拟验证的局限性,设计者求助于各种形式化的验证方法,如模型检验、定理证明和等价性检验等,使用形式化验证方法可以有效地保证设计的正确性。本文提出了一种基于SMV的异步FIFO的模型检验方法,利用符号化模型检验工具SMV对该系统模型和系统属性进行了验证,达到了预期的效果。通过异步FIFO的设计和形式化验证,可以有效地解决跨时钟域信号传输产生的亚稳态问题,有效地提升了数字系统的稳定性,同时也为数字系统的验证提供了一种可靠的方法。