论文部分内容阅读
跨时钟城（ClockDomainCrossing，CDC）设计和验证是soC系统芯片设计的关键问题。讨论了异步FIFO的模型检验方法，利用模型检验工具SMV，建立了异步FIFO的有限状态机模型，使用时序逻辑LTL对该模型和属性进行了描述和验证。实验结果达到要求，同时表明该方法是行之有效的。与传统的模拟和仿真等验证方法相比较，模型检验具有能够自动进行、验证速度快、不用书写测试激励等优点。