异步fifo的模型检验方法

跨时钟域(clockdomaincrossing,cdc)设计和验证是soc系统芯片设计的关键问题。讨论了异步fii}}()的模型检验方法，利用模型检验工具smv，建立了异步fifo的有限状态机模型，使用时序逻辑ltl对该模型和属性进行了描述和验证。实验结果达到要求，同时表明该方法是行之有效的。与传统的模拟和仿真等验证方法相比较，模型检验具有能够自动进行、验证速度快、不用书写测试激励等优点。