%0 Journal Article
%T 异步fifo的模型检验方法
%A 罗莉
%A 欧国东
%A 刘彬
%A 徐炜遐
%A 窦强？
%J 计算机科学
%D 2012
%X 跨时钟域(clockdomaincrossing,cdc)设计和验证是soc系统芯片设计的关键问题。讨论了异步fii}}()的模型检验方法，利用模型检验工具smv，建立了异步fifo的有限状态机模型，使用时序逻辑ltl对该模型和属性进行了描述和验证。实验结果达到要求，同时表明该方法是行之有效的。与传统的模拟和仿真等验证方法相比较，模型检验具有能够自动进行、验证速度快、不用书写测试激励等优点。
%K cdc（clockdomaincrossing)
%K 异步fifo
%K ltl
%K 符号模型检验
%K smv
%U http://www.jsjkx.com/jsjkx/ch/reader/view_abstract.aspx?file_no=120361&flag=1