在金融领域,嵌入式产品越来越复杂同时应用越来越广泛,但嵌入式产品稳定性一直没有得到有效地解决,所以会在正常的金融交易中存在安全隐患,这往往会给人们在日常金融交易带来不便甚至是财产损失。为了解决这方面的问题,本文对基于模型检测的外设控制器验证方法进行分析和研究,最大限度地提高嵌入式产品的稳定性,具有一定的应用价值。论文主要工作如下:1.硬件设计验证方法以及模型检测的国内外研究现状综述。对硬件验证方法相关技术进行研究,其中包括验证方法学分析,基于SystemVerilog验证关键技术以及模型检测硬件验证相关技术分析。2.模型检测建模方法研究。包括用例模型转化状态模型方法研究,状态模型转化为nuSMV模型方法及其转换规则研究;对模型检测属性设计方法研究,其中包括属性提取方法研究、属性分解方法研究,以及属性设计方法研究;最后实例分析,以实际开发项目A类点钞机为平台,对接触式图像传感器控制器进行用例建模、状态建模、nuSMV建模,用模型检测进行验证并产生反例,通过反例不断修改接触式图像传感器控制器,最终设计出稳定性好的接触式图像传感器控制器。3.模型检测属性设计方法的研究。通过提出正向提取法和逆向提取的方法,解决系统属性提取不够全面、由状态爆炸引起属性急剧增多,无法进行属性描述的问题。4.CIS(Contact Image Sensor,接触式图像传感器)控制器并进行设计与验证。针对CIS控制器进行用例建模、状态图建模、unSMV建模、Verilog建模,用基于模型检测的方法对其进行验证,根据模型检测验证工具提供的反例进行设计修改,直到设计满足要求为止,解决了在实际项目中图像采集不稳定、质量差的问题。本课题通过使用基于模型检测的验证方法完成接触式图像传感器控制器的设计,解决了项目中接触式图像传感器控制器采集图像不稳定,图像质量差的问题,在硬件设计领域基于模型检测的验证方法应用将会越来越广泛。